Software-intensive systems such as communicating cars or collaborating robots consist of multiple interacting components, where physical or virtual relationships between components change at run-time. This dynamic system structure inuences the components' behavior, which again aects the system's structure. With the often distributed and concurrent nature of the software, this causes substantial complexity that must be mastered during system design. For this purpose, we propose a specication method that combines scenario-based modeling and graph transformations. The specications are executable and can be analyzed via simulation. We furthermore developed a formal synthesis procedure that can nd inconsistencies or prove the specication's realizability. This method is implemented in ScenarioTools , an Eclipse-based tool suite that combines the Scenario Modeling Language, an extended variant of LSCs, and graph transformations modeled with Henshin. The particular novelty is the synthesis support for systems with dynamic structure.
In domains such as manufacturing, transportation, or logistics, we often nd critical systems that consist of multiple software-intensive components that collaborate in order to control physical processes and react to user input. In systems like communicating cars, mobile robot systems or adaptive production systems, the physical or virtual relationships between system components may change at run-time, for example due to the physical movement of components or users, or due to changing roles and responsibilities of the system components. This ? Funded by grant no. 1258 of the German-Israeli Foundation for Scientic Research and Development (GIF). See demo video here: https://youtu.be/p9mo6FJvqEE dynamic system structure inuences the behavior of the software-intensive components, and the software can again inuence the system’s structure.
Take for example a Car-to-X communication system: the system structure can change due to the movement of the cars or the occurrence of obstacles (change of physical relationships), or due to the assignment of roles, such as leader and followers in a convoy (change of virtual relationships). A car’s software must then behave dierently depending on the specic trac situation and the specic role of the car in that context. Furthermore, the car’s software can inuence how the system structure evolves subsequently, either by advising the driver or by controlling the car directly. On top of this, a car can be involved in dierent collaborations at the same time, for example convoy management and collision avoidance coordination at an obstacle.
This induces substantial complexity compared to static systems: not only do we need to develop systems with distributed and concurrent software, but the components’ behavior is also context sensitive to and in tight interrelation with the evolving system structure.
To master this complexity, we propose a specication method that combines
formal scenario-based modeling and graph transformations. This method is
implemented in ScenarioTools [
The scenario-based paradigm allows engineers to capture specications in a
way that is very close to how they are naturally conceived and communicated
during the early design. The specications are executable via an extension of the
play-out algorithm [
In this tool demonstration paper, we present the modeling, simulation and
controller synthesis capabilities of ScenarioTools based on a Car-to-X
example. The modeling approach and a prototype tool were already presented in
previous work [
As an example, we present a Car-to-X system that assists drivers in passing a narrow passage created by road works that block one lane of a two-lane street. Figure 1 shows a sketch where a car approaching the road works on the blocked lane must stop and yield to a car approaching from the opposite direction.
The lanes of the street are subdivided into lane areas. One lane area is blocked by the road works. One scenario from the system’s specication ( Scenario 1 illustrated in Fig. 1) demands that whenever a car approaches the obstacle on the blocked lane, it must show either a STOP or GO signal to the driver, and this signal must be shown before the car nally reaches the obstacle.
A second scenario ( Scenario 2 in Fig. 1) extends the behavior described by the rst: it requires that when a car approaches the obstacle on the blocked lane, it must register at a control station. This obstacle control then must check whether another car has registered for approach from the opposite direction. If so, it must disallow the rst car to enter and the STOP signal must be shown to the driver. Otherwise, it must allow the rst car to enter and the GO signal must be shown. It can be seen here how a non-deterministic choice between showing STOP or GO in Scenario 1 is now determined by Scenario 2. To specify the system further, more scenarios are added.
approaching obstacle on narrow passage lane obstacle control
Listing 1 shows how the two scenarios illustrated above are modeled with SML in ScenarioTools. The specication CarToX imports an ecore le that contains the class model of the system. Here, it denes classes for cars, lane areas, the obstacle control, etc., including their relationships. For simulation and controller synthesis, an object model, which is an instance of this class model, must be dened, with a particular number of cars and obstacles at certain positions.
The specication then denes which classes of objects are controllable and which ones are uncontrollable. Controllable classes are the components for which we specify the (software) behavior. In our case, this is the car and the control station for an obstacle that blocks one street lane. Uncontrollable classes model environment entities that are the source of environment events that the controllable components react to. In our case, the class Environment is an abstraction of the car’s sensors. For example, the environment can send a car an event that it moved to the next lane area or that it approaches a certain obstacle. In the real system a camera- or GPS-based module may send these events.
Scenario 1 “Dashboard of the car approaching Scenario 2 “Control station checks for car approaching on the blocked lane shows STOP or GO”
on the blocked lane whether entering is allowed or not” approaching an obstacle on the blocked lane approaching an obstacle on the blocked lane is narrow area free? (any car registered from other side?)
3 obstacle control 2 register
entering (Dis)Allowed 4 1
5 show stop or go define Environment as uncontrollable define Car as controllable define ObstacleBlockingOneLaneControl as controllable define Dashboard as uncontrollable collaboration ApproachingObstacleOnBlockedLane{ domain cartox // reference Ecore package assumption scenario ApproachingObstacleOnBlockedLaneAssumption with dynamic bindings [ bind currentArea to car.inArea bind nextArea to currentArea.next bind obstacle to nextArea.obstacle
Listing 1. Part of the Car-to-X SML specication message env->car.carMovesToNextArea() interrupt if [obstacle == null] message strict requested env->car.setApproachingObstacle(obstacle) } constraints [
forbidden message env->car.carMovesToNextArea() ] } // ... additional collaborations and scenarios dynamic role Environment env dynamic role Car car dynamic role Dashboard dashboard dynamic role ObstacleBlockingOneLaneControl obstacleControl // Scenario 1 specification scenario DashboardOfCarApproachingOnBlockedLaneShowsStopOrGo with dynamic bindings [ bind dashboard to car.dashboard message env->car.setApproachingObstacle(*) alternative{
message strict requested car->dashboard.showGo() } or {
message strict requested car->dashboard.showStop() } message env->car.obstacleReached() // Scenario 2 specification scenario ControlStationAllowsCarOnBlockedLaneToEnterOrNot with dynamic bindings [ bind obstacle to car.approachingObstacle bind obstacleControl to obstacle.controlledBy bind dashboard to car.dashboard message env->car.setApproachingObstacle(*) message strict requested car->obstacleControl.register() alternative if [obstacleControl.carsRegisteredOnNarrowPassageLane.isEmpty()]{ message strict requested obstacleControl->car.enteringAllowed() message strict car->dashboard.showGo() } or if [!obstacleControl.carsRegisteredOnNarrowPassageLane.isEmpty()]{ message strict requested obstacleControl->car.enteringDisallowed() message strict car->dashboard.showStop()
Next, a specication contains collaborations. A collaboration denes roles that represent collaborating objects in the system. Furthermore, a collaboration denes scenarios that describe requirements on how the controllable objects must or must not react to environment events ( specication scenarios ) or they describe what can or cannot happen in the environment ( assumption scenarios ). The two specication scenarios shown in Listing 1 model the scenarios in Fig. 1.
Each scenario describes a valid sequence of message events, where each message event is the sending of a message from one object to another. ScenarioTools supports alternative, parallel, and loop constructs within the scenarios. Furthermore, the messages in the scenarios can have the modalities strict and requested. In a nutshell, when a strict message is expected by a scenario, no message event must occur in the system that corresponds to a message in that scenario that is not currently expected. Such violations are called safety violations .
The modality requested indicates that the message must eventually occur. If a scenario never progresses at a requested message, this is a liveness violation . Hence, these modalities allow us to specify safety and liveness properties.
The scenarios also dene how the roles used by its messages shall be bound to objects in the object model. The binding of the sending and receiving roles of the rst message are given through the occurrence of the event that initiates the scenario. The binding of the other roles in the scenario is dened through binding expressions that refer to properties of objects bound to other roles. This way we can dene a behavior that is sensitive to the current system structure.
Listing 1 also shows an assumption scenario that describes that after a car moved onto a new area, and the area after this now current area has a obstacle, the car will eventually receive the event that it is approaching that obstacle.
Reference or attribute values of objects can change as a side-eect of messages prexed with set. For example, when setApproachingObstacle(obstacle) is received by a car, the car’s value for the reference ApproachingObstacle is set to obstacle. This way we can specify in the second scenario where the car shall register.
Furthermore, messages can be associated with graph transformation (GT)
rules. Figure 2 shows a rule from the Car-to-X example. A GT rule for a
message must have at least two parameters that get bound to the sending and
receiving object of the message event. A GT rule serves two purposes. First, it
restricts that messages can only occur when their corresponding GT rule is
applicable in the current object model (for details, see [
The example GT rule in Fig. 2 expresses that on the occurrence of the event carMovesToNextArea , the receiving car’s inArea link will change to express that the car moves to the next area relative to its current area. Moreover, the rule constraints that the event cannot occur, for example, when the next lane area is occupied an obstacle. Also, the car cannot advance to the next lane area if it is following a car that still resides on the same lane area. This way, GT rules associated with environment events also formulate assumptions on when these environment events can or cannot occur. «forbid#3» «forbid#1» followedBy «forbid#4»
approaching
ScenarioTools supports the execution and interactive simulation of the
combined scenario- and GT rule specications, based on an extended play-out
algorithm [
active scenarios SML editor inspect role bindings
simulation history graph enabled messages selection of message event alternative selection of next message event
The controller synthesis feature of ScenarioTools allows us to check whether the specication is realizable or not, i.e., whether an environment that satises the assumption scenarios can force the system into a safety or liveness violation of the specication scenarios. This works by creating an explicit state graph of all play-out executions, including the changing object structures, and running game-solving algorithms on this graph. ScenarioTools also supports visualizing strategies or counter-strategies that show how the system can or cannot guarantee to satisfy the specication. Using synthesis for our Car-to-X example, we can, for instance, nd out that the software cannot avoid crashes of cars unless we assume that drivers obey the dashboard signals. 4
The two notions at the core of our techniquescenario-based modeling and systems with dynamic structurehave each been studied extensively. There exist many scenario-based modeling approaches based on MSCs, UML SDs, and LSCs. There also exist approaches combining scenarios with other behavior models, such as state machines or temporal logics. Likewise, there are many approaches for modeling systems with dynamic structures, especially graph transformations.
The modeling and analysis of LSCs is supported also by the PlayGo [
Another related approach is MechatronicUML [
Acknowledgment: We thank Timo Gutjahr, Florian Knig, and Nils Glade for their work on ScenarioTools.