Towards Generation of Adaptive Test Cases from Partial Models of Determinized Timed Automata

B. K. Aichernig and F. Lorber

Abstract:

The well-defined timed semantics of timed automata as specification models provide huge advantages for the verification and validation of real-time systems. Thus, timed automata have already been applied in many different areas, including model-based testing. Unfortunately, there is one drawback in using timed automata for test-case generation: if they contain non-determinism or silent transitions, the problem of language inclusion between timed automata becomes undecidable. In recent work, we developed and implemented a technique to determinize timed automata up to a certain depth k. The resulting timed automata are unfolded to directed acyclic graphs (DAGs) up to depth k. The unfolding caused an exponential state-space explosion. Consequently, our model-based test-case generation algorithm for deterministic timed automata, which uses language inclusion, did not scale anymore. Within this paper we investigate how to split the determinized DAGs into partial models, to overcome the problems caused by the increased state space and find effective ways to use the deterministic DAGs for model-based test case generation.

Reference: B. K. Aichernig and F. Lorber. Towards generation of adaptive test cases from partial models of determinized timed automata. In Proceedings of the 11th Workshop on Advances in Model Based Testing, A-MOST 2015, co-located with ICST 2015. IEEE Computer Society, 2015.