Formal mutation testing for
Formal mutation testing for
复制标题
正式突变测试
DOI：
10.1016/j.infsof.2016.04.003
复制
发表时间：
2017
影响因子：
3.9
通讯作者：
Alberto A
中科院分区：
文献类型：
--
作者：
Alberto A
背景：行业对更可靠和可伸缩的测试开发机制的需求促进了使用正式模型来指导测试的生成。尽管基于状态的模型已经取得了许多进展，如有限状态机（FSM）和输入/输出转换系统（IOTS），更先进的形式主义，需要指定大型，状态丰富，并发系统。马戏团，一个状态丰富的进程代数结合Z，CSP和细化演算，是适合这一点;然而，从这样的模型派生测试相应地更具挑战性。最近，一个测试理论已被声明forCircus，允许验证的过程细化基于穷举测试sets.Objective：我们研究基于故障的测试细化从Circus规格使用突变。我们寻求这样的技术在测试集质量断言和基于故障的测试用例选择的好处。我们的目标相关的结果不仅为马戏团，但任何进程代数的细化，结合CSP与数据language.Method：我们提出了一个正式的定义为基于故障的测试集，扩展theCircustesting理论，和广泛的研究突变算子为马戏团。利用这些结果，我们提出了一种方法来生成测试杀死突变体。最后，我们解释了如何原型工具支持可以获得与实施的突变体生成器，翻译fromCircusto CSP，和细化检查CSP，并与一个更复杂的链的工具，支持使用的symbolic tests.Results：我们正式的突变测试forCircus，定义了详尽的测试集，可以杀死一个给定的突变体。我们还提供了一种技术来选择测试从这些集的基础上规范的痕迹的突变体。最后，我们提出了突变算子，考虑故障相关的反应和数据操作行为。总而言之，我们为Circus定义了一种新的基于故障的测试生成技术。结论：我们得出的结论是，Circus的突变测试可以通过关注特定故障，真正帮助从状态丰富的模型中生成更易于处理的测试。
Context:The demand from industry for more dependable and scalable test-development mechanisms has fostered the use of formal models to guide the generation of tests. Despite many advancements having been obtained with state-based models, such as Finite State Machines (FSMs) and Input/Output Transition Systems (IOTSs), more advanced formalisms are required to specify large, state-rich, concurrent systems.Circus, a state-rich process algebra combining Z, CSP and a refinement calculus, is suitable for this; however, deriving tests from such models is accordingly more challenging. Recently, a testing theory has been stated forCircus, allowing the verification of process refinement based on exhaustive test sets.Objective:We investigate fault-based testing for refinement fromCircusspecifications using mutation. We seek the benefits of such techniques in test-set quality assertion and fault-based test-case selection. We target results relevant not only forCircus, but to any process algebra for refinement that combines CSP with a data language.Method:We present a formal definition for fault-based test sets, extending theCircustesting theory, and an extensive study of mutation operators forCircus. Using these results, we propose an approach to generate tests to kill mutants. Finally, we explain how prototype tool support can be obtained with the implementation of a mutant generator, a translator fromCircusto CSP, and a refinement checker for CSP, and with a more sophisticated chain of tools that support the use of symbolic tests.Results:We formally characterise mutation testing forCircus, defining the exhaustive test sets that can kill a given mutant. We also provide a technique to select tests from these sets based on specification traces of the mutants. Finally, we present mutation operators that consider faults related to both reactive and data manipulation behaviour. Altogether, we define a new fault-based test-generation technique forCircus.Conclusion:We conclude that mutation testing forCircuscan truly aid making test generation from state-rich model more tractable, by focussing on particular faults.