Coverage-Based Testing with Symbolic Transition Systems

We provide a model-based testing approach for systems comprising both state-transition based control flow, and data elements such as variables and data-dependent transitions. We propose test generation and execution, based on model-coverage: we generate test cases that aim to reach all transitions of the model. To obtain a test case reaching a certain transition, we need to combine reachability in the control flow, and satisfiability of the data elements of the model. Concrete values for data parameters are generated on-the-fly, i.e., during test execution, such that received outputs from the system can be taken into account for the inputs later provided in test execution. Due to undecidability of the satisfiability problem, SMT solvers may return result 'unknown'. Our algorithm deals with this explicitly. We implemented our method in Maude combined with Z3, and use this to demonstrate the applicability of our method on the Bounded Retransmission Protocol benchmark. We measure performance by counting the number of inputs and outputs needed to discover bugs in mutants, i.e., in non-conforming variants of the specification. As a result, we find that we perform 3 times better, according to the geometric mean, than when using random testing as implemented by the tool TorXakis.