What Do Message Sequence Charts Mean
Peter Bernard Ladkin, Stefan Leue · KOPS (University of Konstanz) · 1994
We propose a semantics for Message Sequence Charts (MSCs). Our requirements are: to determine unambiguously which execution traces are allowed by an MSC; and to use a finite-state interpretation. Our semantics handles both synchronous and asynchronous communication. We define a global state automaton from an MSC, by first defining a transition system of global states, and from that a Buchi automaton. In using MSCs, properties of the environment and liveness properties of the MSC itself may be underspecified. We propose a method using temporal logic formulas to specify the required liveness properties.