论文部分内容阅读
如何从协议规范出发生成满足一定覆盖标准的测试序列和测试套是协议一致性测试中的一个核心问题，现有的协议一致性测试序列和测试套生成方法大部分都是基于协议的FSM模型。
模型检查技术通常用于硬件电路以及协议规范的形式化验证中，本文将模型检查技术引入到以EFSM为模型的协议一致性测试序列和测试套的自动生成中，认为生成满足一定测试覆盖标准的测试套问题可以转化为模型检查中的反例构造问题，进而提出了一种新的测试生成方法。该方法用Kripke结构描述协议的EFSM模型，用一系列CTL公式刻画测试套所要满足的控制流和数据流覆盖标准，然后利用模型检查工具所具有的反例构造功能为每个CTL公式构造一个反例，每个反例对应于一条满足一定覆盖要求的测试序列，所有CTL公式的反例集合就对应于满足一定覆盖标准的测试套。该方法的显著优点在于：自动生成的测试序列和测试套是完全可执行的。