|
|
|
|
|
This section provides a brief overview of the Message Sequence Charts specification language. The MSC language supported by the KLOCwork MSC to SDL Synthesizer is based on the MSC-2000 standard. However, certain constructs of the MSC-2000 standard are not supported by the Synthesizer. Data manipulations within MSC scenarios are handled with certain minor deviations from the MSC-2000 standard.
The MSC language has a graphical notation. There are two kinds of MSC diagrams: basic message sequence charts (bMSC), and high-level message sequence charts (HMSC). A textual representation of MSC specifications is also available. The Telelogic Tau Integration Module of the KLOCwork MSC to SDL Synthesizer allows you to directly use the graphical MSC diagrams from the Telelogic Tau MSC Editor. The input to the core KLOCwork MSC to SDL Synthesizer is several MSCs in textual notation. Telelogic Tau can perform the conversion between the graphical and the textual notations of the MSCs.
The following figure shows a basic MSC. A basic MSC diagram describes the behavior of several instances. Each instance is graphically represented as a vertical line (called an instance axis). Each instance has an instance head that contains the name of the instance. An instance axis corresponds to the timeline of the instance. Instances exchange messages, which are shown as arrows between two instances or between an instance and the frame of the diagram. An instance can be created by another instance. A dashed arrow pointing at the instance head of the child instance shows this parent-child relationship.
Message Sequence Charts can use timers. This figure shows how timer T is started by instance c, and then expires, resulting in a timeout. An instance can also stop a timer (not shown).
A basic MSC describes events for each instance. Events on each instance axis are ordered. If the first event occurs higher on the instance axis than the second one, the first event occurs before the second one. Related pairs of message output and message input introduce another order: message output occurs before the corresponding message input. Semantics of an MSC specification is a (transitive) partial ordering of the events for all instances in all basic MSC diagrams.
The total ordering of events along each instance in general may not be appropriate. By means of a coregion, an exception to this can be made. A coregion is introduced for the specification of unordered events on an instance. Such a coregion in particular covers the practically important case of two or more incoming messages in which the ordering of consumption may be interchanged. For example, the order of consumption for messages y and e on an instance c is not specified (see Elements of a basic Message Sequence Chart diagram).
Composition of basic MSCs is represented graphically using high-level message sequence chart (HMSC) diagrams. As shown in the following figure, an HMSC diagram contains references to basic MSC diagrams and flow lines.
Data-related elements of MSC specifications include:
Composition of basic MSCs can be also described by global conditions.