@article{Dam2005,
Author = {Damm, Werner and Josko, Bernhard and Pnueli, Amir and Votintseva, Angelika},
Title = {A discrete-time UML semantics for concurrency and communication in safety-critical applications},

Year = {2005},
Pages = {81-115},
Month = {01},
Editor = {Elsevier},
Publisher = {Elsevier},
Edition = {55},
Isbn = {0167-6423},
type = {article},
note = {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 syn},
Abstract = {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.}
}
@COMMENT{Bibtex file generated on }