基于模型检查的协议一致性测试套自动生成

Automatic Protocol Conformance Test Suite Generation Based on Model Checking

提出一种构造完全可执行协议一致性测试套的新方法。该方法分别用Kripke结构和CTL公式来描述协议的EFSM模型和测试套所要满足的控制流和数据流测试覆盖标准,借助模型检查中的例证构造技术生成满足相应覆盖标准的测试套。在此基础上该文给出了测试套优化算法。实验结果表明该方法可行有效。

A new method is proposed to generate executable protocol conformance test suite using model checking technique, Using Kripke structure and CTL formulate, this paper formulates the problem of test generation from protocol＇s EFSM model as the problem of finding witnesses in model checking. This paper also gives a heuristic algorithm to optimize the test suite. The results show the feasibility and effectivity of this method.