Safety-Liveness Semantics for UML 2.0 Sequence Diagrams

12 years 10 days ago
Safety-Liveness Semantics for UML 2.0 Sequence Diagrams
We provide an automata-theoretic solution to one of the main open questions about the UML standard, namely how to assign a formal semantics to a set of sequence diagrams without compromising refinement? Our solution relies on a rather obvious idea, but to our knowledge has not been used before in this context: that bad and good sequence diagrams in the UML standard should be regarded as safety and liveness properties, respectively. Proceeding in this manner, we obtain a semantics that essentially complements the set of behaviors associated with the set of sequence diagrams, thereby allowing us to use the standard notion of refinement as language inclusion. We show that refinement in this setting is compositional with respect to sequential composition, alternative composition, parallel composition, and star+ composition.
Radu Grosu, Scott A. Smolka
Added 24 Jun 2010
Updated 24 Jun 2010
Type Conference
Year 2005
Where ACSD
Authors Radu Grosu, Scott A. Smolka
Comments (0)