Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
9657461 | Science of Computer Programming | 2005 | 35 Pages |
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âkrtUML a symbolic transition system STS(M). We briefly 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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva,