I. INTRODUCTION

Software-intensive systems often consist of multiple cooperating reactive components. This is also the case for the challenge problems of the MDE Tools Challenge 2017: the 'Rover' and the 'Intelligent House'. Such systems provide increasingly rich functionality in order to meet growing customer needs. Therefore, developing correct software for these systems is a difficult challenge, especially due to the distributed and concurrent nature of the systems' software.

Model-Driven Engineering tools support engineers by offering problem-specific and platform-independent modeling languages, along with a systematic and automated process of deriving platform-specific, executable code. If the modeling languages have a precise semantics, formal analysis can help analyze the system design and identify problems early and on a problem-specific level.

SCENARIOTOOLS offers such an MDE approach for the development of distributed reactive systems. It supports the scenario-based modeling via the Scenario Modeling Language (SML), a textual variant of Live Sequence Charts (LSCs) [1], [2]. SML and LSCs model the behavior of a system as a set of separate scenarios that each describe how the system components may, must, or must not react to external events. The resulting specifications are executable via the play-out algorithm [2], which enables early validation by simulation, and even executing the scenarios as the actual implementation of the system. SML in particular supports the modeling of environment assumptions in the form of assumption scenarios. They describe what will or will not happen in the environment or how the environment, in turn, will react to system actions. Modeling such assumptions is essential for systems that control processes in the physical world, such as robot control software. Also, SML supports the modeling of systems with dynamic topologies, which are systems where the component properties and relationships change at runtime and influence on how the components interact. SML supports dynamic role bindings and intergration with graph transformations for this purpose [3] (the latter will not be the focus here).

SCENARIOTOOLS supports an MDE process called SBDP (Scenario-Based Development Process). It consists of the following steps, also see Fig. 1: 1) Modeling the system structure and behavior: The structure, i.e., the systen and environment components, their properties and relationships, is modeled using a class diagram; the behavior is specified by an SML assume/guarantee specification that refers to that system structure model. 2) Realizability-checking and verifying the specification: SCENARIOTOOLS implements a formal synthesis algorithm that checks whether a strategy exists for the system to react to any sequence of environment events in such a way that the specification will be satisfied. If this is not the case, the specification is unrealizable and the algorithm produces a counter-strategy (similar to a counter-example in model checking) that helps the engineer understand the specification flaw. The algorithm can also verify whether implementation code, as created in the next step, will satisfy the specification. sumptions (run-time assumption validation). 4) Extension with platform-specific code: Code is added to bridge problem-specific events in the specification to platform-specific sensor and actuator events. Example: In the specification it may be natural to describe an event robot enters room. On the platform, this involves inferring information from multiple sensors. Such a logic may itself be a complex reactive subsystem; then it can also be implemented in SBP or by applying the process here. In this paper, we describe SBDP by the example of a cleaning robot system (our variant of the Rover challenge problem) (Sect. III). We show parts of the SML specification, give a brief explanation of play-out and the formal checks (Sect. IV), and explain the generated SBP code (Sect. V). We also describe some platform-specific functions required to execute on a RaspberryPi-based robot (Pi2Go) (Sect. VI). Last, we overview related work (Sect. VII) and conclude (Sect. VIII).

The SBDP approach appears also in [4], but with a different example. The contribution of this paper is demonstrating SBDP for the development of mobile robot system for comparison in the MDE Tools Challenge 2017 workshop.

II. CHALLENGE PROBLEM: A VACUUM CLEANER ROBOT SYSTEM

As an example, we consider a vacuum cleaning robot system where robots move between rooms in a given layout. Figure 2 shows a simple layout with three rooms and one robot. Some rooms are equipped with dirt sensors that notify a central robot manager when a room gets dirty. The robot manager then orders a robot to start moving and cleaning. When moving, the robot's battery discharges and it has to recharge at a charging station before it runs out of charge. III. SCENARIO-BASED SPECIFICATION An SML specification defines how objects in an object model must interact by sending messages. We consider synchronous communication where the sending and receiving of a message is a single message event. A message has one sending and one receiving object and it refers to an operation or property defined for the receiving object. When referring to a property, a message event has a side-effect on that property value for the receiving object, such as adding/removing elements from a list (e.g. rManager→rManager.dirtyRooms.add(dirtyableRoom)) or setting a property value (robotCtrl→robotCtrl.setMoving(true)). A run of a system is an infinite sequence of message events and object model configurations that evolve from an initial object model due to message events side-effects.

The object model is partitioned into controllable (system) objects and uncontrollable (environment) objects. A message event is a (controllable) system event if sent by a system object and an (uncontrollable) environment event otherwise.

