Conformance Testing for Timed Recursive Programs

  • Hana M’HemdiEmail author
  • Jacques Julliand
  • Pierre-Alain Masson
  • Riadh Robbana
Conference paper
Part of the Studies in Computational Intelligence book series (SCI, volume 614)


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.


Timed automata Timed pushdown automata Conformance testing Approximated determinization Analog-clock testing Reachability automaton 


  1. 1.
    Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: LICS, pp. 35–44 (2012)Google Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)zbMATHMathSciNetGoogle Scholar
  3. 3.
    Autebert, J.M., Berstel, J., Boasson, L.: Context-free languages and pushdown automata. In: Handbook of Formal Languages, vol. 1, pp. 111–174. Springer (1997)Google Scholar
  4. 4.
    Benerecetti, M., Minopoli, S., Peron, A.: Analysis of timed recursive state machines. In: TIME 2010, pp. 61–68. IEEE (2010)Google Scholar
  5. 5.
    Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. Hybrid Systems II, LNCS, vol. 999, pp. 64–85. Springer, Berlin (1995)CrossRefGoogle Scholar
  6. 6.
    Cassez, F., Jessen, J.J., Larsen, K.G., Raskin, J.F., Reynier, P.A.: Automatic synthesis of robust and optimal controllers—an industrial case study. In: HSCC’09, pp. 90–104. Springer (2009)Google Scholar
  7. 7.
    Chadha, R., Legay, A., Prabhakar, P., Viswanathan, M.: Complexity bounds for the verification of real-time software. In: VMCAI’10. LNCS, vol. 5944, pp. 95–111. Springer (2010)Google Scholar
  8. 8.
    de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS. LNCS, vol. 4963, pp. 337–340 (2008)Google Scholar
  9. 9.
    Dreyfus, A., Héam, P.C., Kouchnarenko, O., Masson, C.: A random testing approach using pushdown automata. STVR 24(8), 656–683 (2014)Google Scholar
  10. 10.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems (ext. abs.). In: Infinity. ENTCS, vol. 9, pp. 27–37 (1997)Google Scholar
  11. 11.
    Godefroid, P.: Test generation using symbolic execution. In: IARCS, pp. 24–33 (2012)Google Scholar
  12. 12.
    Krichen, M., Tripakis, S.: Conformance testing for real-time systems. FMSD 34(3), 238–304 (2009)zbMATHGoogle Scholar
  13. 13.
    Păsăreanu, C.S., Rungta, N., Visser, W.: Symbolic execution with mixed concrete-symbolic solving. In: ISSTA’11, pp. 34–44. ACM (2011)Google Scholar
  14. 14.
    Sénizergues, G.: L(a) = l(b)? decidability results from complete formal systems. In: ICALP. LNCS, vol. 2380, pp. 1–37. Springer (2002)Google Scholar
  15. 15.
    Tretmans, J.: Testing concurrent systems: a formal approach. In: Concurrency Theory. LNCS, vol. 1664, pp. 46–65. Springer (1999)Google Scholar
  16. 16.
    Trivedi, A., Wojtczak, D.: Recursive timed automata. In: ATVA’10, LNCS, vol. 6252, pp. 306–324. Springer (2010)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Hana M’Hemdi
    • 1
    • 2
    Email author
  • Jacques Julliand
    • 1
  • Pierre-Alain Masson
    • 1
  • Riadh Robbana
    • 3
  1. 1.FEMTO-ST/DISCUniversity of Franche-ComtéBesançonFrance
  2. 2.LIP2University of Tunis El ManarTunisTunisia
  3. 3.LIP2 and INSAT-University of CarthageTunisTunisia

Personalised recommendations