Test Generation from Timed Pushdown Automata with Inputs and Outputs

International audienceWe consider in this paper the model of Timed Pushdown Automata with Inputs and Outputs (TPAIO), for which state reachability can only be solved in exponential time. We compute by means of a polynomial algorithm a reachability timed automaton (RTA), thus partial, of a TPAIO. When the algorithmis applied to untimed pushdown automata, the reachability is equivalent in both automata. But with the addition of clock constraints, reachability in the RTA is only a sufficient condition. To decide if a succession of timed transitions can be executed, we compute the backward closures of the clock constraints, and evaluate them by means of satisfiability decision procedures. Additionally, we compute a path table that relates a feasibletransition of the RTA to the corresponding path of the TPAIO. We accept the incompleteness of our method as a price to pay for efficiency. It can be used in test generation since testing is incomplete by nature. Test generation relies on unfolding the transitions of the reachability timed automaton thanks to the path table. Keywords: Timed Pushdown Automata; Reachability Timed Automata; Clock Constraints Backward Closure; Test Generationfrom Automata; Conformance Relation for TPAIO