A discrete-time UML semantics for concurrency and communication in safety-critical applications
Damm, Werner and Josko, Bernhard and Pnueli, Amir and Votintseva, Angelika
We define a subset krtUML of UML which is rich enough to express such modelling entities of UML, used in real-time applications, as active objects, dynamic object creation and destruction, dynamically changing communication topologies, combinations of synchronous and asynchronous communication, and shared memory usage through object attributes. We define a formal interleaving semantics for this kernel language by associating with each model M in krtUML a symbolic transition system STS(M). We shortly outline how to compile models of industrial systems making use of generalisation hierarchies, weak- and strong aggregation, and hierarchical state-machines into krtUML. The main aim of the paper is to provide an executable semantics for krtUML suitable for the formal verification of temporal model properties with existing model-checking tools.
01 / 2005
0167-6423
article
Elsevier
81-115
Elsevier
55
