Understanding UML: A formal semantics of concurrency and communication in real-time UML

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 epsilon 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].