基于模型检测工具NuSMV的功能测试用例生成方法

摘要

对现今已有的基于模型检测的测试用例生成方法以及覆盖准则进行了研究，在此基础上设计一个基于模型检测工具NuSMV生成功能测试用例的方法。首先，从被测系统状态图入手，经过抽象映射成NuSMV支持的模型验证器( SMV)模型；其次，将测试覆盖标准以CTL时序逻辑公式给出，并设计出陷阱性质；最后，利用NuSMV进行模型检测，自动获得反例集，在去除冗余后，自动生成能够满足变换覆盖和状态覆盖的功能测试用例集。实验结果表明，该方法能够生成满足变换覆盖和状态覆盖的功能测试用例集，与传统方法相比，减少了测试用例生成的工作量，简化了测试用例集。