Specification and Verification of Message Sequence Charts

The use of message sequence charts (MSCs) is popular in designing and documenting communication protocols. A recent surge of interest in MSCs has led to various algorithms for their automatic analysis, e.g., finding race conditions. In this paper we adopt a causality based temporal logic to specify properties of MSCs. This alleviates some problems that arise when specifying properties of MSCs using the traditional interleaving-based linear temporal logic: systems of MSCs are not necessarily finite state systems, leading to undecidability of LTL model checking. Even when dealing with finite state MSC systems, the set of linearizations can easily generate an exponential state space explosion. We provide an efficient model checking algorithm for systems of MSCs. Our construction models the fifo MSC systems using a restricted version of omega-automata with two successor relations. We implemented a model checking environment for MSCs as an extension to the SPIN model checking system.