×

zbMATH — the first resource for mathematics

Conformance testing for real-time systems. (English) Zbl 1180.68072
Summary: 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.

MSC:
68M15 Reliability, testing and fault tolerance of networks and computer systems
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Uppaal; STG; Kronos
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126:183–235 · Zbl 0803.68071
[2] Alur R, Fix L, Henzinger T (1994) A determinizable class of timed automata. In: CAV’94. LNCS, vol 818. Springer, Berlin · Zbl 0912.68132
[3] 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
[4] 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
[5] 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
[6] 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 · Zbl 0930.68077
[7] Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. IFIP Congr Ser 9:41–46
[8] 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 · Zbl 1081.68566
[9] Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality. LNCS, vol 1536. Springer, Berlin
[10] Bouyer P (2004) Forward analysis of updatable timed automata. Formal Methods in System Design 24(3):281–320 · Zbl 1073.68041
[11] Bouyer P, Chevalier F, D’Souza D (2005) Fault diagnosis using timed automata. In: FoSSaCS’05. LNCS, vol 3441. Springer, Berlin, pp 219–233 · Zbl 1118.68374
[12] 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 · Zbl 0974.68556
[13] 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
[14] Braberman V, Felder M, Marre M (1997) Testing timing behavior of real-time software. In: International software quality week
[15] 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 · Zbl 1078.68665
[16] Brinksma E, Tretmans J (2001) Testing transition systems: an annotated bibliography. In: MOVEP 2000. LNCS, vol 2067. Springer, Berlin · Zbl 0985.68661
[17] Briones L, Brinksma E (2004) A test generation framework for quiescent real-time systems. In: FATES’04. LNCS, vol 3395. Springer, Berlin · Zbl 1081.68569
[18] Cardell-Oliver R (2002) Conformance test experiments for distributed real-time systems. In: ISSTA’02. ACM, New York
[19] Chow TS (1978) Testing software design modeled by finite-state machines. IEEE Trans Softw Eng 4(1) · Zbl 0379.68039
[20] Clarke D, Jéron T, Rusu V, Zinovieva E (2002) STG: a symbolic test generation tool. In: TACAS’02. LNCS, vol 2280. Springer, Berlin · Zbl 1043.68546
[21] 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)
[22] 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
[23] 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
[24] 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
[25] 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
[26] 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
[27] Groote JF, van de Pol J (1996) A bounded retransmission protocol for large data packets. In: Algebraic methodology and software technology, pp 536–550
[28] Henzinger T, Manna Z, Pnueli A (1992) What good are digital clocks? In: ICALP’92. LNCS, vol 623. Springer, Berlin
[29] Hessel A, Larsen K, Nielsen B, Pettersson P, Skou A (2003) Time-optimal real-time test case generation using UPPAAL. In: FATES’03 · Zbl 1185.68248
[30] 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
[31] 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
[32] Jard C, Jéron T, Morel P (2000) Verification of test suites. In: TestCom 2000
[33] Khoumsi A, Jéron T, Marchand H (2003) Test cases generation for nondeterministic real-time systems. In: FATES’03 · Zbl 1185.68415
[34] 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 · Zbl 1125.68370
[35] 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 · Zbl 1109.68368
[36] 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
[37] 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 · Zbl 1109.68368
[38] Larsen K, Mikucionis M, Nielsen B (2004) Online testing of real-time systems using uppaal. In: FATES’04. LNCS, vol 3395. Springer, Berlin · Zbl 1081.68574
[39] 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
[40] Lee D, Yannakakis M (1996) Principles and methods of testing finite state machines–a survey. Proc IEEE 84:1090–1126
[41] Myers GJ (1979) The art of software testing. Wiley, New York
[42] Nielsen B, Skou A (2001) Automated test generation from timed automata. In: TACAS’01. LNCS, vol 2031. Springer, Berlin · Zbl 0978.68538
[43] Peleska J (2002) Formal methods for test automation–hard real-time testing of controllers for the airbus aircraft family. In: IDPT’02
[44] Puri A (2000) Dynamical properties of timed automata. Discrete Event Dyn Syst 10(1–2):87–113 · Zbl 0986.93042
[45] 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 · Zbl 1379.68240
[46] Springintveld J, Vaandrager F, D’Argenio P (2001) Testing timed automata. Theor Comput Sci 254 · Zbl 0972.68104
[47] Tretmans J (1999) Testing concurrent systems: a formal approach. In: CONCUR’99. LNCS, vol 1664. Springer, Berlin
[48] Tretmans J (2002) Testing techniques. Lecture notes. University of Twente, The Netherlands
[49] 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 · Zbl 1278.68140
[50] 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 · Zbl 1099.68648
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.