Accelerated model-based robustness testing of state machine implementations

In this paper, we present an approach for accelerating model-based robustness testing of state-based software components. We use the Z3 SAT solver to derive executable test cases fully automatically from a state model based on a UML Statechart. The test cases are paths along the Statechart comprising states and transitions. The main advantage of our approach is an accelerated execution of the test cases by refining already reached states as starting points for further test cases using reverse execution. Furthermore, the presented approach is able to check whether a correct target state has been reached or not when executing the path-based test cases using runtime verification and therefore increases the test significance. The runtime verification is done without instrumenting the source code of the component under test.