@inproceedings{Dam2003,
Author = {Damm, Werner and Josko, Bernhard and Pnueli, Amir and Votintseva, Angelika},
Title = {Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML},

Year = {2003},
Pages = {71-98},
Month = {01},
Editor = {Springer Verlag},
Publisher = {Springer Verlag},
Series = {Lecture Notes in Computer Science 2852},
Isbn = {3-540-20303-6},
Booktitle = {Formal Methods for Components and Objects.  First International Symposium, FMCO 2002, Leiden, The Netherlands, November 5-8, 2002, Revised Lectures},
type = {inproceedings},
note = {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 communicatio},
Abstract = {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 [11].}
}
@COMMENT{Bibtex file generated on }