Reconstructing timed symbolic traces from rtioco -based timed test sequences using backward-induction

As of today, model-based testing is considered as a leading-edge technology in the IT industry. In model-based testing, an implementation under test is tested for compliance with a model that describes the required behaviour of the implementation. U ppaal T ron is a popular tool for online model-based conformance testing of real-time systems; it uses the U ppaal verification engine to generate and convert on-the-fly timed symbolic traces into concrete test sequences. Among the advantages of online testing is the reduction of the symbolic state space needed for computing traces, better addressing non-determinism, as well as the possibility to execute longer-lasting test runs. However, analysing and debugging long test runs can be tedious and time-consuming especially when analysing root causes of failed tests. In game theory, backward-induction is a process to reason backwards in time, from the end of a problem or situation, in order to determine a sequence of optimal actions. In this paper, we propose an approach to reconstruct symbolic traces from test sequences generated by U ppaal T ron using backward-induction. The resulting symbolic traces can be imported in the U ppaal tool and visualised in the U ppaal simulator. The evaluation of the implementation of the approach shows that it has the potential to satisfy the needs of industrial level testing.