Component Diagrams and Real-Time Coordination Patterns
The example steams from the RailCab research research project at the University of Paderborn. Autonomous shuttles are developed which operate individually and make independent and decentralized operational decisions.
The modular railway system further combines sophisticated undercarriages with the advantages of new actuation techniques as employed in the Transrapid to increase passenger comfort while still enabling high speed transportation. In contrast to the Transrapid the existing railway tracks will be reused. One particular problem is to reduce the energy consumption due to air resistance by coordinating the autonomously operating shuttles in such a way that they build convoys whenever possible. Such convoys are built on-de\-mand and require a small distance between the different shuttles such that a high reduction of energy consumption is achieved. Coordination between speed control units of the shuttles becomes a safety-critical aspect and results in a number of hard real-time constraints, which have to be addressed when building the control software of the shuttles.
In this example, we consider a simplified version of this shuttle coordination problem, namely we assume that only convoys of two shuttles are formed. One main requirement of the shuttle controller software is that no rear-end collision happens when the front shuttle has to brake suddenly e.g.~in case of an emergency. In order to avoid such accidents, a shuttle of a convoy brakes just with limited force when another shuttle is driving behind it with reduced distance. If no convoy is formed, the shuttles brake with full intensity.
As the shuttles change their behavior (reducing distance, changing force of emergency brakes), building and breaking of convoys needs to be coordinated. In this coordination, it must be guaranteed that never a situation occurs in which the front shuttle is in no-convoy mode and brakes with full intensity while the rear shuttle is in convoy-mode and reduced the distance.
In this example, we will first design the coordination pattern which is applied to build and to break convoys, Section. By verification of the pattern, we will recognize a design fault. We will correct and verify the pattern. Then, we will refine the pattern roles to construct the behavior of the whole shuttle component and we will verify this behavior as well. The code of the component is automatically generated and is subsequently simulated. The example is completely modeled in the two files ConvoyCoordinationUnsafe.fpr.gz and ConvoyCoordination.fpr.gz. The example is taken from our ESEC 2003 publication.
Specification of the Architecture
The first step is to specify the architecture of the system, which is done with a component diagram as visualized in Figure 1. The system consists of two shuttle components, which have two ports, refining the frontRole respectively rearRole. A communicate channel (connector) between frontRole of the first shuttle and rearRole of the second Shuttle transfers messages in order to coordinate the building and braking of the convoy. The arrows indicate, that the channel is bidirectional.
The coordination pattern, which specifies the communication protocol, is called ConvoyPattern pattern. The behavior of the roles, which belong to the pattern, is specified by real-Time Statecharts. An ATCTL formula specifies the requirement of the pattern: No deadlock may occur and the situation that the frontRole is in no-convoy mode while the rearRole is in convoy mode may never occur.
Figure 1: Structure of the shuttle system
Specification of the Behavior of the Pattern
A first version of the role behavior is given in the ConvoyCoordinationUnsafe.fpr.gz file (see Figures 2 and 3). The rearRole sends non-deterministically (indicated by the non-urgent transition, visualized by the dashed arrow) a convoyProposal event to frontRole. The frontRole replies either by rejecting (event convoyProposalRejected) or by accepting the proposal (event startConvoy). Note that a raised event has the form receiver.eventname and a event trigger has the form sender.eventname. In this example t0 indicates a clock which is reset to zero when the transition to state answer is fired. In state answer, the time invariant t0 <=1000 is is specified which describes how long the Real-Time Statechart may reside in this state.
Figure 2: Real-Time Statechart of the frontRole
Figure 3: Real-Time Statechart of the rearRole
This protocol has the advantage that even in case of message loss the aforementioned pattern constraint is never violated: If startConvoy message is lost, the frontRole is in state convoy and will brake with reduced power, and the rearRole will be in \p{no-convoy} mode, holding a large distance. Although both shuttles are in different modes, safety is still guaranteed. Breaking the convoy is done similar.
The Real-Time Statecharts entitled RearRole_TO_FrontRole and FrontRole_TO_RearRole model the realistic behavior of the channel: They model that messages are forwarded into both directions under the assumption that some of them get lost. Another useful application of this model, which describes the behavior of the connector, would be to model a delay when forwarding messages.
Verification of the Behavior of the Pattern
Switching back to the component diagram and verifying the real-time constraint (choose Modelchecking from the pop-up menu of the diagram) points out that the modeled behavior invalidates the requirement. The problem is a possible message loss, when breaking the convoy. When frontRole sends breakeConvoy back rearRole, it switches to no-convoy mode. If this message is lost, the rearRole would still be in convoy mode which invalidates safety.
Therefore we change the behavior as indicated in Figures 4 and 5 and specified in the file ConvoyCoordination.fpr.gz. In the protocol specified by these roles the rearRole initiates the building of the convoy, and the frontRole initiates the breaking of the convoy. Verification proofs that the changed behavior does not violate the safety constraints.
Figure 4: Corrected Real-Time Statechart of the frontRole
Figure 5: Corrected Real-Time Statechart of the rearRole
Specification of the Behavior of the Shuttle Component
The Real-Time Statecharts from Figures 4 and 5 specify the communication protocol between Shuttles. The concrete behavior of the Shuttle has to respect this behavior. We say the component behavior has to refine the role behaviors. Figure 6 depicts the whole behavior of the shuttle. It consists of the three orthogonal states: The upper orthogonal state refines the frontRole behavior, the lower orthogonal state refines the rearRole behavior and the orthogonal state in the middle, synchronizes the roles. This state initiates the building and the breaking of the convoys, dependent on the boolean variable convoyUseful, which is set by the shuttle software. Further, it ensures that a shuttle does not act as front role and as rear role at the same time. Note that transitions are associated with deadlines indicating how fast a state change has to occur (e.g.~the transition from noConvoy to convoyRear has the deadline interval [0, 200]).
Figure 6: Real-Time Statechart specifying the behavior of the Shuttle component
Implementation of the Behavior of the Shuttle Component
Generating code for the shuttle component will result in the class components.Shuttle1.Shuttle1. It requires an execution framework, which is provided in the libs directory of the RealtimeStatechartRealtimeJavaGenerator PlugIn. The sdm-hard-real-time.jar library guarantees that all deadlines are met. It requires an implementation of the Real-Time Specification for Java (RTSJ). We tested it with the implementation, which is available at TimeSys. It is started with the MainHardRealtime class, which is generated as well (cf. The Fujaba Real-Time Statechart PlugIn). However, sometimes a real-time system which provides an implementation of the RTSJ is not available. For this case, we provide the sdm-soft-real-time.jar library and the MainSoftRealtime class. Note that the soft-real-time version does not guarantee that all deadlines are met!
In order to demonstrate that the generated code is working, the additional java file CognitiveOperator.java is used. This file starts a non-real-time thread (java.lang.Thread), which determines if it is useful to build or to break a convoy. In fact the user determines this, by hitting a button, which results in a change of the according boolean convoyUseful attribut, which initiates the building and breaking of the convoy (cf. Figure 7).
Figure 7: Cognitive Operator