基于模型检测技术的变异测试用例生成方法

Approach of Mutation Test Case Generation Based on Model Checking

为了进行基于模型的软件测试变异分析,文中提出了一种基于模型检测的变异测试用例生成方法。基于模型检测工具UPPAAL的形式化分析与测试框架,首先用符合规范的时间自动机模型描述被测系统;然后基于时间自动机模型的基本结构和语法,对系统模型进行一组变异操作,并模拟实现时可能出现的一些错误;对变异后的模型分别使用UPPAAL Yggdrasil工具,生成一组能覆盖变异区域的测试用例;在系统变异模型上执行生成的测试用例,根据测试执行结果(是否能"杀死"变异体)筛选出一组有效的测试用例。通过实例验证,所提方案生成的测试用例是有效的,且测试用例集变异分数优于现有的基于状态机复制的变异测试用例自动生成方法和基于模型中变换覆盖的变异测试用例生成方法。

In order to carry out mutation analysis of software testing,this paper proposed a method generating mutation test case based on model checking.Using formalized analysis of UPPAAL and test framework,the system under test is firstly described as a timed automata which conforms to its specifications.Then a set of mutation operation following timed automata’s basic structure and grammar are injected into the original model to simulate some implementation error which may occur.The mutated models and accessibility property are used as inputs to UPPAAL Yggdrasil to gene-rate test cases covering mutation area.Lastly,test cases are executed on the mutated model and a set of valid test cases is selected on the basis of test execution result(whether the test case can kill the mutation).Experimental results show that the generating test case of the proposed method is valid.Moreover,the mutation score of test case set is higher than that of the existing one based on state machine duplication and model’s transition coverage.