A Model Checking Approach to Protocol Conversion

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

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.