MSD Specifications

Modal Sequence Diargams (MSDs), defined by Harel and Maoz [2], are a scenario-based formalism for specifying the behavior of systems of components that interact via message exchanges and have to react continuously to environment events. MSDs are a variant of Live Sequence Charts (LSCs) [4] and, as LSCs, allow engineers to precisely express which sequences may, must, or must not occur in a system. Besides their precise semantics, MSDs (like LSCs) can also be executed via the play-out algorithm [3,4]. The explanations in the following are largely based on [2,4] and [1].

MSDs and the Object Systemmode

An MSD specification consists of a set of MSDs. An MSD can be existential or universal. Existential diagrams specify sequences of events that must be possible to occur in the system. Universal diagrams specify requirements that must be satisfied by all sequences of events that occur. Here, we focus on universal MSDs.

In the following, the components of the system and entities in its environment are called objects, and together make up the object system. Each lifeline in an MSD represents an object in the object system. The set of system objects is also simply called the system; the set of environment objects is called the environment. The objects interact via messages, which have a sender, a receiver, and a name. Messages sent from system objects are called system messages; messages sent from environment objects are called environment messages. Here we consider only synchronous messages where both the sending and receiving of the message is a single, atomic event. We call the sending and receiving of a message a message event or simply event.

The figure below shows a sketch of a production robot that presses metal blanks into plates. Blanks arrive via the feed belts onto a table where they are picked up by arm A and transported to a press. There, the blanks are pressed to plates, which are then transported by arm B to the deposit belt from where they leave the system. The system is controlled by one software controller that receives events from a sensor in the table and interacts with the robot arms and the press. This system can be abstracted in an object system as shown in the lower half of the figure.

The messages in a universal MSD have a temperature and an execution kind. The temperature is either hot or cold; the execution kind is either monitored or executed. The semantics of these MSD messages is as follows: A message event occurring in the object system can be unified with an MSD message iff the event name equals the MSD message’s name and the sending and the receiving objects are represented by the sending resp. receiving lifelines of the MSD message. When an event occurs in the system that can be unified with the first message in an MSD, an active copy of the MSD or active MSD is created. We assume that an MSD has only one first message. As further events occur that can be unified with the subsequent messages in the diagram, the active MSD progresses.  This progress is captured by the cut, which marks for every lifeline the attached ends of the messages that were unified with the message events. The points where message ends are attached to the lifeline are also called the lifeline’s locations. If the cut passes the last location on each lifeline of the MSD, the active copy is terminated.

If the cut is in front of a message on its sending and receiving lifeline, the message is enabled. If a hot message is enabled, the cut is also hot; otherwise the cut is cold. If an executed message is enabled, the cut is also executed; otherwise the cut is monitored. An enabled executed message is also called an active message.

A safety violation occurs iff, while in a hot cut, a message event occurs that can be unified with a message in the MSD that is not currently enabled. If this happens in a cold cut, it is called a cold violation. Safety violations must never happen, while cold violations may occur and result in terminating the active copy of the MSD. If the cut is executed, this means that the active MSD must progress and it is a liveness violation if an active MSD never terminates or progresses to a monitored cut. (Note that this semantics slightly differs from the original semantics in [2], where hot messages reflect both the safety and the liveness aspect.)

As an example, the figure below shows two MSDs, which specify, in part, the intended behavior of the above production cell. The hot or cold temperature of a message is indicated by the red or blue color. Executed messages have a solid arrow; monitored messages have a dashed arrow. The dashed horizontal lines in the MSDs also show the reachable cuts. There the cuts  are either hot and executed (h/e) or hot and monitored (h/m). Intuitively, the first MSD (ArmATransportBlankToPress) expresses the following requirement: If a blank arrives on the table, arm A must pick it up, move to the press, release it, and move back to the table. The first message of an MSD is always cold and monitored. The subsequent messages are hot in this MSD to indicate that this scenarios must strictly follow the indicated sequence of events, especially no new blank must arrive before the robot arm has returned to the table. The system messages are executed because the system must progress at these steps. The environment messages are monitored to indicate that it is allowed, for example, for a robot arm not to arrive at the press. But then, because the message is hot, it must still not happen that another blank arrives on the table.

There can be multiple MSDs active at the same time, this way imposing multiple constraints on what must or must not happen in the system. The second MSD (PressPlateAfterArmAReleasesBlankPlate) for example specifies that if arm A releases the blank into the press, the press must press the blank; once finished, arm B must pick up the blank. This process can take place in parallel with the previous scenario. But again, this process must be finished by the time arm A releases the next blank into the press.

Consistency

We assume that always eventually a next environment events occurs and that the system is always fast enough to send any finite number of messages before the next environment event occurs. An infinite sequence of message events is called a run of the system and its environment. A run satisfies an MSD specification consisting of a set of universal MSDs iff it does not lead to a safety or liveness violation in any MSD and the system does not take an infinite sequenceof system steps, i.e., it always eventually “listens” for the next environment event. We say that an MSD specification is consistent or realizable iff it is possible for the system objects to react to every possible sequence of environment events so that the resulting run satisfies the MSD specification. A system that does so is called a (valid) implementation of the MSD specification, or it is said to satisfy the MSD specification.

Environment Assumptions

The above MSD specification can easily be violated by the environment and is thus not consistent. For example, a new blank can arrive on the table before the arm A arrived with a previous blank at the press. So, what can we do about it? We can only realize the specification if we assume further properties about the mechanical behavior of the robot. We must assume that arm A is fast enough to return to the table before the next blank arrives (or, conversely, we must assume that blanks arrive with sufficient delay). But furthermore, to satisfy the specification, we must also assume that the arm A arrives at the press or table if the controller tells it to. Also, we must assume that the press is finished before arm A releases the next blank.

