A Model Checking based Converter Synthesis Approach for Embedded Systems
Samik Basu, Roopak Sinha, Partha S. Roop · Iowa State University Digital Repository (Iowa State University) · 2006
Protocol conversion problem involves identifying whether two or more protocols can be com-posed with or without an intermediary, referred to as a converter, to obtain a pre-specied desired behavior. We investigate this problem in formal setting and propose, for the rst time, a temporal logic based automatic solution to the convertibility verication and synthesis. At its core, our tech-nique 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 rst time), using a single unifying model checking based solution. Secondly, the proposed approach uses temporal logic for the specication of correct behaviors (un-