An SML specification defines the valid runs of a system by a set of assumptionand guarantee scenarios. Guarantee scenarios describe how system objects may, must, or must not react to environment events; assumption scenarios describe what may, will, or will not happen in the environment, or how the environment may, will, or will not react to system events. A run satisfies an SML specification if it satisfies all guarantee scenarios or violates at least one assumption scenario.

Listing 1 shows parts of the SML specification of the cleaning robot system. An SML specification refers to a domain class model (line 5) that describes a set of possible object models for which the specification models the behavior. In this example, the class model defines rooms, robots, their software controller, and the robot manager. For execution and analysis, an initial object model, for example one as shown in Fig. 2, must be provided in an external configuration.

In line 7, the specification defines controllable objects by listing their classes in a corresponding section. All other objects are environment objects.

The non-spontaneous events section (line 9) lists events that we assume cannot happen spontaneously, but only when an assumption scenario specifies that they can happen. In this example, rooms can become dirty spontaneously, but a robot's room only changes when the robot was ordered to move.

The remaining specification consists of scenarios that can be organized in collaborations. A collaboration defines roles, which represent interacting objects. In this case, all scenarios are grouped in one collaboration.

A scenario specifies what are valid sequences of message events and object model conditions. Message events are modeled as scenario messages. A scenario message refers to a sending and a receiving role, an operation or property defined by the receiving role's class, and possibly message parameter expressions.

When a message event occurs in the system that matches the first message in a scenario, an active copy of the scenario is created and the sending and receiving roles are bound to the sending and receiving objects of the message event. Further roles appearing in the scenario must be bound based on binding expressions (e.g. line 36) or they are bound to objects referenced as parameters by the message event (e.g. line 26). The active copy of the scenario progresses as further message events occur that match the subsequent messages in the context of the previously determined role bindings.

The messages can have different modalities such as strict, urgent, or eventually. When the scenario progresses to these messages-we say that they become enabled-the modalities influence what may, must, and must not happen next. When a scenario proceeds to a strict message, it means that no message event must occur that corresponds to a message in the same scenario that is not currently enabled. When an urgent system message is enabled, it means that a corresponding message event must occur before the next environment event occurs. When an eventually message is enabled, a corresponding message event must occur eventually. Violations of the eventually modality are called liveness violations, violations of the strict and urgent modalities are safety violations.

A scenario can also specify wait, interrupt, and violation conditions. When an active scenario progresses to an interrupt condition that evaluates to true, the active scenario terminates; otherwise it progresses immediately. When the active scenario reaches a wait condition that evaluates to false, the active scenario does not progress until the condition renders true; when it evaluates to true, it immediately progresses beyond it. Wait conditions can have the eventually modality, meaning that the condition must become true eventually (otherwise, this is again a liveness violation). If an active scenario progresses to a violation condition that evaluates to true, this is a safety violation.

Example scenarios explained: The RobotManagerAdds-DirtyRoomToListAndSelectsRobot scenario specifies that when a room is reported as being dirty, the robot manager must add the room to a list of dirty rooms and select any of its associated robots, resp. their controllers, for cleaning it. The scenario RobotManagerOrdersRobotToCleanRoom specifies that after selecting a robot controller, the robot manager must signal that robot controller to start moving the robot. The EventuallyCleanDirtyRoom scenario specifies that once a robot manager registers a room in a list of dirty rooms, this room must eventually be removed from that list. The scenario MoveRobotWhenOrderedTo specifies that after a robot is ordered to move, the robot must move to any of the adjacent rooms. The any in the parameter expression means that one of the adjacent rooms of the robot's current room can be selected non-deterministically. How the robot should select a route to the next dirty room is not specified in this scenario-it is often desirable during the early design to under-specify in such a way, when a concrete solution has not yet been decided upon. The behavior can be refined by adding further scenarios that, for example, select a next rooms from a list of rooms that was computed as the shortest path to a dirty room. (Details are omitted for brevity.) The assumption scenario RobotArrivesInRoom specifies that when a robot is ordered to move to an adjacent room, and only if the room is really adjacent to its current room, it will eventually arrive in that room. The scenario Robot-DischargesOrRecharges specifies the assumption that the robot's battery will discharge when moving to a next room, and it will be recharged if it moves to a room with a charging station.

IV. PLAY-OUT, REALIZABILITY CHECKING, VERIFICATION

The play-out algorithm defines an execution semantics for SML specifications. In brief, it works as follows: Initially, the system waits for environment events to occur. When an environment event occurs that activates or progresses guarantee scenarios such a way that urgent or eventually system messages are enabled, the system non-deterministically chooses a corresponding system message for execution, as long as it is not blocked by another active guarantee scenario, i.e., would lead to a safety-violation. The system can send further messages until there are no more enabled system messages marked as urgent or eventually. Then the system waits for the next environment event and the process is repeated. We assume that the system is fast enough to execute any finite number of message events before the next environment event occurs. SCENARIOTOOLS supports an interactive play-out of the SML specification, which can be used for validation.

