Extendable and modifiable operational semantics for UML 2.0 sequence diagrams

UML sequence diagrams is a specification language that has proved itself to be of great value in system development. When put to applications such as simulation, testing and other kinds of automated analysis there is a need for formal semantics. Such methods of analysis are by nature operational, and this motivates formalizing an operational semantics. We present an operational semantics for UML sequence diagrams, which we believe gives a solid starting point for developing methods for automated analysis. The operational semantics can be proved to be sound and complete with resect to to a denotational semantics for the same language. It handles negative behavior as well as potential and mandatory choice. We are not aware of any other operational semantics of this strength. UML sequence diagrams [5] and their predecessor Message Sequence Charts (MSC) [4] are specification languages that have proved themselves to be of great practical value in system development. When sequence diagrams are used t