Abstract
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].
This research was partially supported by the German Research Council (DFG) within the priority program Integration of Specification Techniques with Engineering Applications under grant DA 206/7-3 and by the Information Society DG of the European Commission within the project IST-2001-33522 OMEGA (Correct Development of Real-Time Embedded Systems).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Telelogic AB. Telelogic Tau, 2003. http://www.telelogic.com/products/tau/index.cfm
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), http://www.cs.york.ac.uk/puml/mmf/AlvarezUML2001.pdf
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)
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 http://dblp.uni-trier.de
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), www.dcs.kcl.ac.uk/staff/tony/docs/MMLCalculus.ps
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 http://www.puml.org
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 http://www.puml.org
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), http://www.kettering.edu/~jhuggins/papers/uml2000.ps
Rational Software Corporation. Rational Rose Family (2003), http://www.rational.com/products/rose/index.jsp
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 http://www-omega.imag.fr/doc/d1000009_6/D112_KL.pdf
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)
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)
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)
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), http://www.cs.york.ac.uk/puml/papers/nfmw97.ps
Harel, D., Gery, E.: Executable Object Modeling with Statecharts. IEEE Computer 30(7), 31–42 (1997)
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)
I-Logix Inc. Rhapsody (2002), http://www.ilogix.com/products/rhapsody/index.cfm
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)
Kleppe, A., Warmer, J.: Unification of Static and Dynamic Semantics of UML (2001), http://www.klasse.nl/english/uml/unification-report.pdf
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)
Lilius, J., Paltor, I.P.: vUML: a Tool for Verifying UML Models. Turku Centre for Computer Science, Abo Akademi University, Finland. Technical Report
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)
Ober, I.: Harmonizing Design Languages with Object-Oriented Extensions and an Executable Semantics, PhD Thesis. Institut National Polytechnique de Toulouse, France (April 2001)
Object Management Group. UML 1.4 with Action Semantics, Final Adopted Specification, ptc/02-01-09 (January 2002), Available from http://www.kc.com/as_site/home.html
Object Management Group. UML Profile for Schedulability, Performance, and Time Specification, ptc/02-03-02 OMG Adopted Specification (March 2002), Available from http://cgi.omg.org/docs/ptc/02-03-02.pdf
Övergaard, G.: Formal Specification of Object-Oriented Meta-Modelling. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 193. Springer, Heidelberg (2000)
Övergaard, G.: Using the BOOM Framework for Formal Specification of the UML. In: Proceedings of Defining Precise Semantics for UML (2000)
Ö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)
Reggio, G., Astesiano, E., Choppy, C., Hußmann, H.: Analyzing UML Active Classes and Associated State Machines - A Lightweight Formal Approach. In: FEAS (2000), ftp://ftp.disi.unige.it/pub/person/ReggioG/Reggio99a.ps
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), ftp://ftp.disi.unige.it/pub/person/CerioliM/FASE2001.pdf
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Josko, B., Pnueli, A., Votintseva, A. (2003). Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2002. Lecture Notes in Computer Science, vol 2852. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39656-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-39656-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20303-2
Online ISBN: 978-3-540-39656-7
eBook Packages: Springer Book Archive