Understanding UML: a formal semantics of concurrency and communication in real-time UML. (English) Zbl 1254.68140

de Boer, Frank S. (ed.) et al., Formal methods for components and objects. First international symposium, FMCO 2002, Leiden, The Netherlands, November 5–8, 2002. Revised lectures. Berlin: Springer (ISBN 3-540-20303-6/pbk). Lect. Notes Comput. Sci. 2852, 71-98 (2003).
Summary: 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 \in \text{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 [W. Damm and B. Westphal, ibid. 2852, 99–135 (2003; Zbl 1254.68148)].
For the entire collection see [Zbl 1028.00026].


68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


Zbl 1254.68148
Full Text: DOI