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

关键词: 一致性测试；模型检查；测试序列；测试套

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

Key words: Conformance test; Model checking; Test sequence; Test suite