archives

A Model Checking Approach to Protocol Conversion


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Sinha, Roopak, Roop, Partha and Basu, Samik (2006) A Model Checking Approach to Protocol Conversion. Technical Report 0000482, Computer Science, Iowa State University.

Full text available as:Adobe PDF

Abstract

Protocol conversion for mismatched protocols has been addressed in a number of formal and informal settings. However, existing solutions address this problem only partially. This paper develops the first on-the-fly local approach to protocol conversion based on temporal logic model checking. The tableau-based approach verifies the existence of a converter and if a converter exists, it is automatically synthesized. Our approach handles control and data mismatches under a single unifying framework. A NuSMV-based implementation has been developed and we provide results for some non-trivial protocol mismatch examples.

Keywords:Formal methods, model checking, protocol conversion
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:00000497
Deposited by:Samik Basu on 11 January 2007



Contact site administrator at: ssg@cs.iastate.edu