一种基于模型检验的类测试用例生成方法  

Using model checking to generate test cases for class testing

作　　者：梁陈良[1,2] 聂长海[1,2] 徐宝文[1,2] 陈振宇[1,2] 

机构地区：[1]东南大学计算机科学与工程学院,南京210096 [2]江苏省软件质量研究所,南京210096

出　　处：《东南大学学报（自然科学版）》2007年第5期776-781,共6页Journal of Southeast University：Natural Science Edition

基　　金：国家杰出青年科学基金资助项目(60425206);国家自然科学基金资助项目(60403016);江苏省自然科学基金资助项目(BK2005060);东南大学优秀青年教师教学科研资助项目

摘　　要：提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的Kripke结构.使用CTL公式描述测试覆盖标准,然后把这组CTL公式和描述类状态行为的Kripke结构输入模型检验工具,并利用模型检验工具自动生成相应的证据路径,最后将路径转化成满足相应覆盖标准的类测试用例.该方法直接从源代码生成测试用例,并使用贪心法约减冗余用例以降低测试成本.实验表明该方法生成的测试用例具有较高的覆盖率.A novel approach is presented to generate test cases for class testing. The states and the behaviors of the object are extracted from the source code. Then the class under testing is characterized abstractly with a 4-tuple, which can be converted into an equivalent Kripke model. The coverage criteria are expressed by computer tree logic （CTL） formulae. Model checker generates witnesses automatically when verifying CTL formulae on that Kripke model. The witnesses can be converted into a test suite which satisfies the corresponding coverage criteria. Test cases are generated from source code directly, and the greedy method is used to reduce redundant test cases in order to save the cost of software testing. The experimental results show that test cases generated by the proposed approach can achieve high rate of coverage.

关 键 词：软件测试 模型检验 时序逻辑 测试用例 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]