Semantics and Simulation of Message Sequence Charts and Flow Graphs

Message Sequence Chart (MSC) is an ISO standard formal description technique for showing simple message flow in time between concurrent communicating processes. Informally, such devices are used everywhere in telecommunications, in text books and in software development, and are known by various other names such as Time Sequence Diagrams. The MSC standard is distinguished by a specific visual syntax. The semantics - the definition of what this pretty syntax means - is unfortunately somewhat further behind in its development.

In 1991-92, Peter Ladkin and Barbara Simons, then of IBM Almaden Research Center, showed how so-called loop processes, processes formed using sequential concatenation and the non-terminating loop operator as the only control structures (thus in particular no branching) could be analysed for deadlock, using simple but apparently powerful combinatorial techniques. The idea was to join corresponding send/receive statements in processes with an edge, thereby creating a graph whose edges were either next-statement edges within a process, or message-exchange edges between processes. It turns out that if the system does not deadlock, suitable unwinding of the infinite loops allows division of the graph into two: `preamble' nodes (message exchanges before an occurrence of the loop structure command) are connected only with preamble nodes; loop-internal nodes are connected only with loop-internal nodes; and each node is connected with precisely one other node in some other process. This was called the Message Flow Graph (MFG), and is mathematically very similar to an MSC with loops. If on the contrary the system does deadlock, a cycle (containing within-process edges and message-exchange edges) exists and is detected.

This work is described in the monograph Static Analysis of Communicating Processes.

In 1992, Ladkin and Stefan Leue (of the University of Waterloo, then of the Universität Bern) gave a semantics for MFGs based on the graph of transitions between global states of the system - the Global State Transition Graph (GSTG). This semantics preceded and subsumed the `official' MSC semantics developed by the ITC standardisation committee, in particular it gave meaning to certain kinds of MSCs with loops. We observed certain problems determining the meaning of infinite MSCs, namely that it was not determined, nor was it intuitively obvious, whether certain infinite traces were allowed or prohibited by the MSC. We also observed that certain branching behavior meant that the Büchi termination condition for automata was insufficient to determine trace acceptance/rejection when the underlying state graph was the GSTG. We suggested using annotations in Manna-Pnueli-style temporal logic to disambiguate the MSCs.

This work was written up in the paper Interpreting Message Flow Graphs.

Subsequently, Ladkin and Leue investigated the automatic analyis of MFGs and MSCs by translating them into Promela specifications and using the XSpin analysis tool from Lucent Bell Laboratories. This work justified Ladkin and Leue's published concerns (in the FORTE '94 Conference) concerning the incoherence of some aspects of MSC meaning by demonstrating the problems, as well as allowing a reasonable way for MSC writers to check the coherence of their MSCs.

This work appeared in Implementing and Verifying Message Sequence Chart Specifications Using Promela/XSpin.

Further publications on MSC topics from Ladkin and Leue may be found in the section Formal Definition of Message Sequence Charts of Ladkin's publications page. Stefan Leue's page on Research on Message Sequence Charts and Message Flow Graphs.

Further publications on deadlock analysis using MFGs by Ladkin and Simons may be found in the section Analysis of Communication in Parallel and Distributed Environments of Ladkin's publications page.