Conformance Testing for Timed Recursive Programs

This paper is about conformance testing of timed pushdown automata with inputs and outputs (TPAIO), that specify both stack and clock constraints. TPAIO are used as a model for timed recursive programs. This paper proposes a novel method of off-line test generation from deterministic TPAIO. In this context, a first problem is to resolve the clock constraints. It is solved by computing a deterministic timed pushdown tester with inputs and outputs (TPTIO), that is a TPAIO with only one clock, and provided with a location fail. To generate test cases from a TPTIO, we compute from it a finite reachability automaton (RA), that relates any of its transitions to a path of the TPTIO. The RA computation takes the TPTIO transitions as a coverage criterion. The transitions of the RA, thus the paths of the TPTIO are used for generating test cases that aim at covering the reachable locations and transitions of the TPAIO.