A Model Checking Approach to Protocol Conversion

Abstract

<p>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.</p>