Damm, Werner and Josko, Bernhard and Pnueli, Amir and Votintseva, Angelika
Formal Methods for Components and Objects. First International Symposium, FMCO 2002, Leiden, The Netherlands, November 5-8, 2002, Revised Lectures
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 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 .