Model-based mutation testing via symbolic refinement checking

• We deal with model- and mutation-based test case generation.
• The main focus lies on optimisations of the underlying conformance check.
• We explain the construction of test cases based on the conformance check.
• We allow for non-determinism in the test models.
• We demonstrate the effectiveness of our optimisations on industrial case studies.

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.