Moreover, SCENARIOTOOLS is capable of building a graph of all possible play-out executions. In that graph, edges are labeled with environment and system message events; the structure can be viewed as an infinite two-player game, played by the system against the environment. The system wins the game if, no matter what environment events the environment chooses, the system can chose system events in such a way that the resulting path corresponds to a run that satisfies the specification. If this is not the case, the specification is unrealizable and must be fixed. The game is a GR(1) game that SCENARIOTOOLS solves by an implementation of the GR(1) game algorithm by Chatterjee et al. [5]. If the specification is realizable, the algorithm produces a strategy of how the system can satisfy the specification; if the specification is unrealizable, the algorithm produces a counter-strategy of how the environment can always force a violation. The counterstrategy helps understand the specification flaw.

If the specification is realizable, but the strategy identifies that not all system moves in the play-out graph are winning, it means that during play-out, the system may make choices that do not lead to a valid run. For example, when the cleaning robot is in room 01, and room 02 gets dirty, but the robot only moves between room 01 and room 03, the dirty room may never be cleaned. In such a case, the specification can be refined, for example as explained before, in order to constrain the system choices, so that each play-out choice is winning.

When this property is satisfied, we can generate SBP code from the SML specification, which will then perform a playout of the specification that is guaranteed to satisfy the specification. SCENARIOTOOLS provides the SBP framework in which scenarios specifications can be programmed in a way that is very similar to SML. SBP builds on the Behavioral Programming for Java framework, BPJ [6]. A BPJ program consists of a collection of collaborating BThreads. Scenarios can be programmed in SBP by extending a special scenario BThread class, and SBP adds certain BThreads so that the scenario BThreads are executed according to the play-out algorithm.

SBP is suitable for programming scenarios manually, but it is also a convenient target for code generation from SML. Listing 2 shows the SBP scenario generated from the Robot-ManagerOrdersRobotToCleanRoom scenario. The class overrides different methods from a scenario superclass: the registerAlphabet method registers all messages appearing in the scenario. The initialisation method registers the messages upon which an instance of the scenario BThread will be started. The body method implements the scenario behavior after the occurrence of the first message. Here, a role binding must be performed based on a parameter that was carried by the initializing message event. A call of the request method makes the BThread yield and hand over different message events to the play-out event selection mechanism. For more details, see [4], [7].

VI. PLATFORM-SPECIFIC EXTENSION

The SBP code from the example can be executed in a distributed setting, where the robot controller runs on a RaspberryPi-based robot (Pi2Go) that mimics a cleaning robot, and the robot manager runs on a different computer, both communicating via MQTT. The Pi2Go moves on a grid that represents the room layou, see Fig. 3. The dirtDetected events can be injected via a GUI. moveToAdjacentRoom events are translated into commands that make the robot turn and follow a line to the next 'room'. When the robot arrives at the next 'room', another platform-specific component translates the sensor inputs into arrivedInRoom and setCharge events.

See the demo video here: https://youtu.be/VsSbueeIVYk. Other MDE tools for designing reactive systems exist, but most use component-and state-based models, such as MechatronicUML [9], UML-RT resp. Papyrus-RT [10], Matlab Simulink Stateflow, or the P language [11].

VIII. CONCLUSION a) Strengths:: The main strength of the approach is the requirements-aligned nature of the modeling: engineers can formally model the behavior similar to use case scenarios. Scenarios can be added to add behavior as well as restrict previous behavior. Moreover, the scenarios specify the interaction of components rather than describing the behavior of each of the components. Further strengths are:

• The formal realizability checking and verification that it supports. • The assumption validation at run-time (assumption scenario monitoring). • The distributed execution capabilities.

• Support for systems with dynamic topology b) Weaknesses:: The flexible modeling with overlapping behavior aspects spread across many scenarios has the problem that detecting and understanding specification flaws can be difficult. However, the same problem arises also when using informal use-cases and scenarios-then the problem is only worse, because no automated checks can help find them early. Further weaknesses are:

• Currently, only the generation of SBP Java code is supported. The concepts, however, can also be mapped to C++ code. • The SBP code relies on the play-out algorithm where active scenarios are run as separate threads that coordinate for event-selection. This creates memory and time overhead, which may be critical for applications where hardware resources are sparse. We propose alternative approaches in this case [12], [13]. • Currently, SCENARIOTOOLS supports no real-time constraint in SML, but a previous tool version shows how real-time constraints can be integrated [12].