A Model Checking based Converter Synthesis Approach for Embedded Systems

Date
2006-11-01
Authors
Basu, Samik
Sinha, Roopak
Roop, Partha
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

Protocol conversion problem involves identifying whether two or more protocols can be composed with or without an intermediary, referred to as a converter, to obtain a pre-specified desired behavior. We investigate this problem in formal setting and propose, for the first time, a temporal logic based automatic solution to the convertibility verification and synthesis. At its core, our technique is based on local model checking technique and determines the existence of the converter and if a converter exists, it is automatically synthesized. A number of key features of our technique distinguishes it from all existing formal and/or informal techniques. Firstly, we handle both data and control mismatches (for the first time), using a single unifying model checking based solution. Secondly, the proposed approach uses temporal logic for the specification of correct behaviors (unlike earlier automaton based specifications) which is both elegant and natural to express event ordering and data-matching requirements. Finally, we have have experimented extensively with the examples available in the existing literature to evaluate the applicability of our technique in wide range of applications.

Description
Keywords
Citation
DOI
Source
Collections