Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML

  • Werner Damm
  • Bernhard Josko
  • Amir Pnueli
  • Angelika Votintseva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)


We define a subset krtUML of UML which is rich enough to express all behavioural modelling entities of UML used for real-time applications, covering such aspects as active objects, dynamic object creation and destruction, dynamically changing communication topologies in inter-object communication, asynchronous signal based communication, synchronous communication using operation calls, and shared memory communication through global attributes. We define a formal interleaving semantics for this kernel language by associating with each model M ∈ krtUML a symbolic transition system STS(M). We outline how to compile industrial real-time UML models making use of generalisation hierarchies, weak- and strong aggregation, and hierarchical state-machines into krtUML, and propose modelling guidelines for real-time applications of UML. This work provides the semantical foundation for formal verification of real-time UML models described in the companion paper [11].


Formal Semantic Active Object Abstract State Machine Passive Object Operation Call 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Telelogic AB. Telelogic Tau, 2003. Google Scholar
  2. 2.
    Alvarez, J.M., Clark, T., Evans, A., Sammut, P.: An Action Semantics for MML. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, p. 2. Springer, Heidelberg (2001), CrossRefGoogle Scholar
  3. 3.
    Börger, E., Cavarra, A., Riccobene, E.: An ASM Semantics for UML Activity Diagrams. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 293–308. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Börger, E., Cavarra, A., Riccobene, E.: Modeling the Dynamics of UML State Machines. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 223–241. Springer, Heidelberg (2000), DBLP CrossRefGoogle Scholar
  5. 5.
    Clark, T., Evans, A., Kent, S.: The Metamodelling Language Calculus: Foundation Semantics for UML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 17–31. Springer, Heidelberg (2001), CrossRefGoogle Scholar
  6. 6.
    Clark, T., Evans, A., Kent, S., Brodsky, S., Cook, S.: A Feasibility Study in Rearchitecting UML as a Family of Languages Using a Precise OO Meta-Modelling Approach, version 1.0 (September 2000), Available from
  7. 7.
    Clark, T., Evans, A., Kent, S., Sammut, P.: The MMF Approach to Engineering Object-Oriented Design Languages. In: Proc. Workshop on Language Descriptions, Tools and Applications, LDTA 2001 (2001), Available via
  8. 8.
    Compton, K., Huggins, J., Shen, W.: A Semantic Model for the State Machine in the UML. In: Reggio, G., Knapp, A., Rumpe, B., Selic, B., Wieringa, R. (eds.) Dynamic Behaviour in UML Models: Semantic Questions, Workshop Proceedings, UML 2000 Workshop, Bericht 0006, October 2000. Ludwig-Maximilians-Universität München, Institut für Informatik, pp. 25–31 (2000),
  9. 9.
    Rational Software Corporation. Rational Rose Family (2003),
  10. 10.
    Damm, W., Josko, B., Pnueli, A., Votintseva, A.: A Formal Semantics for a UML Kernel Language. Omega Technical report, part 1 of the deliverable D1.1.2, Project IST-2001-33522 OMEGA (January 2003), Available from
  11. 11.
    Damm, W., Westphal, B.: Live and Let Die: LSC-based Verification of UMLModels. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 99–135. Springer, Heidelberg (2003) (to appear)CrossRefGoogle Scholar
  12. 12.
    Engels, G., Hausmann, J.H., Heckel, R., Sauer, S.: Dynamic Meta Modeling: A Graphical Approach to the Operational Semantics of Behavioral Diagrams in UML. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol. 1939, pp. 323–337. Springer, Heidelberg (2000)Google Scholar
  13. 13.
    Evans, R., France, K.: Lano, and B. Rumpe. The UML as a Formal Modeling Notation. In: The Unifed Modeling Language: the first international workshop. Springer, Heidelberg (June 1998)Google Scholar
  14. 14.
    Evans, A.S., Clark, A.N.: Foundations of the Unified Modeling Language. In: 2nd Northern Formal Methods Workshop, Ilkley, electronic Workshops in Computing. Springer, Heidelberg (1998), Google Scholar
  15. 15.
    Harel, D., Gery, E.: Executable Object Modeling with Statecharts. IEEE Computer 30(7), 31–42 (1997)Google Scholar
  16. 16.
    Hußmann, H.: Loose Semantics for UML, OCL. In: Proceedings 6th World Conference on Integrated Design and Process Technology (IDPT 2002). Society for Design and Process Science (June 2002)Google Scholar
  17. 17.
  18. 18.
    Kim, S.-K., Carrington, D.: Formalizing the UML Class Diagrams Using Object- Z. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 83–98. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  19. 19.
    Kleppe, A., Warmer, J.: Unification of Static and Dynamic Semantics of UML (2001),
  20. 20.
    Kwon, G.: Rewrite Rules and Operational Semantics for Model Checking UML Statcharts. In: Evans, A., Kent, S., Selic, B. (eds.) UML 2000. LNCS, vol. 1939, pp. 528–540. Springer, Heidelberg (2000)Google Scholar
  21. 21.
    Lilius, J., Paltor, I.P.: vUML: a Tool for Verifying UML Models. Turku Centre for Computer Science, Abo Akademi University, Finland. Technical ReportGoogle Scholar
  22. 22.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)zbMATHGoogle Scholar
  23. 23.
    Ober, I.: Harmonizing Design Languages with Object-Oriented Extensions and an Executable Semantics, PhD Thesis. Institut National Polytechnique de Toulouse, France (April 2001)Google Scholar
  24. 24.
    Object Management Group. UML 1.4 with Action Semantics, Final Adopted Specification, ptc/02-01-09 (January 2002), Available from
  25. 25.
    Object Management Group. UML Profile for Schedulability, Performance, and Time Specification, ptc/02-03-02 OMG Adopted Specification (March 2002), Available from
  26. 26.
    Övergaard, G.: Formal Specification of Object-Oriented Meta-Modelling. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 193. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  27. 27.
    Övergaard, G.: Using the BOOM Framework for Formal Specification of the UML. In: Proceedings of Defining Precise Semantics for UML (2000)Google Scholar
  28. 28.
    Övergaard, G., Palmkvist, K.: A Formal Approach to Use Cases and Their Relationships. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618, pp. 406–418. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  29. 29.
    Reggio, G., Astesiano, E., Choppy, C., Hußmann, H.: Analyzing UML Active Classes and Associated State Machines - A Lightweight Formal Approach. In: FEAS (2000),
  30. 30.
    Reggio, G., Cerioli, M., Astesiano, E.: Towards a Rigorous Semantics of UML Supporting Its Multiview Approach. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, p. 171. Springer, Heidelberg (2001), CrossRefGoogle Scholar
  31. 31.
    Richters, M., Gogolla, M.: On Formalizing the UML Object Constraint Language OCL. In: Ling, T.-W., Ram, S., Li Lee, M. (eds.) ER 1998. LNCS, vol. 1507, pp. 449–464. Springer, Heidelberg (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Werner Damm
    • 1
  • Bernhard Josko
    • 1
  • Amir Pnueli
    • 2
  • Angelika Votintseva
    • 1
  1. 1.OFFISOldenburgGermany
  2. 2.The Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations