Model Checking Timed UML State Machines and Collaborations

  • Alexander Knapp
  • Stephan Merz
  • Christopher Rauh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


We describe a prototype tool, HUGO/RT, that is designed to automatically verify whether the timed state machines in a UML model interact according to scenarios specified by time-annotated UML collaborations. Timed state machines are compiled into timed automata that exchange signals and operations via a network automaton. A collaboration with time constraints is translated into an observer timed automaton. The model checker UPPAAL is called upon to verify the timed automata representing the model against the observer timed automaton.


State Machine Model Check Critical Section Time Automaton Event Queue 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theo. Comp. Sci., 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Rodolphe Arthaud, Udo Brockmeyer, Werner Damm, Bruce P. Douglass, Francois Terrier, and Wang Yi, editors. Proc. Wsh. Formal Design Techniques for Real-Time UML, York, 2000.
  3. 3.
    Grady Booch, James Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, Reading, Mass., &c, 1998.Google Scholar
  4. 4.
    Werner Damm and David Harel. LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design, 19(1):45–80, 2001.zbMATHCrossRefGoogle Scholar
  5. 5.
    Werner Damm, Bernhard Josko, Hardi Hungar, and Amir Pnueli. A Compositional Real-Time Semantics of STATEMATE Designs. In Willem-Paul de Roever, Hans Langmaack, and Amir Pnueli, editors, Proc. Int. Symp. Compositionality (Revised Lectures), volume 1536 of Lect. Notes Comp. Sci., pages 186–238. Springer, Berlin, 1998.Google Scholar
  6. 6.
    Alexandre David and M. Oliver Möller. From HUppaal to Uppaal — A Translation from Hierarchical Timed Automata to Flat Timed Automata. Technical Report BRICS RS-01-11, Department of Computer Science, Aarhus Universitet, 2001.Google Scholar
  7. 7.
    Bruce P. Douglass. Real-Time UML. Addison-Wesley, Reading, Mass., &c., 1998.Google Scholar
  8. 8.
    Thomas Firley, Michaela Huhn, Karsten Diethers, Thomas Gehrke, and Ursula Goltz. Timed Sequence Diagrams and Tool-Based Analysis — A Case Study. In Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999 France and Rumpe [9], pages 645–660.Google Scholar
  9. 9.
    Robert B. France and Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999.Google Scholar
  10. 10.
    David Harel. Statecharts: A Visual Formalism for Complex Systems. Sci. Comp. Program., 8(3):231–274, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    David Harel and Eran Grey. Executable Object Modeling with Statecharts. Computer, July:31–42, 1997.Google Scholar
  12. 12.
    Constance L. Heitmeyer, Ralph D. Jeffords, and Bruce G. Labaw. Comparing Different Approaches for Specifying and Verifying Real-Time Systems. In Proc. 10 th IEEE Wsh. Real-Time Operating Systems and Software, pages 122–129, New York, 1993.Google Scholar
  13. 13.
    Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. Int. J. Softw. Tools for Techn. Transfer, 1(1–2):134–152, 1997.zbMATHCrossRefGoogle Scholar
  14. 14.
    Diego Latella, Istvan Majzik, and Mieke Massink. Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-Checker. Formal Aspects Comp., 11(6):637–664, 1999.zbMATHCrossRefGoogle Scholar
  15. 15.
    Luigi Lavazza, Gabriele Quaroni, and Matteo Venturelli. Combining UML and Formal Notations for Modelling Real-Time Systems. In 8 th Europ. Conf. Software Engineering, Wien, 2001.Google Scholar
  16. 16.
    Johan Lilius and Iván Porres Paltor. Formalising UML State Machines for Model Checking. In Bernhard Rumpe, editors. Proc. 2 nd Int. Conf. UML, volume 1723 of Lect. Notes Comp. Sci. Springer, Berlin, 1999 France and Rumpe [9], pages 430–445.Google Scholar
  17. 17.
    Darmalingum Muthiayen. Real-Time Reactive System Development — A Formal Approach Based on UML and PVS. PhD thesis, Concordia University, Montreal, Canada, 2000.Google Scholar
  18. 18.
    Object Management Group. Unified Modeling Language Specification, Version 1.4. Specification, OMG, 2001.
  19. 19.
    Timm Schäfer, Alexander Knapp, and Stephan Merz. Model Checking UML State Machines and Collaborations. In Scott Stoller and Willem Visser, editors, Proc. Wsh. Software Model Checking, volume 55(3) of Elect. Notes Theo. Comp. Sci., Paris, 2001. 13 pages.Google Scholar
  20. 20.
    Bran Selic, Garth Gullekson, and Paul T. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, New York, 1994.zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Alexander Knapp
    • 1
  • Stephan Merz
    • 1
  • Christopher Rauh
    • 2
  1. 1.Institut für InformatikLudwig-Maximilians-Universität MünchenGermany
  2. 2.Institut für InformatikTechnische Universität MünchenGermany

Personalised recommendations