A Scenario-based MDE Process for Developing Reactive Systems: A Cleaning Robot Example Joel Greenyer, Daniel Gritzner, Jianwei Shi, Eric Wete Software Engineering Group, Leibniz Universität Hannover, Hannover, Germany greenyer@inf.uni-hannover.de, daniel.gritzner@inf.uni-hannover.de Abstract—This paper presents the S CENARIO T OOLS solution SML in particular supports the modeling of environment for developing a cleaning robot system, an instance of the rover assumptions in the form of assumption scenarios. They de- problem of the MDE Tools Challenge 2017. We present an scribe what will or will not happen in the environment or MDE process that consists of (1) the modeling of the system behavior as a scenario-based assume-guarantee specification with how the environment, in turn, will react to system actions. SML (Scenario Modeling Language), (2) the formal realizability- Modeling such assumptions is essential for systems that con- checking and verification of the specification, (3) the generation trol processes in the physical world, such as robot control of SBP (Scenario-Based Programming) Java code from the software. Also, SML supports the modeling of systems with SML specification, and, finally, (4) adding platform-specific code dynamic topologies, which are systems where the component to connect specification-level events with platform-level sensor- and actuator-events. The resulting code can be executed on properties and relationships change at runtime and influence a RaspberryPi-based robot. The approach is suited for devel- on how the components interact. SML supports dynamic role oping reactive systems with multiple cooperating components. bindings and intergration with graph transformations for this Its strength is that the scenario-based modeling corresponds purpose [3] (the latter will not be the focus here). closely to how humans conceive and communicate behavioral requirements. SML in particular supports the modeling of S CENARIO T OOLS supports an MDE process called SBDP environment assumptions and dynamic component structures. (Scenario-Based Development Process). It consists of the The formal checks ensure that the system satisfies its specification. following steps, also see Fig. 1: I. I NTRODUCTION 1) Modeling the system structure and behavior: The struc- Software-intensive systems often consist of multiple coop- ture, i.e., the systen and environment components, their erating reactive components. This is also the case for the chal- properties and relationships, is modeled using a class di- lenge problems of the MDE Tools Challenge 2017: the ’Rover’ agram; the behavior is specified by an SML assume/guar- and the ’Intelligent House’. Such systems provide increasingly antee specification that refers to that system structure rich functionality in order to meet growing customer needs. model. Therefore, developing correct software for these systems is 2) Realizability-checking and verifying the specification: a difficult challenge, especially due to the distributed and S CENARIO T OOLS implements a formal synthesis algo- concurrent nature of the systems’ software. rithm that checks whether a strategy exists for the system Model-Driven Engineering tools support engineers by of- to react to any sequence of environment events in such fering problem-specific and platform-independent modeling a way that the specification will be satisfied. If this languages, along with a systematic and automated process of is not the case, the specification is unrealizable and deriving platform-specific, executable code. If the modeling the algorithm produces a counter-strategy (similar to languages have a precise semantics, formal analysis can help a counter-example in model checking) that helps the analyze the system design and identify problems early and on engineer understand the specification flaw. The algorithm a problem-specific level. can also verify whether implementation code, as created S CENARIO T OOLS offers such an MDE approach for the in the next step, will satisfy the specification. development of distributed reactive systems. It supports the 3) Code generation: S CENARIO T OOLS provides a Scenario- scenario-based modeling via the Scenario Modeling Language Based Programming (SBP) framework that reflects the (SML), a textual variant of Live Sequence Charts (LSCs) [1], SML concepts in Java; for example. scenarios are pro- [2]. SML and LSCs model the behavior of a system as a grammed by extending special scenario classes. Their set of separate scenarios that each describe how the system execution results in a play-out of the scenarios. This components may, must, or must not react to external events. also works in a distributed setting, where components The resulting specifications are executable via the play-out communicate over a network. S CENARIO T OOLS can au- algorithm [2], which enables early validation by simulation, tomatically translate SML into SBP code. Notably, also and even executing the scenarios as the actual implementation assumption scenarios are translated into SBP scenarios; of the system. they monitor whether the environment satisfies the as- specification III. S CENARIO -BASED S PECIFICATION SML Specification 1 analysis: 2 Assumption Assumption Guarantee Guarantee (a) Check An SML specification defines how objects in an object Assumption Guarantee Scenario Scenario Scenario ⇒ Scenario Scenario Scenario realizability (b) Verify play-out model must interact by sending messages. We consider executability synchronous communication where the sending and receiving SML-to-SBP 3 4 of a message is a single message event. A message SBP Program Platform- Sensors/Actuators/UI has one sending and one receiving object and it refers specific Platform monitoring execution to an operation or property defined for the receiving functions Assumption Assumption Guarantee Guarantee object. When referring to a property, a message event Assumption Guarantee Platform- Scenario Scenario Scenario Scenario has a side-effect on that property value for the receiving Scenario Scenario specific functions object, such as adding/removing elements from a list (e.g. rManager→rManager.dirtyRooms.add(dirtyableRoom)) Fig. 1. Scenario-based Design Process (SBDP) illustration or setting a property value (robotCtrl→robotCtrl.setMoving(true)). A run of a system is an infinite sequence of message events and object model sumptions (run-time assumption validation). configurations that evolve from an initial object model due to 4) Extension with platform-specific code: Code is added message events side-effects. to bridge problem-specific events in the specification to The object model is partitioned into controllable (system) platform-specific sensor and actuator events. Example: In objects and uncontrollable (environment) objects. A message the specification it may be natural to describe an event event is a (controllable) system event if sent by a system object robot enters room. On the platform, this involves inferring and an (uncontrollable) environment event otherwise. information from multiple sensors. Such a logic may itself An SML specification defines the valid runs of a system be a complex reactive subsystem; then it can also be by a set of assumption- and guarantee scenarios. Guarantee implemented in SBP or by applying the process here. scenarios describe how system objects may, must, or must In this paper, we describe SBDP by the example of a clean- not react to environment events; assumption scenarios describe ing robot system (our variant of the Rover challenge problem) what may, will, or will not happen in the environment, or how (Sect. III). We show parts of the SML specification, give a brief the environment may, will, or will not react to system events. explanation of play-out and the formal checks (Sect. IV), and A run satisfies an SML specification if it satisfies all guarantee explain the generated SBP code (Sect. V). We also describe scenarios or violates at least one assumption scenario. some platform-specific functions required to execute on a Listing 1 shows parts of the SML specification of the RaspberryPi-based robot (Pi2Go) (Sect. VI). Last, we overview cleaning robot system. An SML specification refers to a related work (Sect. VII) and conclude (Sect. VIII). domain class model (line 5) that describes a set of possible The SBDP approach appears also in [4], but with a different object models for which the specification models the behavior. example. The contribution of this paper is demonstrating In this example, the class model defines rooms, robots, their SBDP for the development of mobile robot system for com- software controller, and the robot manager. For execution and parison in the MDE Tools Challenge 2017 workshop. analysis, an initial object model, for example one as shown in Fig. 2, must be provided in an external configuration. II. C HALLENGE P ROBLEM : A VACUUM C LEANER ROBOT In line 7, the specification defines controllable objects by S YSTEM listing their classes in a corresponding section. All other As an example, we consider a vacuum cleaning robot system objects are environment objects. where robots move between rooms in a given layout. Figure 2 The non-spontaneous events section (line 9) lists events that shows a simple layout with three rooms and one robot. Some we assume cannot happen spontaneously, but only when an rooms are equipped with dirt sensors that notify a central robot assumption scenario specifies that they can happen. In this manager when a room gets dirty. The robot manager then example, rooms can become dirty spontaneously, but a robot’s orders a robot to start moving and cleaning. When moving, the room only changes when the robot was ordered to move. robot’s battery discharges and it has to recharge at a charging The remaining specification consists of scenarios that can station before it runs out of charge. be organized in collaborations. A collaboration defines roles, which represent interacting objects. In this case, all scenarios robot are grouped in one collaboration. manager A scenario specifies what are valid sequences of message dirt sensor room03 room01 dirt sensor room02 events and object model conditions. Message events are mod- eled as scenario messages. A scenario message refers to a robot charging station dirty sending and a receiving role, an operation or property defined by the receiving role’s class, and possibly message parameter expressions. Fig. 2. Vacuum cleaner robot system sketch, simple 3-room topology 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. 1 import "vacuumrobot.ecore" line 26). The active copy of the scenario progresses as further 2 message events occur that match the subsequent messages in 3 specification VacuumrobotSpecification { 4 the context of the previously determined role bindings. 5 domain vacuumrobotmodel // class model 6 The messages can have different modalities such as strict, 7 controllable { VacuumRobotManager VacuumRobotController } urgent, or eventually. When the scenario progresses to these 8 9 non-spontaneous events { VacuumRobotController.setRoom messages—we say that they become enabled—the modalities VacuumRobotController.setCharge} 10 influence what may, must, and must not happen next. When a 11 collaboration VacuumrobotCollaboration { 12 scenario proceeds to a strict message, it means that no message 13 static role VacuumRobotManager rManager event must occur that corresponds to a message in the same 14 dynamic role DirtyableRoom dirtyableRoom 15 dynamic role Room room scenario that is not currently enabled. When an urgent system 16 dynamic role VacuumRobot robot 17 dynamic multi role VacuumRobotController robotCtrl message is enabled, it means that a corresponding message 18 event must occur before the next environment event occurs. 19 guarantee scenario RobotManagerAddsDirtyRoomToListAndSelectsRobot{ When an eventually message is enabled, a corresponding mes- 20 dirtyableRoom->rManager.dirtDetected 21 strict urgent rManager->rManager.dirtyRooms.add(dirtyableRoom) sage event must occur eventually. Violations of the eventually 22 strict urgent rManager->rManager.orderRobotToCleanRoom( rManager.vacuumRobotControllers.any()) modality are called liveness violations, violations of the strict 23 } and urgent modalities are safety violations. 24 25 guarantee scenario EventuallyCleanDirtyRoom{ A scenario can also specify wait, interrupt, and violation 26 rManager->rManager.dirtyRooms.add(bind dirtyableRoom) 27 wait eventually [!rManager.dirtyRooms.contains(dirtyableRoom)] conditions. When an active scenario progresses to an interrupt 28 } condition that evaluates to true, the active scenario terminates; 29 30 guarantee scenario RobotManagerOrdersRobotToCleanRoom{ otherwise it progresses immediately. When the active scenario 31 rManager->rManager.orderRobotToCleanRoom(bind robotCtrl) 32 strict urgent rManager->robotCtrl.startMoving() reaches a wait condition that evaluates to false, the active 33 } 34 scenario does not progress until the condition renders true; 35 guarantee scenario MoveRobotWhenOrderedTo when it evaluates to true, it immediately progresses beyond 36 bindings [ robot = robotCtrl.robot ]{ 37 rManager->robotCtrl.startMoving() it. Wait conditions can have the eventually modality, meaning 38 interrupt [robotCtrl.moving] 39 var Room currentRoom = robotCtrl.room that the condition must become true eventually (otherwise, this 40 strict urgent robotCtrl->robot.moveToAdjacentRoom(currentRoom. is again a liveness violation). If an active scenario progresses 41 adjacentRooms.any()) strict urgent robotCtrl->robotCtrl.setMoving(true) to a violation condition that evaluates to true, this is a safety 42 } 43 violation. 44 guarantee scenario RobotMustEventuallyRecharge{ 45 robot->robotCtrl.setCharge(*) Example scenarios explained: The RobotManagerAdds- 46 wait eventually [robotCtrl.charge == robot.maxCharge] DirtyRoomToListAndSelectsRobot scenario specifies that 47 } 48 when a room is reported as being dirty, the robot manager 49 guarantee scenario RobotMustNotRunOutOfCharge{ 50 robot->robotCtrl.setCharge(*) must add the room to a list of dirty rooms and select any of 51 violation [robotCtrl.charge <= 0] its associated robots, resp. their controllers, for cleaning it. The 52 53 } // further guarantee scenarios ... scenario RobotManagerOrdersRobotToCleanRoom speci- 54 55 assumption scenario RobotArrivesInRoom { fies that after selecting a robot controller, the robot manager 56 robotCtrl->robot.moveToAdjacentRoom(bind room) 57 var Room currentRoom = robotCtrl.room must signal that robot controller to start moving the robot. 58 interrupt [!currentRoom.adjacentRooms.contains(room)] The EventuallyCleanDirtyRoom scenario specifies that once 59 eventually robot->robotCtrl.arrivedInRoom(room) 60 } a robot manager registers a room in a list of dirty rooms, this 61 62 assumption scenario RobotDischargesOrRecharges { room must eventually be removed from that list. The scenario 63 robot->robotCtrl.arrivedInRoom(bind room) MoveRobotWhenOrderedTo specifies that after a robot is 64 65 alternative [room.hasChargingStation]{ strict committed robot->robotCtrl.setCharge(robot.maxCharge) ordered to move, the robot must move to any of the adjacent 66 } or [!room.hasChargingStation]{ 67 strict committed robot->robotCtrl.setCharge( rooms. The any in the parameter expression means that one of 68 robotCtrl.charge-1) 69 } the adjacent rooms of the robot’s current room can be selected 70 } non-deterministically. How the robot should select a route to 71 // further assumption scenarios ... 72 } the next dirty room is not specified in this scenario—it is often desirable during the early design to under-specify in such a Listing 1. Part of the vacuum robot system SML specification 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 1 public class RobotManagerOrdersRobotToCleanRoomScenario extends that when a robot is ordered to move to an adjacent room, 2 VacuumrobotCollaboration { and only if the room is really adjacent to its current room, 3 @Override 4 protected void registerAlphabet() { it will eventually arrive in that room. The scenario Robot- 5 setBlocked(rManager, rManager, "orderRobotToCleanRoom", 6 RANDOM); DischargesOrRecharges specifies the assumption that the 7 setBlocked(rManager, robotCtrl, "startMoving"); robot’s battery will discharge when moving to a next room, 8 } 9 and it will be recharged if it moves to a room with a charging 10 @Override 11 protected void initialisation() { station. 12 addInitializingMessage(new Message(rManager, rManager, 13 "orderRobotToCleanRoom", RANDOM)); 14 } IV. P LAY- OUT, R EALIZABILITY C HECKING , V ERIFICATION 15 16 @Override The play-out algorithm defines an execution semantics for 17 protected void body() throws Violation { 18 robotCtrl.setBinding((VacuumRobotController) getLastMessage(). SML specifications. In brief, it works as follows: Initially, the getParameters().get(0)); system waits for environment events to occur. When an en- 19 request(STRICT, rManager, robotCtrl, "startMoving"); 20 } vironment event occurs that activates or progresses guarantee 21 } scenarios such a way that urgent or eventually system mes- Listing 2. SBP code for the RobotManagerOrdersRobotToClean- sages are enabled, the system non-deterministically chooses Room scenario 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 V. S CENARIO -BASED P ROGRAMMING (SBP) messages until there are no more enabled system messages S CENARIO T OOLS provides the SBP framework in which marked as urgent or eventually. Then the system waits for scenarios specifications can be programmed in a way that is the next environment event and the process is repeated. We very similar to SML. SBP builds on the Behavioral Program- assume that the system is fast enough to execute any finite ming for Java framework, BPJ [6]. A BPJ program consists number of message events before the next environment event of a collection of collaborating BThreads. Scenarios can be occurs. S CENARIO T OOLS supports an interactive play-out of programmed in SBP by extending a special scenario BThread the SML specification, which can be used for validation. class, and SBP adds certain BThreads so that the scenario Moreover, S CENARIO T OOLS is capable of building a graph BThreads are executed according to the play-out algorithm. of all possible play-out executions. In that graph, edges are SBP is suitable for programming scenarios manually, but labeled with environment and system message events; the it is also a convenient target for code generation from SML. structure can be viewed as an infinite two-player game, played Listing 2 shows the SBP scenario generated from the Robot- by the system against the environment. The system wins the ManagerOrdersRobotToCleanRoom scenario. The class game if, no matter what environment events the environment overrides different methods from a scenario superclass: the chooses, the system can chose system events in such a way registerAlphabet method registers all messages appearing in that the resulting path corresponds to a run that satisfies the scenario. The initialisation method registers the messages the specification. If this is not the case, the specification is upon which an instance of the scenario BThread will be unrealizable and must be fixed. The game is a GR(1) game that started. The body method implements the scenario behavior S CENARIO T OOLS solves by an implementation of the GR(1) after the occurrence of the first message. Here, a role binding game algorithm by Chatterjee et al. [5]. If the specification must be performed based on a parameter that was carried by is realizable, the algorithm produces a strategy of how the the initializing message event. A call of the request method system can satisfy the specification; if the specification is makes the BThread yield and hand over different message unrealizable, the algorithm produces a counter-strategy of how events to the play-out event selection mechanism. For more the environment can always force a violation. The counter- details, see [4], [7]. strategy helps understand the specification flaw. If the specification is realizable, but the strategy identifies VI. P LATFORM -S PECIFIC E XTENSION that not all system moves in the play-out graph are winning, it The SBP code from the example can be executed in means that during play-out, the system may make choices that a distributed setting, where the robot controller runs on a do not lead to a valid run. For example, when the cleaning RaspberryPi-based robot (Pi2Go) that mimics a cleaning robot, robot is in room 01, and room 02 gets dirty, but the robot and the robot manager runs on a different computer, both only moves between room 01 and room 03, the dirty room communicating via MQTT. The Pi2Go moves on a grid that may never be cleaned. In such a case, the specification can be represents the room layou, see Fig. 3. The dirtDetected events refined, for example as explained before, in order to constrain can be injected via a GUI. moveToAdjacentRoom events the system choices, so that each play-out choice is winning. are translated into commands that make the robot turn and When this property is satisfied, we can generate SBP code follow a line to the next ’room’. When the robot arrives at the from the SML specification, which will then perform a play- next ’room’, another platform-specific component translates out of the specification that is guaranteed to satisfy the the sensor inputs into arrivedInRoom and setCharge events. specification. See the demo video here: https://youtu.be/VsSbueeIVYk. R EFERENCES [1] W. Damm and D. Harel, “LSCs: Breathing life into message sequence charts,” in Formal Methods in System Design, vol. 19, 2001, pp. 45–80. [2] D. Harel and R. Marelly, Come, Let’s Play: Scenario-Based Program- ming Using LSCs and the Play-Engine. Springer, 2003. [3] J. Greenyer, D. Gritzner, G. Katz, and A. Marron, “Scenario-based mod- eling and synthesis for reactive systems with dynamic system structure in ScenarioTools,” in Proceedings of the MoDELS 2016 Demo and Poster Fig. 3. The RaspberryPi robot in action Sessions, co-located with ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2016), J. de Lara, P. J. Clarke, and M. Sabetzadeh, Eds., vol. 1725. CEUR, VII. R ELATED W ORK 2016, pp. 16–32. [4] J. Greenyer, D. Gritzner, F. König, J. Dahlke, J. Shi, and E. Wete, Harel and Maoz describe a mapping from LSCs to AspectJ “From scenario modeling to scenario programming for reactive systems (S2A) for play-out [8]. It is similar to SBP, but SBP scenario with dynamic topology,” in Proceedings of ESEC/FSE’17, Paderborn, threads resemble the SML scenarios more closely than the Germany, September 4-8, 2017 (to appear). ACM, 2017. [5] K. Chatterjee, W. Dvorák, M. Henzinger, and V. Loitzenbauer, “Con- AspectJ code. Also, no extension exists for the distributed ditionally Optimal Algorithms for Generalized Büchi Games,” in 41st execution of S2A code. International Symposium on Mathematical Foundations of Computer Other MDE tools for designing reactive systems exist, Science (MFCS 2016), ser. Leibniz International Proceedings in Infor- matics (LIPIcs), P. Faliszewski, A. Muscholl, and R. Niedermeier, Eds., but most use component- and state-based models, such as vol. 58. Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer MechatronicUML [9], UML-RT resp. Papyrus-RT [10], Mat- Informatik, 2016, pp. 25:1–25:15. lab Simulink Stateflow, or the P language [11]. [6] D. Harel, A. Marron, and G. Weiss, “Behavioral programming,” Comm. ACM, vol. 55, no. 7, pp. 90–100, 2012. VIII. C ONCLUSION [7] F. W. H. König, “Szenariobasierte Programmierung und verteilte Ausführung in Java,” Master’s Thesis, Leibniz Universität Hannover, a) Strengths:: The main strength of the approach is the Software Engineering Group, 2017. [Online]. Available: http://jgreen. requirements-aligned nature of the modeling: engineers can de/wp-content/documents/msc-theses/2017/Koenig2017.pdf [8] S. Maoz, D. Harel, and A. Kleinbort, “A compiler for multimodal formally model the behavior similar to use case scenarios. scenarios: Transforming lscs into aspectj,” ACM Trans. Softw. Eng. Scenarios can be added to add behavior as well as restrict Methodol., vol. 20, no. 4, pp. 18:1–18:41, Sep. 2011. previous behavior. Moreover, the scenarios specify the inter- [9] D. Schubert, C. Heinzemann, and C. Gerking, “Towards safe exe- cution of reconfigurations in cyber-physical systems,” in 2016 19th action of components rather than describing the behavior of International ACM SIGSOFT Symposium on Component-Based Software each of the components. Further strengths are: Engineering (CBSE), April 2016, pp. 33–38. • The formal realizability checking and verification that it [10] N. Kahani, N. Hili, J. R. Cordy, and J. Dingel, “Evaluation of uml-rt and papyrus-rt for modelling self-adaptive systems,” in Proceedings of supports. the 9th International Workshop on Modelling in Software Engineering, • The assumption validation at run-time (assumption sce- ser. MISE ’17. Piscataway, NJ, USA: IEEE Press, 2017, pp. 12–18. nario monitoring). [11] A. Desai, I. Saha, J. Yang, S. Qadeer, and S. A. Seshia, “Drona: A framework for safe distributed mobile robotics,” in Proceedings of the • The distributed execution capabilities. 8th International Conference on Cyber-Physical Systems, ser. ICCPS • Support for systems with dynamic topology ’17. New York, NY, USA: ACM, 2017, pp. 239–248. [12] C. Brenner, J. Greenyer, and W. Schäfer, “On-the-fly synthesis of b) Weaknesses:: The flexible modeling with overlapping scarcely synchronizing distributed controllers from scenario-based spec- behavior aspects spread across many scenarios has the problem ifications,” in Fundamental Approaches to Software Engineering (FASE that detecting and understanding specification flaws can be 2015), ser. Lecture Notes in Computer Science, A. Egyed and I. Schae- fer, Eds. Springer, 2015, vol. 9033, pp. 51–65. difficult. However, the same problem arises also when using [13] D. Gritzner and J. Greenyer, “Controller synthesis and PCL code gen- informal use-cases and scenarios—then the problem is only eration from scenario-based GR(1) robot specifications,” in Proceedings worse, because no automated checks can help find them early. of the The 4th International Workshop on Model-driven Robot Software Engineering, STAF 2017, Marburg, Germany (to appear), 2017. Further weaknesses are: • Currently, only the generation of SBP Java code is A PPENDIX supported. The concepts, however, can also be mapped See a demo video here: https://youtu.be/VsSbueeIVYk. to C++ code. S CENARIO T OOLS can be installed following the setup in- • The SBP code relies on the play-out algorithm where structions: http://scenariotools.org/downloads/download/. active scenarios are run as separate threads that coordi- The example project is located in https://bitbucket.org/ nate for event-selection. This creates memory and time jgreenyer/scenariotools-sml-examples/src//org.scenariotools. overhead, which may be critical for applications where examples.sbp.vacuumrobotv2/?at=master (Import to Eclipse hardware resources are sparse. We propose alternative runtime workspace mentioned in the above setup instructions.) approaches in this case [12], [13]. • Currently, S CENARIO T OOLS supports no real-time con- straint in SML, but a previous tool version shows how real-time constraints can be integrated [12]. Acknowledgments:: This work is funded by the German Israeli Foundation for Scientific Research and Development (GIF), grant No. 1258.