Analyzing Interoperability of Protocols Using Model Checking  

作　　者：WUPeng 

机构地区：[1]LaboratoryofComputerScience,InstituteofSoftware,ChineseAcademyofSciences,GraduateSchooloftheChineseAcademyofSciences,Beijing100080,China

出　　处：《Chinese Journal of Electronics》2005年第3期453-457,共5页电子学报（英文版）

摘　　要：In practical terms, protocol interoperability testing is still laborious and error-prone with little effect, even for those products that have passed conformance testing. Deadlock and unsymmetrical data communication are familiar in interoperability testing, and it is always very hard to trace their causes. The previous work has not provided a coherent way to analyze why the interoperability was broken among protocol implementations under test. In this paper, an alternative approach is presented to analyzing these problems from a viewpoint of implementation structures. Sequential and concurrent structures are both representative implementation structures, especially in event-driven development model. Our research mainly discusses the influence of sequential and concurrent structures on interoperability, with two instructive conclusions: (a) a sequential structure may lead to deadlock; (b) a concurrent structure may lead to unsymmetrical data communication. Therefore, implementation structures carry weight on interoperability, which may not gain much attention before. To some extent, they are decisive on the result of interoperability testing. Moreover, a concurrent structure with a sound task-scheduling strategy may contribute to the interoperability of a protocol implementation. Herein model checking technique is introduced into interoperability analysis for the first time. As the paper shows, it is an effective way to validate developers' selections on implementation structures or strategies.

关 键 词：通讯协议 协同工作 构象理论 CCS 

分 类 号：TN915.04[电子电信—通信与信息系统]