Abstract
We propose a new framework for black-box conformance testing of real-time systems. The framework is based on the model of partially-observable, non-deterministic timed automata. We argue that partial observability and non-determinism are essential features for ease of modeling, expressiveness and implementability. The framework allows the user to define, through appropriate modeling, assumptions on the environment of the system under test (SUT) as well as on the interface between the tester and the SUT. We consider two types of tests: analog-clock tests and digital-clock tests. Our algorithm for generating analog-clock tests is based on an on-the-fly determinization of the specification automaton during the execution of the test, which in turn relies on reachability computations. The latter can sometimes be costly, thus problematic, since the tester must quickly react to the actions of the system under test. Therefore, we provide techniques which allow analog-clock testers to be represented as deterministic timed automata, thus minimizing the reaction time to a simple state jump. We also provide algorithms for static or on-the-fly generation of digital-clock tests. These tests measure time only with finite-precision digital clocks, another essential condition for implementability. We also propose a technique for location, edge and state coverage of the specification, by reducing the problem to covering a symbolic reachability graph. This avoids having to generate too many tests. We report on a prototype tool called \(\mathsf{TTG}\) and two case studies: a lighting device and the Bounded Retransmission Protocol. Experimental results obtained by applying \(\mathsf{TTG}\) on the Bounded Retransmission Protocol show that only a few tests suffice to cover thousands of reachable symbolic states in the specification.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126:183–235
Alur R, Fix L, Henzinger T (1994) A determinizable class of timed automata. In: CAV’94. LNCS, vol 818. Springer, Berlin
Belinfante A, Feenstra J, de Vries RG, Tretmans J, Goga N, Feijs L, Mauw S, Heerink L (1999) Formal test automation: a simple experiment. In: 12th international workshop on testing of communicating systems. Kluwer, Dordrecht
Bengtsson J, Yi W (2003) On clock difference constraints and termination in reachability analysis of timed automata. In: ICFEM’03. LNCS, vol 2885. Springer, Berlin
Bensalem S, Bozga M, Krichen M, Tripakis S (2005) Testing conformance of real-time applications by automatic generation of observers. In: 4th international workshop on runtime verification (RV’04). ENTCS, vol 113. Elsevier, Amsterdam, pp 23–43
Berard B, Petit A, Diekert V, Gastin P (1998) Characterization of the expressive power of silent transitions in timed automata. Fund Inform 36(2–3):145–182
Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. IFIP Congr Ser 9:41–46
Blom J, Hessel A, Jonsson B, Pettersson P (2004) Specifying and generating test cases using observer automata. In: Proceedings of formal approaches to software testing, pp 125–139
Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality. LNCS, vol 1536. Springer, Berlin
Bouyer P (2004) Forward analysis of updatable timed automata. Formal Methods in System Design 24(3):281–320
Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: FoSSaCS’05. LNCS, vol 3441. Springer, Berlin, pp 219–233
Bozga M, Fernandez JC, Ghirvu L, Graf S, Krimm JP, Mounier L (2000) IF: a validation environment for timed asynchronous systems. In: Proc CAV’00. LNCS, vol 1855. Springer, Berlin
Bozga M, Graf S, Kerbrat A, Mounier L, Ober I, Vincent D (2000) SDL for real-time: what is missing? In: Proceedings of SAM’00: 2nd workshop on SDL and MSC, Grenoble, France, pp 108–122. IMAG, June 2000
Braberman V, Felder M, Marre M (1997) Testing timing behavior of real-time software. In: International software quality week
Brat G, Giannakopoulou D, Goldberg A, Havelund K, Lowry M, Pasareanu C, Venet A, Visser W (2003) Experimental evaluation of V&V tools on martian rover software. In: SEI software model checking workshop
Brinksma E, Tretmans J (2001) Testing transition systems: an annotated bibliography. In: MOVEP 2000. LNCS, vol 2067. Springer, Berlin
Briones L, Brinksma E (2004) A test generation framework for quiescent real-time systems. In: FATES’04. LNCS, vol 3395. Springer, Berlin
Cardell-Oliver R (2002) Conformance test experiments for distributed real-time systems. In: ISSTA’02. ACM, New York
Chow TS (1978) Testing software design modeled by finite-state machines. IEEE Trans Softw Eng 4(1)
Clarke D, Jéron T, Rusu V, Zinovieva E (2002) STG: a symbolic test generation tool. In: TACAS’02. LNCS, vol 2280. Springer, Berlin
Clarke D, Lee I (1997) Automatic generation of tests for timing constraints from requirements. In: 3rd workshop on object-oriented real-time dependable systems (WORDS’97)
Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool Kronos. In: Hybrid systems III, verification and control. LNCS, vol 1066. Springer, Berlin, pp 208–219
Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: Tools and algorithms for the construction and analysis of systems ’98, Lisbon, Portugal. LNCS, vol 1384. Springer, Berlin
Dill D (1989) Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J (ed) Automatic verification methods for finite state systems. LNCS, vol 407. Springer, Berlin, pp 197–212
En-Nouaary A, Dssouli R, Khendek F, Elqortobi A (1998) Timed test cases generation based on state characterization technique. In: RTSS’98. IEEE, New York
Fernandez JC, Jard C, Jéron T, Viho G (1996) Using on-the-fly verification techniques for the generation of test suites. In: CAV’96. LNCS, vol 1102. Springer, Berlin
Groote JF, van de Pol J (1996) A bounded retransmission protocol for large data packets. In: Algebraic methodology and software technology, pp 536–550
Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: ICALP’92. LNCS, vol 623. Springer, Berlin
Hessel A, Larsen K, Nielsen B, Pettersson P, Skou A (2003) Time-optimal real-time test case generation using UPPAAL. In: FATES’03
Higashino T, Nakata A, Taniguchi K, Cavalli A (1999) Generating test cases for a timed I/O automaton model. In: IFIP international workshop on testing of Communicating Systems. Kluwer, Dordrecht
ISO/IEC (1992) Open systems interconnection conformance testing methodology and framework—part 1: general concept; part 2: abstract test suite specification; part 3: the tree and tabular combined notation (TTCN). Technical Report 9646, International Organization for Standardization—Information Processing Systems—Open Systems Interconnection, Genève
Jard C, Jéron T, Morel P (2000) Verification of test suites. In: TestCom 2000
Khoumsi A, Jéron T, Marchand H (2003) Test cases generation for nondeterministic real-time systems. In: FATES’03
Krichen M, Tripakis S (2004) Black-box conformance testing for real-time systems. In: 11th international spin workshop on model checking of software (SPIN’04). LNCS, vol 2989. Springer, Berlin
Krichen M, Tripakis S (2004) Real-time testing with timed automata testers and coverage criteria. In: Formal techniques, modelling and analysis of timed and fault tolerant systems (FORMATS-FTRTFT’04). LNCS, vol 3253. Springer, Berlin
Krichen M, Tripakis S (2005) An expressive and implementable formal framework for testing real-time systems. In: The 17th IFIP international conference on testing of communicating systems (TestCom’05). LNCS, vol 3502. Springer, Berlin
Krichen M, Tripakis S (2005) State identification problems for timed automata. In: The 17th IFIP international conference on testing of communicating systems (TestCom’05). LNCS, vol 3502. Springer, Berlin
Larsen K, Mikucionis M, Nielsen B (2004) Online testing of real-time systems using uppaal. In: FATES’04. LNCS, vol 3395. Springer, Berlin
Larsen K, Mikucionis M, Nielsen B, Skou A (2005) Testing real-time embedded software using UPPAAL-TRON: an industrial case study. In: 5th ACM international conference on embedded software. ACM, New York, pp 299–306
Lee D, Yannakakis M (1996) Principles and methods of testing finite state machines—a survey. Proc IEEE 84:1090–1126
Myers GJ (1979) The art of software testing. Wiley, New York
Nielsen B, Skou A (2001) Automated test generation from timed automata. In: TACAS’01. LNCS, vol 2031. Springer, Berlin
Peleska J (2002) Formal methods for test automation—hard real-time testing of controllers for the airbus aircraft family. In: IDPT’02
Puri A (2000) Dynamical properties of timed automata. Discrete Event Dyn Syst 10(1–2):87–113
Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: 13th Annual symposium on theoretical aspects of computer science, STACS’96. LNCS, vol 1046. Springer, Berlin
Springintveld J, Vaandrager F, D’Argenio P (2001) Testing timed automata. Theor Comput Sci 254
Tretmans J (1999) Testing concurrent systems: a formal approach. In: CONCUR’99. LNCS, vol 1664. Springer, Berlin
Tretmans J (2002) Testing techniques. Lecture notes. University of Twente, The Netherlands
Tripakis S (2002) Fault diagnosis for timed automata. In: Formal techniques in real time and fault tolerant systems (FTRTFT’02). LNCS, vol 2469. Springer, Berlin
Tripakis S (2004) Folk theorems on the determinization and minimization of timed automata. In: Formal modeling and analysis of timed systems (FORMATS’03). LNCS, vol 2791. Springer, Berlin
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Krichen, M., Tripakis, S. Conformance testing for real-time systems. Form Methods Syst Des 34, 238–304 (2009). https://doi.org/10.1007/s10703-009-0065-1
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-009-0065-1