Towards generation of adaptive test cases from partial models of determinized timed automata

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.