An Executable Specification Language Based on Message Sequence Charts

Abstract. Message Sequence Charts (MSCs) are an appealing visual formalism that play a useful role in the early design stages of reactive systems such as telecommunication protocols. They also constitute one of the behavioral diagram types in the UML framework [4]. MSCs are usually intended to capture system requirements. However there is no standard relationship between such requirements and an executable specification. Here we deploy MSCs instead as refinements of actions at the executable level by formulating a state-based model called Cyclic Transaction Processes. We provide a transition system semantics for the CTP model as also a detailed example to illustrate its modeling and behavioral features. 1 Introduction Message Sequence Charts (MSCs) are an appealing visual formalism that play a useful role in the early design stages of reactive systems [22]. They also constitute one of the behavioral diagram types in the UML framework [7]. MSCs are usually deployed to capture system requirements. A variety of choices exist as to what ought to be the relationship between such requirements and an executable specification of the system, say, in the form of a statechart [8]. Two extreme possibilities are:- The requirements constitute a necessarily incomplete testbench that the executable specification must satisfy.- The requirements constitute a complete behavioral description and henc