A Simple Trace Semantics for Asynchronous Sequence Diagrams

TL;DR

The paper tackles the lack of a rigorous yet accessible semantics for UML sequence diagrams by presenting a simple denotational framework for asynchronous diagrams based on regular-language theory. It separates lifeline interpretations into asynchronous semantics and handles core fragments—basic, loop, alt, par—along with lifeline creation and deletion, providing a compositional mapping from diagram constructs to sets of traces and lifeline namespaces. Key contributions include explicit trace-based semantics for weak sequential composition, interleaving, and iteration, plus a clear treatment of lifeline scope through create/destroy, and a discussion of extensions to synchronous interactions and additional fragments. The approach aims to clarify meaning for practitioners while laying groundwork for tool support and future work on synchronous semantics, operational guidance, and refinement relations between diagrams.

Abstract

Sequence diagrams are a popular technique for describing interactions between software entities. However, because the OMG group's UML standard is not based on a rigorous mathematical structure, it is impossible to deduce a single interpretation for the notation's semantics, nor to understand precisely how its different fragments interact. While there are a lot of suggested semantics in the literature, they are too mathematically demanding for the majority of software engineers, and often incomplete, especially in dealing with the semantics of lifeline creation and deletion. In this work we describe a simple semantics based on the theory of regular languages, a mathematical theory that is a standard part of the curriculum in every computer science undergraduate degree and covers all the major compositional fragments, and the creation and deletion of lifelines.

Figures (12)

• Figure 1: Abstract syntax for asynchronous sequence diagrams. The $+$ sign indicates a sequence of one or more entities.
• Figure 2: A simple asynchronous sequence diagram. It represents three traces, according to the possible positions of $m_3$ (either before $m_1$, between $m_1$ and $m_2$, or after $m_2$).
• Figure 3: An alternative fragment. Process $A$ may send either message $m1$ or $m2$ to process $B$ depending on the value of the boolean expression $P$. Afterwards $A$ sends $m3$ to $C$.
• Figure 4: A parallel combined fragment. The coordinator may invite the participants in any order. However, each participant accepts only after they have been invited.
• Figure 5: Asynchronous loop

Theorems & Definitions (2)

• theorem 1
• proof