Does this fault lead to failure? Combining refinement and input-output conformance checking in fault-oriented test-case generation

In this paper we describe an advanced test-case generation technique that is implemented in our model-based test-case generator MoMuT::UML. The tool injects faults into a UML model and analyses if the faults propagate to the interface. If a fault does propagate to an observable failure, an explaining sequence of events is generated and converted into a test-case scenario. The faults are detected using a highly optimised refinement checker, their propagation is analysed with an input-output conformance (ioco) checker. We show that this combination is faster than pure input-output conformance checking. It has been used in a recent industrial application of testing automotive measurement devices. The refinement and ioco checker are implemented in Prolog using the SMT solver Z3.