基于符号模型的变异测试：结合可达性和精化检查
Towards Symbolic Model-Based Mutation Testing: Combining Reachability and Refinement Checking
摘要：
基于模型的突变测试使用改变的测试模型来导出测试用例，这些测试用例能够揭示模型化的故障是否已经实现。这需要检查原始模型和变异模型之间的一致性。本文提出了一种用于动作系统的符号一致性检查的方法，该方法非常适合于指定反应式系统。我们还考虑在我们的模型中的非决定性。因此，我们不检查等价性，而是检查精化。我们编码的过渡关系，以及作为一个约束满足问题的一致性关系，并使用约束求解器在我们的可达性和细化检查算法。显式一致性检查技术经常面临状态空间爆炸。第一个实验评估表明，我们的方法有可能优于显式一致性检查。
英文摘要：
Model-based mutation testing uses altered test models to derive test cases that are able to reveal whether a modelled fault has been implemented. This requires conformance checking between the original and the mutated model. This paper presents an approach for symbolic conformance checking of action systems, which are well-suited to specify reactive systems. We also consider nondeterminism in our models. Hence, we do not check for equivalence, but for refinement. We encode the transition relation as well as the conformance relation as a constraint satisfaction problem and use a constraint solver in our reachability and refinement checking algorithms. Explicit conformance checking techniques often face state space explosion. First experimental evaluations show that our approach has potential to outperform explicit conformance checkers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
