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

【Abstract】 The existing methods and coverage criterion of test case generation based on model checking were studied. On this basis,a method of generating functional test cases based on the model checker Nu SMV was presented. First of all,this method started from the state diagram of the system under test,mapped to a SMV( Cymbolic Model Verifier) model; then expressed the coverage criterion by CTL temporal logic and designed the trap properties combined with the transition coverage;finally automatically got the set of counter examples by using the Nu SMV to check model,after reducing the test suite,automatically generated functional test cases satisfied with the transition coverage and state coverage. The experiment results show that this method can generate functional test suite satisfied the transition coverage and state coverage. Compared with the traditional method,the proposed method reduces the task and simplifies the test suite.更多还原