These assumptions can be formalized using assumption MSDs as shown in the figure below. Assumption MSDs are shown with an additional <<EnvironmentAssumption>> label. Some of these assumption MSDs introduce a new construct, called forbidden messages. Forbidden messages have a temperature and they appear in a nested interaction fragment labeled “forbidden” at the end of the diagram. The actual end of the scenario, i,e. the last reachable cut, is before this nested fragment. Their semantics is as follows: If the MSD is active and a message occurs that can be unified with a forbidden message, this is a violation, unless the same event is also currently enabled. In the case of a hot forbidden messages this violation is a safety violation (must not happen); in the case of a cold forbidden message, this is a cold violation (leads to the termination of the active copy of the MSD).

For example, the first assumption MSD (ArmAMoveFromTableToPressAssumption) says that if moveToPress occurred, then arrivedAtPress must eventually occur, and arrivedAtTable must not occur before that. The cold forbidden messages say that this must only hold if not after moveToPress the controller sends moveToTable or moveToPress a second time. Note, however, that sending moveToPress a second time will result in an immediate re-activation of the same MSD and sending moveToTable will result in an active copy of the MSD ArmAMoveFromPressToTableAssumption. The latter MSD expresses a similar assumption for the case of the arm A moving back to the table.

In the presence of environment assumptions, we refer to the non-assumption MSDs also as requirement MSDs. Also, we extend our notion of when a run satisfies the MSD specification: a run satisfies the specification iff it satisfies all requirement MSDs or violates at least one assumption MSD. The meaning of consistency and valid implementation changes accordingly based on this extended notion of a run satisfying the specification.

With these environment assumptions, the specification is realizable. Of course, it remains to specify the behavior of arm B.

On a side note regarding the design methodology: the assumptions must of course not be too optimistic and it must be carefully validated that the actual environment of the system satisfies the assumptions.

ScenarioTools supports the modeling of MSD Specification with environment assumptions. Click here for more information.

Play-out

Harel and Marelly defined an executable semantics for the LSCs, called the play-out algorithm [4], that was later also defined for MSDs [3]. This algorithm is very useful for example for engineers in during the early design of a system to understand the interplay of different scenarios.

The basic principle of this algorithm is that if an environment event occurs and this results in one or more active MSDs with active (enabled executed) system messages, then the algorithm non-deterministically chooses to send a corresponding message if that will not lead to a safety violation in another active MSD. The algorithm will repeat sending system messages until no active MSDs with an active message remain. Then the algorithm will wait for the next environment event, and this process continues. If the play-out algorithm reaches a state where there are active messages,
but they would all lead to safety violations, this is called a violation

If the MSD specification is inconsistent, this implies that there exists a sequence of environment events that will lead the play-out algorithm to a violation. Such a situation can, however, also occur if the specification is consistent. That is because the play-out algorithm will often make non-deterministic choices without “looking ahead” if they guarantee it not to run into violations later.

ScenarioTools supports the play-out of MSD Specification with environment assumptions. Click here for more information.

Consistency-Checking and Controller Synthesis

There exists a range of approaches for automatically synthesizing a finite-state controller that implements an MSD specification. ScenarioTools supports the controller synthesis from MSD Specification with environment assumptions. Click here for more information.

Dynamic Lifeline Bindings

Above, we assumed an MSD specification that specifies the behavior of a fixed object system. But there are also systems for which many different instances exist. Then, it would be impractical to create a new specification for each instance. The figure below shows the example of a railway system, inspired by the RailCab Project in Paderborn. The vehicles in this system are called RailCabs, and drive autonomously. They are supervised by track section controls, where they must register and un-register as they move along the tracks. There can exist many different instances, with different track layouts and numbers of RailCabs. Moreover, the communication relationships between the objects can change, e.g., RailCabs move along the tracks and communicate with different control stations. We call such systems dynamic systems.

To specify the behavior for dynamic systems or many instances of systems, there are MSD specifications where the MSD’s lifelines can bind dynamically to objects. Then a lifeline refers no longer to a concrete objects, but to a class of objects. The objects that a lifeline can bind to can also be constrained.

The figure below shows an example. The top illustrates a situation where a RailCab approaches the end of its current track section. This will be detected by a sensor in a RailCab. Here we abstract from this and say that the RailCab receives the environment event endOfTS, illustrated by a green line in the sketch. After this event, it must request the track section control of the the permission to enter the next track section. The track section control must reply before the RailCab can safely brake for the last time before entering the next track section. This situation can be part of a bigger system. Below the sketch the object diagram shows the corresponding part of an object system that represents a particular RailCab system. The objects are instances of a class model as shown below. The objects reference each other according to associations defined in the class model. In the MSD at the bottom of the figure, the last lifeline has a binding expression that says that this lifeline shall bind to the track section control that is the next track section control of the one that the RailCab is currently on.

For more details about the semantics of dynamic lifelines, we refer to [4] and [2].

ScenarioTools supports the play-out of MSD Specification with dynamic lifelines, as well as the controller synthesis for such specification. For the controller synthesis, however, we require that no new objects are created dynamically in the object system, since this would lead to an infinite state space.

ScenarioTools also supports parametrized messages. Click here for more information.

Literature

[bibtex file=msd-specifications.bib]