Message sequence charts (MSCs) are used in the design phase of a distributed system to record desired system behaviors. They serve as informal documentation of design requirements that are referred to throughout the design process and even in the final system integration and acceptance testing. We show that message sequence charts are open to a variety of semantic interpretations. The meaning of an MSC can depend on, for instance, whether one allows or denies the possibility of message loss or message overtaking, and on the particulars of the message queuing policy to be adopted.
We describe an analysis tool that can perform automatic checks on message sequence charts and can alert the user to the existence of subtle design errors, for any predefined or user-specified semantic interpretation of the chart. The tool can also be used to specify time constraints on message delays, and can then return useful additional timing information, such as the minimum and the maximum possible delays between pairs of events.
Software Concepts and Tools 17(2):70-77, 1996. A preliminary version appeared in Proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1996), LNCS 1055, pp. 35-48.