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

n 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.