Model-based mutation testing via symbolic refinement checking

B. K. Aichernig, E. Jöbstl, and S. Tiran

Abstract:

In model-based mutation testing, a test model is mutated for test case generation. The resulting test cases are able to detect whether the faults in the mutated models have been implemented in the system under test. For this purpose, a conformance check between the original and the mutated model is required. The generated counterexamples serve as basis for the test cases. Unfortunately, conformance checking is a hard problem and requires sophisticated verification techniques. Previous attempts using an explicit conformance checker suffered state space explosion. In this paper, we present several optimisations of a symbolic conformance checker using constraint solving techniques. The tool efficiently checks the refinement between non-deterministic test models. Compared to previous implementations, we could reduce our runtimes by 97%. In a new industrial case study, our optimisations can reduce the runtime from over 6 hours to less than 3 minutes

Reference: B. K. Aichernig, E. Jöbstl, and S. Tiran. Model-based mutation testing via symbolic refinement checking. Science of Computer Programming, 97, Part 4(0):383-404, 2015. Special Issue: Selected Papers from the 12th International Conference on Quality Software (QSIC 2012).