Skip to main content
SpringerLink
Log in
SpringerLink
Log in

A Tutorial on Uppaal

  • Chapter
Formal Methods for the Design of Real-Time Systems (SFM-RT 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3185))

Included in the following conference series:

Abstract

This is a tutorial paper on the tool Uppaal. Its goal is to be a short introduction on the flavor of timed automata implemented in the tool, to present its interface, and to explain how to use the tool. The contribution of the paper is to provide reference examples and modeling patterns.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoretical Computer Science 1-3(300), 411–475 (2003)

    Article  Google Scholar 

  2. Aceto, L., Burgueño, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 263–280. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for realtime systems. In: 5th Symposium on Logic in Computer Science (LICS 1990), pp. 414–425 (1990)

    Google Scholar 

  4. Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  5. Amnell, T., Behrmann, G., Bengtsson, J., D’Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., Möller, M.O., Pettersson, P., Weise, C., Yi, W.: Uppaal - Now, Next, and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 100–125. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times – a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 460–464. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Balarin, F.: Approximate reachability analysis of timed automata. In: 17th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, Los Alamitos (1996)

    Google Scholar 

  8. Behrmann, G.: Data Structures and Algorithms for the Analysis of Real Time Systems. PhD thesis, Aalborg University (2003)

    Google Scholar 

  9. Behrmann, G.: Distributed reachability analysis in timed automata. Software Tool For Technology Transfer (STTT), Currently available in the Online First edition of STTT (2004)

    Google Scholar 

  10. Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: Proc. of 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (2002)

    Google Scholar 

  11. Behrmann, G., David, A., Larsen, K.G., Möller, M.O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. of 40th IEEE Conference on Decision and Control, IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  12. Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 225–229. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. G. Behrmann, A. Fehnker, T. Hune, K.G. Larsen, P. Pettersson, J. Romijn, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Behrmann, G., Hune, T., Vaandrager, F.: Distributed timed model checking - How the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Bengtsson, J.: Clocks, DBMs and States in Timed Systems. PhD thesis, Uppsala University (2002)

    Google Scholar 

  18. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Proceedings of the 9th International Conference on Concurrency Theory (September 1998)

    Google Scholar 

  19. Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Wang, Y., Weise, C.: New generation of uppaal. In: Int. Workshop on Software Tools for Technology Transfer (June 1998)

    Google Scholar 

  20. Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  21. Bowman, H., Faconti, G.P., Katoen, J.-P., Latella, D., Massink, M.: Automatic verification of a lip synchronisation algorithm using uppaal. In: Groote, B.L.J.F., van Wamel, J. (eds.) Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems, Amsterdam, The Netherlands (1998)

    Google Scholar 

  22. D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. David, A.: Hierarchical Modeling and Analysis of Timed Systems. PhD thesis, Uppsala University (November 2003)

    Google Scholar 

  24. David, A., Behrmann, G., Larsen, K.G., Yi, W.: New uppaal architecture. In: Pettersson, P., Yi, W. (eds.) Workshop on Real-Time Tools. Uppsala University Technical Report Series (2002)

    Google Scholar 

  25. David, A., Behrmann, G., Larsen, K.G., Yi, W.: A tool architecture for the next generation of uppaal. In: 10th Anniversary Colloquium. Formal Methods at the Cross Roads: From Panacea to Foundational Support. LNCS (2003)

    Google Scholar 

  26. David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  27. David, A., Yi, W.: Modelling and analysis of a commercial field bus protocol. In: Proceedings of the 12th Euromicro Conference on Real Time Systems, pp. 165–172. IEEE Computer Society, Los Alamitos (2000)

    Chapter  Google Scholar 

  28. Fersman, E.: A Generic Approach to Schedulability Analysis of Real-Time Systems. PhD thesis, Uppsala University (November 2003)

    Google Scholar 

  29. Havelund, K., Larsen, K.G., Skou, A.: Formal verification of a power controller using the real-time model checker uppaal. In: 5th International AMAST Workshop on Real-Time and Probabilistic Systems (1999), available at http://www.uppaal.com

  30. Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal. In: Proceedings of the 18th IEEE Real-Time Systems Symposium, December 1997, pp. 2–13 (1997)

    Google Scholar 

  31. Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  32. Hendriks, M., Larsen, K.G.: Exact acceleration of real-time model checking. In: Asarin, E., Maler, O., Yovine, S. (eds.) Electronic Notes in Theoretical Computer Science, April 2002, vol. 65, Elsevier Science Publishers, Amsterdam (2002)

    Google Scholar 

  33. Henzinger, T.A.: Symbolic model checking for real-time systems. Information and Computatio 111, 193–244 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  34. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)

    Google Scholar 

  35. Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design 13, 289–307 (1998)

    Article  Google Scholar 

  36. Hopcroft, J.E., Ullman, J.D.: Introduction of Automata Theory, Languages, and Computation. Addison-Wesley, Reading (2001)

    Google Scholar 

  37. Hune, T., Larsen, K.G., Pettersson, P.: Guided synthesis of control programs using uppaal. In: Lai, T.H. (ed.) Proc. of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation, April 2000, pp. E15–E22. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  38. Iversen, T.K., Kristoffersen, K.J., Larsen, K.G., Laursen, M., Madsen, R.G., Mortensen, S.K., Pettersson, P., Thomasen, C.B.: Modelchecking real-time control programs – Verifying LEGO mindstorms systems using uppaal. In: Proc. of 12th Euromicro Conference on Real-Time Systems, June 2000, pp. 147–155. IEEE Computer Society Press, Los Alamitos (2000)

    Chapter  Google Scholar 

  39. Jensen, H.E.: Abstraction-Based Verification of Distributed Systems. PhD thesis, Aalborg University (June 1999)

    Google Scholar 

  40. Jensen, H.E., Larsen, K.G., Skou, A.: Scaling up uppaal automatic verification of real-time systems using compositionality and abstraction. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 19–20. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  41. Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking (1999), http://www.it-c.dk/people/hra/mcpa/katoen.ps

  42. Skou, A., Havelund, K., Larsen, K.G.: Formal verification of a power controller using the real-time model checker Uppaal. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 277–298. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  43. Kristoffersen, K.J.: Compositional Verification of Concurrent Systems. PhD thesis, Aalborg University (August 1998), http://www.itu.dk/people/kjk/publications.html

  44. Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  45. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)

    Article  MATH  Google Scholar 

  46. Larsson, F., Larsen, K.G., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structures and state-space reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, December 1997, pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  47. Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gearbox controller. Springer International Journal of Software Tools for Technology Transfer (STTT) 3(3), 353–368 (2001)

    MATH  Google Scholar 

  48. Lönn, H., Pettersson, P.: Formal verification of a TDMA protocol startup mechanism. In: Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, December 1997, pp. 235–242 (1997)

    Google Scholar 

  49. Nielsen, B.: Specification and Test of Real-Time Systems. PhD thesis, Aalborg University (2000)

    Google Scholar 

  50. Pettersson, P.: Modelling and Verification of Real-time Systems Using Timed Automata: Theory and Practice. PhD thesis, Uppsala University (1999)

    Google Scholar 

  51. Yi, W., Petterson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Seventh International Conference on Formal Description Techniques, pp. 223–238 (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Denmark

    Gerd Behrmann, Alexandre David & Kim G. Larsen

Authors
  1. Gerd Behrmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandre David
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Istituto di Scienze e Tecnologie dell’Informazione, Università di Urbino “Carlo Bo”, Italy

    Marco Bernardo

  2. Dipartimento di Matematica ed Informatica, University of Camerino, Via Madonna delle Carceri 9, 62032, Camerino, Italy

    Flavio Corradini

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Behrmann, G., David, A., Larsen, K.G. (2004). A Tutorial on Uppaal . In: Bernardo, M., Corradini, F. (eds) Formal Methods for the Design of Real-Time Systems. SFM-RT 2004. Lecture Notes in Computer Science, vol 3185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30080-9_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30080-9_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23068-7

  • Online ISBN: 978-3-540-30080-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation