A Model Checking based Converter Synthesis Approach for Embedded Systems







Deposit Papers 


Basu, Samik, Sinha, Roopak and Roop, Partha (2006) A Model Checking based Converter Synthesis Approach for Embedded Systems. Technical Report, Department of Computer Science, Iowa State University.

Full text available as:Adobe PDF


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.

Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
ID code:00000537
Deposited by:Samik Basu on 18 April 2007

Contact site administrator at: