Test Case Generation from Mutants Using Model Checking Techniques
Test Case Generation from Mutants Using Model Checking Techniques
复制标题
使用模型检查技术从突变体生成测试用例
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
G. Fey
中科院分区：
文献类型：
--
作者：
Heinz Riener;R. Bloem;G. Fey
突变测试是一种强大的测试技术：在程序中植入人为错误并进行测试。未被发现的故障可以用来改进试验台。从未检测到的错误自动生成测试用例的问题通常没有被现有的突变测试系统解决。我们提出了一个符号过程，即Sym BMC，用于使用有界模型检查（BMC）技术从给定程序生成测试用例。Sym BMC过程确定一个测试台，该测试台根据给定的展开边界检测影响程序语义的所有种子错误。我们已经构建了一个原型工具，该工具使用可满足模理论（SMT）求解器来生成测试用例，并展示了ANSI-C基准程序的初始结果。
Mutation testing is a powerful testing technique: a program is seeded with artificial faults and tested. Undetected faults can be used to improve the test bench. The problem of automatically generating test cases from undetected faults is typically not addressed by existing mutation testing systems. We propose a symbolic procedure, namely Sym BMC, for the generation of test cases from a given program using Bounded Model Checking (BMC) techniques. The Sym BMC procedure determines a test bench, that detects all seeded faults affecting the semantics of the program, with respect to a given unrolling bound. We have built a prototype tool that uses a Satisfiability Modulo Theories (SMT) solver to generate test cases and we show initial results for ANSI-C benchmark programs.