Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Approaches to Software Testing

FATES 2004: Formal Approaches to Software Testing pp 79–94Cite as

Online Testing of Real-time Systems Using Uppaal

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3395))

Abstract

We present T-Uppaal — a new tool for online black-box testing of real-time embedded systems from non-deterministic timed automata specifications. We describe a sound and complete randomized online testing algorithm and how to implement it using symbolic state representation and manipulation techniques. We propose the notion of relativized timed input/output conformance as the formal implementation relation. A novelty of this relation and our testing algorithm is that they explicitly take environment assumptions into account, generate, execute and verify the result online using the Uppaal on-the-fly model-checking tool engine. A medium size case study shows promising results in terms of error detection capability and computation performance.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111(2), 193–244 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: A simple experiment. In: 12th Int. Workshop on Testing of Communicating Systems, pp. 179–196 (1999)

    Google Scholar 

  5. Blom, J., Hessel, A., Jonsson, B., Pettersson, P.: Specifying and generating test cases using observer automata. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)

    Google Scholar 

  6. Braberman, V., Felder, M., Marré, M.: Testing Timing Behaviors of Real Time Software. In: Quality Week 1997, San Francisco, USA, April-May 1997, pp. 143–155 (1997)

    Google Scholar 

  7. Brinksma, E., Larsen, K.G., Nielsen, B., Tretmans, J.: Systematic Testing of Realtime Embedded Software Systems (STRESS), Research proposal submitted and accepted by the Dutch Research Council (March 2002)

    Google Scholar 

  8. Briones, L.B., Brinksma, E.: A test generation framework for quiescent real-time systems. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)

    Google Scholar 

  9. Cardell-Oliver, R.: Conformance Testing of Real-Time Systems with Timed Automata. Formal Aspects of Computing 12(5), 350–371 (2000)

    Article  MATH  Google Scholar 

  10. Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing 5, 1–20 (1993)

    Article  MATH  Google Scholar 

  11. En-Nouaary, A., Dssouli, R., Khendek, F., Elqortobi, A.: Timed Test Cases Generation Based on State Characterization Technique. In: 19th IEEE Real-Time Systems Symposium (RTSS 1998), December 2-4, pp. 220–229 (1998)

    Google Scholar 

  12. Frantzen, L., Tretmans, J., Willemse, T.: Test generation based on symbolic specifications. In: Formal Approaches to Testing of Software, Linz, Austria, September 21. LNCS. Springer, Heidelberg (2004)

    Google Scholar 

  13. Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-Optimal Test Cases for Real-Time Systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114–130. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Higashino, T., Nakata, A., Taniguchi, K., Cavalli, A.R.: Generating test cases for a timed i/o automaton model. In: IFIP Int’l Work. Test. Communicat. Syst., pp. 197–214 (1999)

    Google Scholar 

  15. Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 327–341. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, June 2003, pp. 198–207. IEEE Computer Society, Los Alamitos (2003)

    Google Scholar 

  17. Jéron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 108–121. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  18. Khoumsi, A., Jéron, T., Marchand, H.: Test cases generation for nondeterministic real-time systems. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 131–146. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Larsen, K.G.: A Context Dependent Equivalence Between Processes. Theoretical Computer Science 49, 185–215 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  20. Krichen, M., Tripakis, S.: Black-Box Conformance Testing for Real-Time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Mandrioli, D., Morasca, S., Morzenti, A.: Generating Test Cases for Real-Time Systems from Logic Specifications. ACM Transactions on Computer Systems 13(4), 365–398 (1995)

    Article  Google Scholar 

  22. Mikucionis, M., Larsen, K.G., Nielsen, B.: Online on-the-fly testing of real-time systems. Technical Report RS-03-49, Basic Researc. In: Computer Science (BRICS) (December 2003)

    Google Scholar 

  23. Mikucionis, M., Nielsen, B., Larsen, K.G.: Real-time system testing on-the-fly. In: The 15th Nordic Workshop on Programming Theory, Turku, Finland, October 29-31, 2003, vol. 34(B), pp. 36–38 (2003); Åbo Akademi, Department of Computer Science, Finland (Abstracts)

    Google Scholar 

  24. Mikucionis, M., Sasnauskaite, E.: On-the-fly testing using UppAal. Master’s thesis, Department of Computer Science, Aalborg University, Denmark (June 2003)

    Google Scholar 

  25. Nielsen, B., Skou, A.: Automated Test Generation from Timed Automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 343–357. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Peleska, J., Amthor, P., Dick, S., Meyer, O., Siegel, M., Zahlten, C.: Testing Reactive Real-Time Systems. In: Material for the School – 5th International School and Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1998), Lyngby, Denmark (1998)

    Google Scholar 

  27. Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 205. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing Timed Automata. Theoretical Computer Science 254(1-2), 225–257 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  29. Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  30. Tretmans, J.: Testing concurrent systems: A formal approach. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 46–65. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  31. Tretmans, J., Belinfante, A.: Automatic testing with formal methods. In: EuroSTAR 1999: 7th European Int. Conference on Software Testing, Analysis & Review. EuroStar Conferences, Barcelona, Spain, Galway, Ireland, November 8-12 (1999)

    Google Scholar 

  32. Diekert, V., Gastin, P., Petit, A.: Removing epsilon-Transitions in Timed Automata. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 583–594. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  33. de Vries, R., Tretmans, J., Belinfante, A., Feenstra, J., Feijs, L., Mauw, S., Goga, N., Heerink, L., de Heer, A.: Côte de resyste in Progress. In: STW Technology Foundation (ed.) Progress 2000 – Workshop on Embedded Systems, Utrecht, The Netherlands, October 2000, pp. 141–148 (2000)

    Google Scholar 

  34. de Vries, R.G., Tretmans, J.: On-the-fly conformance testing using Spin. Software Tools for Technology Transfer 2(4), 382–393 (2000)

    Article  MATH  Google Scholar 

  35. Yi, W., Pettersson, P., Daniels, M.: Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In: Hogrefe, D., Leue, S. (eds.) Proc. of the 7th Int. Conf. on Formal Description Techniques, pp. 223–238. North Holland, Amsterdam (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Fredrik Bajers Vej 7B, 9220, Aalborg Øst, Denmark

    Kim G. Larsen, Marius Mikucionis & Brian Nielsen

Authors
  1. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marius Mikucionis
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Brian Nielsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Goettingen, Germany

    Jens Grabowski

  2. Department of Computer Science, Aalborg University, Fredrik Bajersvej 7E, DK-9220, Aalborg, Denmark

    Brian Nielsen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 IFIP International Federation for Information Processing

About this paper

Cite this paper

Larsen, K.G., Mikucionis, M., Nielsen, B. (2005). Online Testing of Real-time Systems Using Uppaal . In: Grabowski, J., Nielsen, B. (eds) Formal Approaches to Software Testing. FATES 2004. Lecture Notes in Computer Science, vol 3395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31848-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-31848-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25109-5

  • Online ISBN: 978-3-540-31848-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation