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

Using model checking to generate test cases for class testing

提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的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.