Verification and simulation of self-adaptive mechatronic systems / Christian Heinzemann

Christian Heinzemann Verification and Simulation of Self- Adaptive Mechatronic Systems Band 348 der Verlagsschriftenreihe des Heinz Nixdorf Instituts © Heinz Nixdorf Institut, Universität Paderborn – Paderborn – 2015 ISSN (Print): 2195-5239 ISSN (0nline): 2365-4422 ISBN: 978-3-942647-67-0 Das Werk einschließlich seiner Teile ist urheberrechtlich geschützt. Jede Verwertung außerhalb der engen Grenzen des Urheberrechtsgesetzes ist ohne Zustimmung der Herausgeber und des Verfassers unzulässig und strafbar. Das gilt insbesondere für Vervielfältigung, Übersetzungen, Mikroverfilmungen, sowie die Einspeicherung und Verarbeitung in elektronischen Systemen. Als elektronische Version frei verfügbar über die Digitalen Sammlungen der Universitätsbibliothek Paderborn. Satz und Gestaltung: Christian Heinzemann Hersteller: Verlagshaus Monsenstein und Vannerdat OHG Druck Buch Verlag Münster Printed in Germany Bibliografische Information Der Deutschen Bibliothek Die Deutsche Bibliothek verzeichnet diese Publikation in der Deutschen Nationalbibliografie; detaillierte bibliografische Daten sind im Internet über http://dnb.ddb.de abrufbar Verification and Simulation of Self-Adaptive Mechatronic Systems zur Erlangung des akademischen Grades eines DOKTOR DER NATURWISSENSCHAFTEN (Dr. rer. nat.) der Fakultät Elektrotechnik, Informatik und Mathematik der Universität Paderborn genehmigte DISSERTATION von Dr. Christian Heinzemann Kassel Tag des Kolloquiums: 30. Juli 2015 Referent: Prof. Dr. Wilhelm Schäfer Korreferent: Prof. Dr. Betty H. C. Cheng Korreferent: Prof. Dr.-Ing. Steffen Becker Preface So called self-adaptive of self-optimizing systems adjust their software architecture, i.e. the configuration of software modules at a certain point in time, automatically at run time. This behavior results in an efficient use of available (hardware) resources and makes these systems more robust than non self-adaptive systems in cases when the environment conditions change. Developing self-adaptive systems is very challenging, because the systems, which are the subject of this thesis, belong to the class of cyber-physical systems and exhibit a complex interplay between hardware and software components as well as hard real time requirements for inter- and intra-component communication. The thesis presents a holistic development approach for cyber-physical systems, which is based on model driven development. However, it extends this “classical” software engineering approach by means to formally specify and analyze software (architecture) reconfigurations in combination with the fulfillment of hard real time constraints for reconfiguration and communication. A particular new and intriguing feature is to include and adapt existing simulation techniques and tools from control engineering to support the analysis of a system model. The approach represents a significant step forward in making the development of complex cyber-physical systems more efficient, i.e. less costly, more rigorous and controllable concerning the quality of the resulting system. It will surely make its way also into industrial use. Paderborn , November 6, 2015 Prof. Dr. Wilhelm Schäfer Summary Self-adaptive mechatronic systems automatically adapt their behavior to a changing environment by reconfiguring their software architecture at runtime. In particular, this includes to dynamically form systems of systems at runtime, where several systems collaborate with each other using message-based communication protocols. Often, these systems are safety-critical and need to satisfy hard real-time constraints, i.e., any (timing) error in their behavior may put lives at risk. As a consequence, the software of a mechatronic system needs to meet high quality standards. In particular, it needs to be guaranteed that reconfigurations of the software architecture do not lead to an unsafe behavior or a violation of the real-time constraints. Testing alone cannot prove the correctness and thereby the safety of the mechatronic system. Existing approaches for model-driven development and analysis of mechatronic systems either provide support for analyzing real-time constraints or for analyzing reconfigurations of the software architecture, but none of the existing approaches supports both. In this thesis, we present a combination of constructive and analytical techniques that can be used by software engineers as part of a model-driven software engineering method for assuring the correctness of the software of a self-adaptive mechatronic system. As a key novelty, our approach combines formal verification and simulation-based testing for achieving a scalable analysis of the system's software. As a basis, our component-based software architecture explicitly separates discrete event-based software components from time-continuous feedback controllers. This enables to verify the software components using a compositional model checking approach that we extended by a refinement check for message-based communication protocols. The correct integration of software components and feedback controllers is assessed by a testing-based approach based on model-in-the-loop simulation. Finally, we define an approach for specifying and verifying the reconfiguration behavior of software components that, in particular, separates the reconfiguration behavior from the functional behavior for improving scalability of the verification. We evaluated all of our contributions based on the RailCab system. In particular, we specified a component-based software architecture including reconfigurations for a RailCab and conducted two case studies. These case studies demonstrate the viability of our techniques. Zusammenfassung Selbstadaptive mechatronische Systeme passen ihr Verhalten über die Rekonfiguration ihrer Softwarearchitektur zur Laufzeit automatisch an eine sich verändernde Umwelt an. Dies ermöglicht insbesondere die Bildung von sogenannten „Systems-of-Systems“ zur Laufzeit, in denen mehrere eigenständige Systeme unter Verwendung nachrichtenbasierter Kommunikationsprotokolle miteinander kollaborieren. Dabei müssen die einzelnen Systeme in der Regel harten Echtzeitanforderungen genügen und sind häufig sicherheitskritisch, d.h. jegliche Fehler im funktionalen oder zeitlichen Verhalten können Menschenleben gefährden. Nicht zuletzt deshalb muss die Software eines komplexen mechatronischen Systems hohen Qualitätsstandards genügen. Die besondere Kritikalität dieser Systeme bedingt, dass eine Rekonfiguration der Softwarearchitektur nicht zu einem undefinierten bzw. gefährdenden Verhalten oder einer Verletzung der Echtzeitanforderungen führt. Durch die Anwendung testbasierter Verfahren alleine kann die Korrektheit und damit auch die Sicherheit des mechatronischen Systems nicht garantiert werden. Existierende Ansätze für eine modellgetriebene Entwicklung und Analyse mechatronischer Systeme ermöglichen entweder die Analyse von Echtzeitanforderungen oder die Analyse von Rekonfigurationen der Softwarearchitektur zur Laufzeit. Bisher existiert jedoch kein Ansatz der beides unterstützt. Im Rahmen dieser Arbeit wird eine Kombination aus konstruktiven und analytischen Verfahren vorgestellt. Sie kann von Softwareentwicklern im Rahmen einer modellgetriebenen Softwareentwicklungsmethode eingesetzt werden, um die Korrektheit der Software eines selbstadaptiven mechatronischen Systems zu verifizieren. Die Neuartigkeit des vorgestellten Konzepts liegt in der gezielten Kombination formaler Verifikationsverfahren mit simulationsbasierten Testverfahren mit dem Ziel, einen skalierbaren Ansatz für die Analyse der Software eines mechatronischen Systems zu erhalten. Als Grundlage für diesen Ansatz wird ein Komponentenmodell vorgestellt, das explizit zwischen ereignisdiskreten Softwarekomponenten und zeitkontinuierlichen Reglern unterscheidet. Es erlaubt die formale Verifikation der Softwarekomponenten mit einem kompositionalen Model Checking Verfahren, das um eine Verfeinerungsüberprüfung für nachrichtenbasierte Kommunikationsprotokolle erweitert wurde. Die fehlerfreie Integration von Softwarekomponenten und Reglern wird anschließend mit einem Testverfahren unter Verwendung von Model-in-the-Loop Simulationen überprüft. Ergänzend wird ein Konzept für die Spezifikation und Verifikation von Rekonfigurationen vorgestellt. Dieser Ansatz trennt explizit die Spezifikation und Analyse des funktionalen Verhaltens vom Rekonfigurationsverhalten, um die Skalierbarkeit der Verifikation zu verbessern. Alle Beiträge dieser Arbeit wurden auf Basis des RailCab Systems evaluiert. Dazu wurde eine komponentenbasierte Softwarearchitektur für das RailCab inklusive der notwendigen Rekonfigurationen entwickelt. Weiterhin wurden zwei Fallstudien durchgeführt, die die praktische Anwendbarkeit der vorgestellten Verfahren aufzeigen. Acknowledgments Writing this PhD thesis has been an intense experience. Throughout all the time that I spend for researching and writing, I was surrounded by many people that supported me in various ways. Without these people, this work would not have been possible. First of all, I want to thank my supervisor Prof. Dr. Wilhelm Schäfer for giving me the opportunity to work in the inspiring environment of his research group and for the scientific guidance along the way. I thank Prof. Dr. Betty H.C. Cheng and Prof. Dr. Steffen Becker for writing their reports and Prof. Dr. Falko Dressler, Dr. Matthias Meyer, Prof. Dr. Ansgar Trächtler for attending my exam. I thank Prof. Dr. Steffen Becker for the many inspiring discussions and a lot of valuable advice. This thesis would not be the same without you. Furthermore, I would like to thank all of my (former) colleagues at the software engineering group and the Fraunhofer project group mechatronic systems design for the scientific discussions, but also for the enjoyable social activities that made my time at Paderborn a very pleasant and valuable experience. These colleagues are Anas Anis, Christian Brenner, Christopher Brink, Nicola Danielzik, Tobias Eckardt, Markus Fockel, Jens Frieben, Christopher Gerking, Faezeh Ghassemi, Dr. Joel Greenyer, Dr. Stefan Henkler, Jörg Holtmann, Thorsten Koch, Sebastian Lehrig, Renate Löffler, Ahmet Mehic, Sven Merschjohann, Dr. Jan Meyer, Faruk Pasic, Marie Christin Platenius, Uwe Pohlmann, Dr. Jan Rieke, David Schmelter, Christian Stritzke, Julian Suck, Oliver Sudmann, Dr. Matthias Tichy, Dietrich Travkin, Dr. Markus von Detten, Benedict Wohlers, Jinying Yu. Special thanks go to three of my colleagues. First, to Matthias Becker for being a very valuable office mate and for the many, not always scientific discussions. Second, to Dr. Claudia Priesterjahn for the excellent cooperation in many scientific topics and a lot of valuable advice along the way. Finally, to Stefan Dziwok for the many discussions and the excellent cooperation in the development of MECHATRONICUML and the MECHATRONICUML Tool Suite. In addition I thank all of the people with whom I collaborated in the SFB 614, in the RailCab project, and in the E-Mobil project for providing me with the opportunity to work in a very interesting, interdisciplinary environment. I highly appreciate our discussions and the excellent interdisciplinary collaboration. Special thanks go to Jutta Haupt and Jürgen Maniera of the software engineering group, Daniela Peine, Meike Steffen, and Andreas Knoke of the Fraunhofer project group as well as Astrid Canisius and Eckhard Steffen of the International Graduate School "Dynamic Intelligent Systems" for their excellent administrative and technical support. You always knew what to do. Moreover, this work would not have been possible without the students that contributed to the ideas and their implementation as part of their Bachelor's and Master's theses as well as their jobs as student workers. In particular, I would like to thank David Schubert and Andreas Volk who have been my student workers for several years. It was always fun working with you. I thank Matthias Becker, Stefan Dziwok, Marie Christin Platenius, Claudia Priesterjahn, and Aindrila Basak for their proof-reading. Page 6 D.3 MATLAB/Simulink and Stateflow................................................. D-16 D.3.1 Simulink ....................................................................... D-18 D.3.2 Stateflow....................................................................... D-19 D.3.3 Message-Based Communication......................................... D-20 D.3.4 Reconfiguration .............................................................. D-23 List of Abbreviations Page 7 List of Abbreviations ACI The Atomicity, Consistency, and Isolation properties of a database system. 23, 24, 93, 133, 134 ACI-T ACI properties combined with a correct Timing. 93–95, 124, 125, 133–136, 225 ADL Architecture Description Language 86, 88–90 AMS Autonomous Mechatronic System 28–30, 44, 51–53, 56, 58, 76–78, 80, 81, 91, 137, 225, A-13 ATCTL ∀-quantified Timed Computation Tree Logic, a variant of TCTL that only uses ∀-path quantifiers 148, 195 CIC Component Instance Configuration 13, 66, 67, 69, 85, 86, 91, 100, 104, 124–127, 136, 137, 176–178, 182, 184, 202, 211, 213, 219, 231, A-46 CSD Component Story Diagram 7, 8, 11, 12, 68–76, 83, 85–87, 91, 94, 95, 100–103, 111, 125–127, 129, 130, 132, 136, 177, 200, 202, 206, 209, 215, 225, A-59 CTL Computation Tree Logic 34, 35, 127, 148, 149 DBM Difference Bound Matrix 161 EMF Eclipse Modeling Framework 85, 215 GTS Graph Transformation System 36–38, 127 LHS Left Hand Side of a Graph Transformation Rule 38, 39, 41, 73, 75, 126 LTL Linear-Time Temporal Logic 36, 88, 127, 148, 149, 166, 167 MFM Mechatronic Function Module 27, 28 MIL Model-in-the-loop simulation 21, 22, 24, 125, 169–171, 175, 176, 217, 221–224 MSD Modal Sequence Diagram 77, 79 NAC Negative Application Condition of a Graph Transformation Rule 38–40 NMS Networked Mechatronic System 28, 51, 76, 135, 137, 167, 225, 229 NTA Network of Timed Automata 8, 31–36, 49, 128, 129, 151, 160, B-3 OCL Object Constraint Language 53, 69, 85, 89, 90 Page 8 OCM Operator-Controller-Module 28, 29, 44, 52, 57–60, 76, 90, 97, 110, 139, 170, 227, 228 QoS Quality-of-Service 49, 170, 178, 187, 189 RHS Right Hand Side of a Graph Transformation Rule 38, 39, 41, 73, 75, 126 RTCP Real-Time Coordination Protocol 7, 8, 10, 11, 43–45, 48–50, 53, 55–58, 61–63, 65, 76–81, 85, 91, 137–142, 149, 160, 162, 163, 166, 167, 186, 219, 221, 225, 226, 229, A-11 RTSC Real-Time Statechart 7–13, 45–49, 51, 55, 56, 58, 77, 78, 80, 85, 94, 101, 105– 107, 112, 113, 115–121, 123, 124, 128, 129, 132, 136–144, 146, 150–152, 154, 155, 159–165, 167, 169, 173, 177, 179, 189, 190, 192–200, 202, 204–211, 213, 216, 219, 226, 229, 230, A-62, B-1 SDD Story Decision Diagram 8, 12, 13, 81–86, 89, 91, 94, 109, 110, 127, 207, 208, 225, A-27 TCTL Timed Computation Tree Logic 34–36, 127, 141, 148, 149 TGG Triple Graph Grammar 190, 215 WCET Worst-Case Execution Time 111, 129–131, 206 List of Figures Page 9 List of Figures 1.1 The RailCab System................................................................... 19 1.2 Illustration of the Software Reconfiguration of RailCabs for Building a Convoy.................................................................................... 21 1.3 Excerpt of the Design Process for the Development of Self-Adaptive Mechatronic Systems ................................................................. 25 2.1 Structuring of Self-Adaptive Mechatronic Systems ........................... 30 2.2 Overview of the Operator-Controller-Module .................................. 31 2.3 Illustration of a Model@Runtime.................................................. 32 2.4 Network of Timed Automata Specifying a Simple Convoy Behavior .... 34 2.5 Excerpt of a Zone Graph of the NTA in Figure 2.4............................ 35 2.6 Example of a Type Graph ............................................................ 39 2.7 Typed Attributed Graph .............................................................. 39 2.8 Graph Transformation Rule for Starting a Convoy ............................ 40 2.9 Story Pattern............................................................................. 42 2.10 Story Diagram with Control Flow ................................................. 43 2.11 Story Diagram with for-each Activity Node..................................... 45 2.12 Declaration of the RTCP DistanceTransmission .................................. 46 2.13 Instance of the RTCP DistanceTransmission ...................................... 47 2.14 RTSC of Role receiver of DistanceTransmission.................................. 48 2.15 RTSC of Multi Role provider of DistanceTransmission ......................... 49 3.1 Kinds of Ports........................................................................... 56 3.2 Kinds of Atomic Components ...................................................... 59 3.3 Structure of a RTSC of a Discrete Atomic Component....................... 60 3.4 Illustration of Exchanging a Controller without Fading Function ......... 61 3.5 The structured component type ConvoyCoordination ........................... 63 3.6 The component type RailCabDriveControl ......................................... 64 3.7 The component type VelocityController............................................. 65 3.8 Structurally Compatible Ports Allowing for a Connector.................... 67 3.9 Component Instance of Component RailCabDriveControl for a RailCab Driving Alone........................................................................... 69 3.10 Component Instance of Component ConvoyCoordination for a Convoy with 1 Member.......................................................................... 70 3.11 CSD for Component RailCabDriveControl that Reconfigures the Component Instance to Serve as a Member............................................... 73 3.12 CSD for Component VelocityController that Reconfigures the Component Instance to Serve as a Member ..................................................... 74 3.13 Order Constraints for Multi Port Variables ...................................... 75 3.14 CSD for Adding a Convoy Member............................................... 76 Page 10 3.15 CSD for Component OperationStrategy that Reconfigures the Ports for Being Member .......................................................................... 78 3.16 MSD Specifying the Broadcast Message Exchange for Instantiating the RTCP ProtocolInstantiation ............................................................ 80 3.17 Declaration of the RTCP ProtocolInstantiation.................................... 81 3.18 MSD Specifying the Message Exchange for Instantiating an RTCP ..... 82 3.19 Component SDD isCoordinator for Component RailCabDriveControl ....... 84 3.20 Component SDD isStandalone for Component RailCabDriveControl........ 86 3.21 Component SDD convoyOrder for Component RailCabDriveControl ........ 87 3.22 Plugins Implementing the Concepts of the Component Model............. 88 4.1 Process for Specifying Reconfiguration Behavior ............................. 96 4.2 Reconfiguration Controller of a Structured Component...................... 97 4.3 Component Instance RailCabDriveControl with Reconfiguration Controller 98 4.4 Short-hand Notation for Reconfigurable Components........................ 99 4.5 Use Case 1: Reconfiguration after Child Request ............................. 101 4.6 Use Case 2: Reconfiguration as Part of 2-Phase-Commit.................... 101 4.7 Problems when Replacing Continuous Component Instances using Single-Phase Execution ................................................................... 102 4.8 Illustration of Three-Phase Execution ............................................ 103 4.9 RailCabDriveControl after Executing the Setup Phase for the Reconfiguration becomeMember.................................................................. 104 4.10 Approach for Identifying Quiescent States in MECHATRONICUML .... 108 4.11 RM Port Specification of the RailCabDriveControl Component .............. 110 4.12 Manager Specification of the RailCabDriveControl Component.............. 112 4.13 Executor Specification of the RailCabDriveControl Component.............. 113 4.14 RE Port Specification of the RailCabDriveControl Component............... 114 4.15 Generation Template for the Manager RTSC ................................... 116 4.16 Generation Template for the Executor RTSC (Pt. 1) .......................... 120 4.17 Generation Template for the Executor RTSC (Pt. 2) .......................... 121 4.18 Internal Structure of the Execute_ThreePhase State............................ 124 4.19 Example of a Forbidden CIC........................................................ 128 4.20 Sketch of the Generated NTA....................................................... 131 4.21 Child Stub Representing ConvoyCoordination for the Verification of Rail- CabDriveControl.......................................................................... 131 5.1 Overview of the Refinement Approach........................................... 142 5.2 RTSCs of Role railcab and Role section of RTCP EnterSection .............. 144 5.3 Components for the Different Types of Track Sections ...................... 146 5.4 Refined Protocol Behavior for Normal Sections ............................... 147 5.5 Deadlock Resulting from RailCab Stopping on a Switch.................... 147 5.6 Refined Protocol Behavior for Switches ......................................... 148 5.7 Incorrectly Refined Protocol Behavior for Railroad Crossings due to a Timing Error in State CheckRequest ............................................... 149 List of Figures Page 11 5.8 Example for Illustrating the Differences Between the Considered Refinement Definitions................................................................... 151 5.9 Refinement Check using Test Automata ......................................... 154 5.10 Decision Tree for Selecting a Refinement Definition ......................... 155 5.11 Construction Schema for our Test Automata.................................... 157 5.12 Example Test RTSC (Excerpt) for Checking the Timed Bisimulation for section................................................................................. 158 5.13 Adjusted Port RTSC for Railroad Crossings .................................... 163 5.14 Plugins Implementing our Refinement Check .................................. 165 5.15 Counterexample for the Incorrectly Refined Behavior for Railroad Crossings ........................................................................................ 168 5.16 Correctly Refined Behavior for Railroad Crossings ........................... 169 6.1 Simple Simulink Model .............................................................. 176 6.2 Enabled Subsystem .................................................................... 177 6.3 Simple Stateflow Chart ............................................................... 178 6.4 Process for Performing a MIL Simulation of a MECHATRONICUML Model in Simulink and Stateflow ................................................. 179 6.5 UML Activity Diagram Defining the Algorithm for Translating a MECHATRONICUML Model into a MATLAB/Simulink and Stateflow Model 181 6.6 Generation Template for Creating a Subsystem for an Atomic Component Instance ............................................................................ 182 6.7 Generation Template for Creating the Internal Structure of a Subsystem for an Atomic Component Instance ............................................... 184 6.8 Generation Template for Internal Structure of a Subsystem for a Fading Component............................................................................... 185 6.9 Example of a Simulink Model for a Fading Component..................... 186 6.10 Example of a Stateflow Chart for a Fading Component...................... 186 6.11 Helper Blocks that Enable Reconfiguration of Continuous Connector Instances in Simulink ................................................................. 187 6.12 Generation Template for Translating Continuous Connector Instances .. 188 6.13 Example for Using a MultiTargetControl Block for Translating a Reconfigurable Delegation Connector .................................................... 188 6.14 Generation Template for Translating Assembly Connector Instances .... 189 6.15 Generation Template for Translating Delegation Connector Instances... 189 6.16 Stateflow Chart for the Subsystem rg1 ............................................ 195 6.17 Generation Template for Translating Sent and Received Messages of Transitions to Stateflow............................................................... 197 6.18 Generation Template for Translating Transitions with Deadline to Stateflow ........................................................................................ 199 6.19 Multi Port Instance with Resulting RTSC ....................................... 200 6.20 Generation Template for Translating Transitions with Plain Synchronizations to Stateflow ................................................................. 201 Page 12 6.21 Generation Template for Translating Transitions with Synchronizations with Selectors to Stateflow........................................................... 202 6.22 Example of Using Transitions with Synchronizations with Selectors in Stateflow.................................................................................. 203 6.23 Excerpt of the Reachability Graph for the Component ConvoyCoordination.......................................................................................... 206 6.24 Integration of the ConfigurationStore in the MATLAB-specific Reconfiguration Controller................................................................... 207 6.25 Generation Template for the Configuration Store RTSC ..................... 209 6.26 Example of the executor Region of the Configuration Store RTSC ....... 210 6.27 Adapted Generation Template for the Manager RTSC ....................... 212 6.28 Adapted Generation Template for the Executor RTSC ....................... 213 6.29 Array Implementation of the AffectedComponents Structure................. 214 6.30 ConfigurationStore in the MATLAB-specific reconfiguration controller... 215 6.31 Generation Template for Integrating the MATLAB-specific Reconfiguration Controller into a Block Diagram of a structure component instance 217 6.32 Reconfiguration in Stateflow ....................................................... 219 6.33 Plugins Implementing the Translation of MECHATRONICUML Models to MATLAB/Simulink Models ..................................................... 220 6.34 Cooperating Delta Robots............................................................ 223 6.35 Coordinated Overtaking of Two Cars ............................................. 223 6.36 RailCabs Trying to Enter the Same Switch...................................... 224 A.1 Declaration of the RTCP ConvoyEntry ............................................. A-2 A.2 RTSC of the Role peer of the RTCP ConvoyEntry .............................. A-3 A.3 Declaration of the RTCP ConvoyCoordination.................................... A-4 A.4 RTSC of the Role coordinator of the RTCP ConvoyCoordination ............. A-6 A.5 RTSC of the Role member of the RTCP ConvoyCoordination................. A-7 A.6 Declaration of the RTCP ProfileDistribution ....................................... A-8 A.7 RTSC of the Role profileProvider of the RTCP ProfileDistribution ............ A-8 A.8 RTSC of the Role profileReceiver of the RTCP ProfileDistribution............ A-9 A.9 Declaration of the RTCP SpeedTransmission..................................... A-9 A.10 RTSCs of the Roles sender and receiver of the RTCP SpeedTransmission. A-10 A.11 Declaration of the RTCP StartExecution........................................... A-10 A.12 RTSCs of the Roles initiator and executor of the RTCP StartExecution ..... A-10 A.13 Declaration of the RTCP StrategyExchange ...................................... A-11 A.14 RTSC of the Role sender of the RTCP StrategyExchange..................... A-11 A.15 RTSC of the Role receiver of the RTCP StrategyExchange ................... A-11 A.16 Declaration of the RTCP NextSectionFree ........................................ A-12 A.17 RTSCs of the Roles tracksection and switch of the RTCP NextSectionFree A-12 A.18 Environment Model for the RailCab System.................................... A-14 A.19 RTSC for the SystemIdentification Protocol .................................... A-15 A.20 Story Diagram Implementing the Operation updateEnvironment............ A-16 A.21 Story Diagram Implementing the Operation addSystem...................... A-16 List of Figures Page 13 A.22 Story Diagram Implementing the Operation clean ............................. A-17 A.23 RTSC Implementing the Broadcast Communication for Instantiating the RTCP ProtocolInstantiation ....................................................... A-18 A.24 RTSC Implementing the Role requestor of the RTCP ProtocolInstantiation A-20 A.25 RTSC Implementing the Role requestee of the RTCP ProtocolInstantiation A-21 A.26 Structured Component RailroadCrossing .......................................... A-22 A.27 Component Instance of Component RailCabDriveControl for a Coordinator RailCab............................................................................... A-23 A.28 Component Instance of Component VelocityController that is used by a Coordinator RailCab .................................................................. A-24 A.29 Component Instance of Component ConvoyCoordination for a Convoy with 1 Member.......................................................................... A-24 A.30 Component Instance of Component ConvoyCoordination for a Convoy with 2 Members ........................................................................ A-25 A.31 Component Instance of Component RailCabDriveControl for a Member RailCab ................................................................................... A-26 A.32 Component Instance of Component VelocityController that is used by a Member RailCab ....................................................................... A-26 A.33 RTSC of the Component OperationStrategy (Pt. 1)............................. A-28 A.34 RTSC of the Component OperationStrategy (Pt. 2)............................. A-29 A.35 RTSC of the Component DriveLogic................................................ A-31 A.36 RTSC of the Component MemberControl.......................................... A-32 A.37 RTSC of the Component ConvoyManagement ................................... A-34 A.38 RTSC of the Component RefGen ................................................... A-36 A.39 RTSC of the Component NormalTrackSection .................................... A-38 A.40 RTSC of the Component Switch .................................................... A-40 A.41 RTSC of the Component Crossing_InfProc ....................................... A-41 A.42 Manager Specification of the ConvoyCoordination Component .............. A-43 A.43 Executor Specification of the ConvoyCoordination Component .............. A-43 A.44 RE Port Specification of the ConvoyCoordination Component ............... A-43 A.45 RM Port Specification of the VelocityController Component.................. A-44 A.46 Manager Specification of the VelocityController Component ................. A-44 A.47 Executor Specification of the VelocityController Component ................. A-44 A.48 RE Port Specification of the VelocityController Component................... A-45 A.49 RM Port Specification of the OperationStrategy Component................. A-45 A.50 RE Port Specification of the OperationStrategy Component.................. A-46 A.51 RM Port Specification of the ConvoyManagement Component.............. A-46 A.52 RE Port Specification of the ConvoyManagement Component............... A-46 A.53 CSD for Component RailCabDriveControl that Reconfigures the Component Instance to Serve as a Coordinator .......................................... A-47 A.54 CSD for Component OperationStrategy that Reconfigures the Ports for Being Coordinator ..................................................................... A-48 A.55 Constructor CSD for Creating an Instance of ConvoyCoordination.......... A-49 Page 14 A.56 Constructor CSD for Creating an Instance of RefGen......................... A-49 A.57 CSD for Component RailCabDriveControl that Adds an Additional Convoy Member............................................................................. A-50 A.58 CSD for Component ConvoyManagement that Adds Port Instances for an Additional Convoy Member at the Beginning of the Convoy........... A-51 A.59 CSD for Component ConvoyManagement that Adds Port Instances for an Additional Convoy Member in the Middle of the Convoy............... A-52 A.60 CSD for Component RailCabDriveControl that Disables the Convoy Mode by Deleting the Necessary Port Instances for Convoy Build-up............ A-53 A.61 CSD for Component OperationStrategy that Disables the Convoy Mode by Deleting the Port Instances that are Necessary for Convoy Build-up . A-53 A.62 CSD for Component RailCabDriveControl that Enables the Convoy Mode by Creating the Necessary Broadcast Port Instance ........................... A-54 A.63 CSD for Component OperationStrategy that Enables the Convoy Mode by Creating the Necessary Broadcast Port Instance ........................... A-54 A.64 CSD for Component OperationStrategy that Creates a requestor Port Instance...................................................................................... A-55 A.65 CSD for Component OperationStrategy that Creates a requestee Port Instance...................................................................................... A-55 A.66 CSD for Component OperationStrategy that Creates a peer Port Instance A-56 A.67 Generated RTSC of the Manager of RailCabDriveControl (Pt. 1)............ A-58 A.68 Generated RTSC of the Manager of RailCabDriveControl (Pt. 2)............ A-59 A.69 Generated RTSC of the Executor of RailCabDriveControl (Pt. 1)............ A-60 A.70 Generated RTSC of the Executor of RailCabDriveControl (Pt. 2)............ A-61 A.71 Definition of the AffectedComponents Data Type ............................... A-63 A.72 Story Diagram Implementing the Operation computeAffectedChildren- ForBecomeMember ...................................................................... A-64 A.73 Story Diagram Specifying the Behavior of getNextPortInstanceForRequest A-65 A.74 Story Diagram Specifying the Behavior of getMessage ...................... A-65 A.75 Story Diagram Specifying the Behavior of setReply........................... A-66 A.76 Story Diagram Specifying the Behavior of allRepliesReceived .............. A-66 A.77 Story Diagram Specifying the Behavior of canCommit ....................... A-67 A.78 Story Diagram Specifying the Behavior of getNextPortInstanceForAction . A-67 A.79 Story Diagram Specifying the Behavior of allActionsPerformed ............. A-68 A.80 Story Diagram Specifying the Behavior of setFinished ....................... A-68 A.81 Story Diagram Specifying the Behavior of allEmbeddedFinished ........... A-69 A.82 Story Diagram Specifying the Behavior of resetActionPerformed ........... A-69 A.83 Component SDD isMember for Component RailCabDriveControl that Specifies that an Instance of the Component Operates as a Convoy Member. A-70 A.84 Component SDD convoyDisabled for Component RailCabDriveControl that Specifies that an Instance of the Component will not Engage in Convoys A-71 List of Figures Page 15 A.85 Invariant Component SDD validConvoyState for Component RailCab- DriveControl that Defines that a RailCab may not be Coordinator and Member at the Same Time........................................................... A-71 A.86 Invariant Component SDD convoyOrder for Component ConvoyCoordination for Specifying a Correct Order of the RefGen Instances ............. A-72 A.87 Component SDD inStandaloneCtrl for Component VelocityController for Specifying that an Instance of the Component Executes the Standalone- Drive Controller ......................................................................... A-74 A.88 Component SDD inConvoyCtrl for Component VelocityController for Specifying that an Instance of the Component Executes the ConvoyDrive Controller ................................................................................ A-74 A.89 Invariant Component SDD validCtrl for Component VelocityController for Specifying that an Instance of the Component does not Execute both Controllers at the Same Time ....................................................... A-75 A.90 Component SDD inCoordinatorMode for Component OperationStrategy for Specifying that an Instance of the Component Operates in a Coordinator RailCab......................................................................... A-76 A.91 Component SDD inMemberMode for Component OperationStrategy for Specifying that an Instance of the Component Operates in a Member RailCab ................................................................................... A-77 A.92 Component SDD isFirst for Component RefGen for Specifying that an Instance of the Component is the First One in the Sequence of RefGen Instances.................................................................................. A-77 A.93 Component SDD isLast for Component RefGen for Specifying that an Instance of the Component is the Last One in the Sequence of RefGen Instances.................................................................................. A-78 A.94 Subsystem corresponding to Component Instance rg1 of Type RefGen... A-79 A.95 Subsystem Corresponding to the Internal Structure of Atomic Component Instance rg1 of Type RefGen .................................................. A-80 A.96 Subsystem corresponding to Component Instance cc of Type Convoy- Coordination .............................................................................. A-81 A.97 Subsystem corresponding to the Embedded CIC of the Structured Component Instance cc of Type ConvoyCoordination ................................. A-82 A.98 Subsystem of Figure A.97 Including the Generated MATLAB-specific Reconfiguration Controller .......................................................... A-83 A.99 Internal Structure of the ReconfigurationController Subsystem Generated for Component Instance cc of Type ConvoyCoordination ...................... A-85 C.1 Framework for Reachability Analyses............................................ C-1 C.2 Class Diagram of the Core Metamodel of the Reachability Analysis Framework............................................................................... C-2 C.3 Class Diagram of the Metamodel for Reachability Analysis on Story Diagrams ................................................................................. C-6 C.4 Enhancing Story Diagrams for Computing Successors....................... C-9 Page 22 Chapter 1 the components is essential for realizing the functionality of the system [SW07]. This includes both, the communication between components inside a single system but also the communication between systems as part of a system of systems [WA13]. As a result, the correctness of the software of a self-adaptive mechatronic system does not only depend on the correctness of a single component but also on the correctness of the applicationlevel communication protocols that define the interaction between components and between different system. Due to the safety critical nature of self-adaptive mechatronic systems, it is desirable to apply formal verification methods like model checking [CGP00, BK08] to ensure correctness of their component-based software. Model checking gives a mathematical proof that safety and liveness properties, which have been specified for the system, hold. However, formal verification techniques like model checking suffer from the so-called stateexplosion problem [CGP00]. It denotes the fact that the number of runtime states of a software grows exponentially in both, the number processes and the number of states of each process, if the system has concurrent executions [CKNZ12]. This makes the verification of component-based systems with concurrent components quickly infeasible. Compositional verification approaches [BCC98] tackle the state-explosion problem by verifying single components of a component-based system in isolation. Many of these approaches are based on the assume/guarantee principle [CGP00, ch. 12], i.e., they verify the correctness of a component based on assumptions that must be guaranteed by the component’s environment. One of the main difficulties of assume/guarantee approaches is deriving good assumptions automatically from the software model [CAC08]. One example of a compositional verification approach based on the assume/guarantee principle is given by the compositional verification approach of MECHATRONICUML [GTB+03, GS13]. This approach prevents the computation of assumptions by providing a syntactic decomposition of the system. In particular, MECHATRONICUML separately defines components and communication protocols that define the interaction of components. Then, components may be verified under the assumption that the interaction via the communication protocol is correct. Guaranteeing this assumption requires two steps. First, we need to verify the communication protocol using model checking [EHH+13]. At this point, the assume/guarantee principle requires that the protocol is independent of the component. Second, we need to guarantee that the component correctly implements the communication protocol without invalidating the verification results obtained for the communication protocol in the first step. However, implementing the communication protocol in the component requires to modify it. In particular, we need to integrate the protocol with the internal behavior of the component, for example, for accessing data and triggering computations. As a result, we need to verify that the component implementation of the communication protocol is a correct refinement of the verified protocol behavior according to a refinement definition. The refinement definition guarantees that the component implementation of a communication protocol does not invalidate the verification result that has been obtained for the communication protocol. In particular, a refinement definition formally defines how the Introduction Page 23 component implementation (refined protocol) may deviate from the communication protocol (abstract protocol) without invalidating a particular set of verified properties. Thus, a suitable definition of refinement is essential for a compositional verification approach as the one used by MECHATRONICUML. In literature, many different refinement definitions and according verification procedures exist [BK08, WL97, JLS00]. "Examples include timed simulation and timed bisimulation [WL97]. Depending on the particular type of protocol that is refined, all refinement definitions might be useful when building a system. A suitable refinement definition for a compositional approach needs to be as weak as possible for enabling reuse of an abstract protocol in as many different components as possible but as strong as necessary for guaranteeing that all verified properties hold for the refined protocol. If the refinement definition is too weak, it is not guaranteed that verified properties still hold for the refined protocol. If the refinement definition is too strong, the refinement check might reject the refined protocol although it fulfills all properties. This may happen, for example, if the refined protocol removes behavior that is irrelevant for the properties, but which is checked by the too strong refinement definition. The existing refinement definitions provide different compromises between reuse and preserved properties. As a consequence, there does not exist one refinement definition that is suitable for all possible protocols. Instead, a compositional verification approach should support several refinement definitions where each of which may be suitable for a particular abstract and refined protocol and a set of verified properties." [HBDS15] As a result, we need an integrated approach that automatically selects a suitable refinement definition and, in particular, verifies it for a given pair of abstract and refined protocols. 3. Simulation of Self-adaptive Mechatronic Systems The safe and correct operation of a mechatronic system depends on the correct integration of the time-continu- ous feedback controllers and the discrete software components. This includes, in particular, reconfiguration of the software architecture at runtime. As discussed before, reconfiguration of the software architecture of a mechatronic system may require to exchange feedback controllers. Exchanging feedback controllers involves the specification and execution of potentially complex fading functions [BGO06, OMT+08] that guarantee that safe meaningful values are applied on the physical machine at any time during the exchange. Therefore, it is absolutely mandatory to ensure correctness of the reconfigurations. A major objective of MECHATRONICUML is to prove the correctness of such system models by applying formal verification. However, the integration of time-continuous feedback controllers whose behavior is defined by differential equations hardens formal verification significantly. In literature, it is often referred to as the hybrid model checking problem [Hen96]. Hybrid model checking approaches either only use very simple models of time-continuous behavior or they apply overapproximation techniques Page 24 Chapter 1 [HHMWT00]. "A primary reason for adopting overapproximation is that a precise model, or a practical engineering model at hand, incorporates elements that no verification tool can handle in combination. This is often the case for hybrid system models due to their rich vocabulary. Analysis of such models can only commence after a chain of approximation steps, some of which can be achieved automatically, others – the majority in practice – requiring manual reformulation of the model under inspection. Each of these approximations may cause a loss of precision in the model, e.g., when capturing nonlinear behavior by a linear model, making the analysis less likely to succeed with a positive certificate as outcome. At the same time, as these approximations often have to be done manually, they require extremely skilled staff, are tedious and have to be repeated when the original model changes." [ERNF12] In addition, even the most recent techniques can only handle models that are "still of academic nature in the size of problems solvable." [ERNF12]. As a result, it is not yet possible to verify correctness for large and complex reconfigurable mechatronic systems such as the RailCab. A different approach to assess the correctness of the operations of a mechatronic system is testing by using a model-in-the-loop (MIL) simulation [Plu06]. In a MIL simulation, the developer tests a model of the mechatronic system against a model of its environment. The model of the mechatronic system always includes the feedback controllers and the discrete software components, but it may also include models of the mechanic, electric, or hydraulic parts of the system. This approach is already used in the automotive industry [BB08, SHS12]. MIL simulation of mechatronic systems is supported by commercial-of-the-shelf simulators such as MATLAB R /Simulink R [Matg] or Dymola [Das] for the specification language Modelica [Fri04, Mod09]. These tools, however, require models to be static, i.e., once specified, components and connections may not change while running a simulation. In addition, they do not provide native support for asynchronous, message-based communication with message buffers. As a result, we need an approach that supports MIL simulation of self-adaptive mechatronic systems that communicate via asynchronous, message-based communication protocols. This approach needs to be integrated into our component-based development approach such that model checking the event-discrete software components using the compositional verification approach mentioned above remains possible. 1.3 Contribution The contribution of this thesis is a combination of constructive and analytical techniques that support the component-based specification and analysis of self-adaptive mechatronic systems as part of a model-driven approach. As a key novelty compared to related approaches, we combine formal verification and simulation-based testing for achieving a scalable analysis for ensuring correctness of the software of a self-adaptive mechatronic Introduction Page 25 system. In particular, we contribute a transactional execution of hierarchical reconfigurations including an approach for their verification (C1), a verification procedure for showing correct refinements of communication protocols (C2), and support for simulating self-adaptive mechatronic systems in MATLAB/Simulink (C3). We integrate our contributions into the MECHATRONICUML method. As a result, our contributions enhance the existing development process of MECHATRONICUML [HSST13, BDG+14b] as outlined in Figure 1.3. All of our contributions have been implemented as part of the MECHATRONICUML Tool Suite [DGB+14]. Domain-Specific Design and Development Derive Component Model Specify Communication Protocols component model communication protocol integrated platform-independent model S1S2 domain-spanning conceptual design Specify Component Reconfiguration reconfiguration behavior real-time component behavior Specify Real-Time Behavior of Components S4 S3 Transactional Execution of Hierarchical Reconfigurations Verification of Correct Refinements Simulation Support in MATLAB/Simulink C1 C2 C3 process step parallel execution artefactcontribution Simulate Platform- Independent Model S5 domain-spanning conceptual design software artifacts Specify Platform- Independent Model Specify Platform- Specific Model Domain-Spanning Conceptual Design platform-independent model platformindependent SW-model Legend Figure 1.3: Excerpt of the Design Process for the Development of Self-Adaptive Mechatronic Systems (cf. [HSST13, GV14]) The starting point for the process, shown in Figure 1.3, is the domain-spanning conceptual design [GFDK09, GSG+09] that has been created collaboratively by experts from all disciplines involved in building the mechatronic system, e.g., mechanical engineering, control engineering, and software engineering. It includes all information about use cases, functions, and system elements that affect more than one discipline. Based on the domain-spanning conceptual design, each of the involved disciplines starts the domain-specific design and development phase. In this phase, the software engineers execute the MECHATRONICUML process [HSST13, BDG+14b], which consists of two main phases in accordance to the model-driven architecture approach [Gro14]. Thus, the process starts by creating a platform-independent model of the software. Then, the software engineers derive a platform-specific model of the software and define a deployment of the software to the hardware platform. The contributions of this thesis address the specification of the platform-independent model. The software engineer starts specifying the platform-independent model in Step S1by deriving an initial component model from the domain-spanning conceptual design. In Page 26 Chapter 1 this thesis, we unify the existing component models of MECHATRONICUML and provide an extension that enables a concise, declarative specification of hierarchical reconfigurations. This specification forms the basis for a transactional execution of reconfigurations (C1) that respects ACI-properties of database systems [BHG87]. These are atomicity, i.e., either all component instances reconfigure or none does, consistency, i.e., each reconfiguration produces a consistent component instance configuration, and isolation, i.e., reconfigurations do not interfere with each other. In Step S2, the software engineer specifies a communication protocol for each interaction between components. This includes a formal verification of the protocol behavior using model checking [GTB+03, EHH+13, Ger13]. After specifying the communication protocols, the software engineer needs to specify the real-time behavior for each component of the component model. This real-time behavior needs to include the communication protocols that have been specified and verified in Step S2such that the verified safety and liveness properties are not invalidated. We support the software engineer in this step by an integrated verification procedure that verifies whether the real-time behavior of a component correctly refines a communication protocol according to a formal refinement definition (C2). As a byproduct, our approach automatically selects a suitable refinement definition out of a set of possible refinement definitions. In Step S4, the software engineer specifies the reconfiguration behavior of the components using our aforementioned extensions of the component model. In addition, we extend this step by an approach for verifying that the reconfiguration behavior fulfills the required ACI-properties and meets all hard real-time deadlines (C1). The result of Steps S3and S4is a platform-independent model of the software. Finally, the software engineer needs to analyze whether event-discrete software and time-continuous feedback controllers have been integrated correctly by using a MIL simulation in Step S5. We support the software engineer in this step by automatically deriving a simulation model that includes both, the real-time behavior and the reconfiguration behavior of the components. The simulation model is then extended by the implementations of the feedback controllers and the environment model. The MIL simulation may then be carried out using MATLAB/Simulink. It enables the engineers of the different disciplines to validate the whole self-adaptive mechatronic system by simulation and enables to use the code generation facilities of MATLAB/Simulink for deriving source code for the system. 1.4 Overview The remainder of this thesis is structured as follows. Chapter 2 introduces the foundations that are required for understanding the contributions of this thesis. In Chapter 3, we define a new component model for MECHATRONICUML. The MECHATRONICUML component model forms the basis for the remaining contributions of this thesis. Along Introduction Page 27 with the component model, we continue our RailCab example from Section 1.1. We use this example throughout the remainder of this thesis. Chapter 4 introduces our concept for transactional execution of reconfigurations. In addition, we explain our concept for verifying reconfigurable components for ACI and timing properties. Thereafter, Chapter 5 presents our approach for verifying that communication protocols have been correctly refined by the components in our component model. Next, we present our approach for MIL simulation of self-adaptive mechatronic systems in Chapter 6. In particular, we define how simulation models in MATLAB/Simulink can be derived automatically from a MECHATRONICUML model. Finally, we summarize the contributions of this thesis and give a perspective on future works in Chapter 7. We discuss the implementation and evaluation of our concepts as well as related works along with our contributions as part of the main chapters of this thesis. The appendices provide additional, more technical information that supplement our contributions. First, Appendix A presents additional parts of the RailCab model that we use as a running example. Appendix B contains a formal definition of the semantics of Real- Time Statecharts that we use for defining state-based behavior. Finally, we describe our framework for performing reachability analyses (Appendix C) and the metamodels that have been created as part of this thesis (Appendix D). Foundations Page 29 2 Foundations This chapter introduces the foundations for understanding the concepts presented in the remainder of this thesis. We start by reviewing concepts and terminology related to self-adaptive mechatronic systems in Section 2.1 that we will use in the following. Thereafter, Section 2.2 introduces timed model checking including timed automata and the timed computation tree logic. The latter two provide the formal basis for specifying and verifying state-based behavior models of a self-adaptive mechatronic system. Section 2.3 introduces graphs and corresponding graph transformations that form the basis for specifying and verifying reconfiguration operations of a self-adaptive mechatronic system. Finally, Section 2.4 introduces MECHATRONICUML, which is a domainspecific language based on timed automata and graph transformations, that enables to specify software models for a self-adaptive mechatronic system on a higher level of abstraction. We will integrate all of the contributions of this thesis into MECHATRONICUML. 2.1 Self-Adaptive Mechatronic Systems Self-adaptive mechatronic systems automatically adapt their software architecture to a changing environment without human intervention. That requires to integrate and associate the software with the constituent parts of the mechatronic system such that the system may reason about itself and its behavior in its current environment. In this section, we introduce basic concepts and corresponding terminology related to selfadaptive mechatronic systems that we use throughout the remainder of this thesis. In Section 2.1.1, we describe how self-adaptive mechatronic systems may be structured hierarchically. Thereafter, we introduce the operator-controller-module as a reference architecture that enables to realize self-adaptive behavior in mechatronic systems (cf. Section 2.1.2). Finally, Section 2.1.3 describes how the concept of models@runtime may be used for executing reconfigurations. 2.1.1 Structuring Self-adaptive mechatronic systems can be structured hierarchically as shown in Figure 2.1. In particular, they can be structured into mechatronic function modules, autonomous mechatronic systems, and networked mechatronic systems (cf. [GRS14, pp. 8- 10]). On the lowest level, a mechatronic system consists of several mechatronic function modules (MFM). An MFM embodies part of the mechanical system including sensors, actuators, and software for controlling the mechanical system. An example is given by the drive module [HZ14] or the active suspension module [KT14] of a RailCab. MFMs may, again, be composed of other MFMs. Page 30 Chapter 2 Networked Mechatronic System (NMS) Autonomous Mechatronic System (AMS) Mechatronic Function Module (MFM) Figure 2.1: Structuring of Self-Adaptive Mechatronic Systems (cf. [GRS14, p. 9]) The overall mechanical structure is represented by the autonomous mechatronic system (AMS). It consists of the MFMs of the mechatronic system and includes additional sensors and software components for realizing self-adaptive behavior. An example of an AMS is a single RailCab. Finally, AMS’ may collaborate and form networked mechatronic systems (NMS). Networked mechatronic systems usually have no physical representation but are only virtually created by the AMS by using message-based communication protocols. Then, each AMS fulfills a particular role in the NMS. An example is given by convoys of RailCabs. 2.1.2 Operator-Controller-Module The operator-controller-module (OCM) is a reference architecture for self-adaptive mechatronic systems that separates the behavior specification into three conceptual levels [HOG04, GRS09, GRS14]. As part of this thesis, we relate our contributions to these three conceptual levels of the OCM. The different levels are the cognitive operator, the reflective operator, and the controller as shown in Figure 2.2. The controller level is the lowest. It contains the feedback controllers that control the physical system that is also called the controlled system [Kil05]. A feedback controller continuously receives the current value of the controlled variable from the physical sensors. Based on a reference value for the controlled variable, it tries to reduce the differ- Foundations Page 31 Action Level Planning Level monitoring sequencer C B A Reflective Operator Controller Operator-Controller-Module (OCM) ... configurationcontrol emergency soft real time hard real time Model-based Self-Optimiazation Behavior-based Self-Optimization cognitive information processing Cognitive Operator Cognitive Loop Reflective Loop reflective information processing motor information processing configurations A C B controlled system Motor Loop Figure 2.2: Overview of the Operator-Controller-Module [GRS14, p. 11] ence between the current value and reference value to zero by computing signals for the system’s actuators. The reflective operator forms the middle layer of the OCM. It contains event-discrete software that is required for the operations of the mechatronic system as, for example, the behavior for operating as a coordinator or member of a convoy. As a key element of this behavior, the reflective operator executes communication protocols for interacting with other AMS. In addition, the reflective operator provides the ability to reconfigure its own software architecture including the feedback controllers on the controller level. In accordance to Allen et al. [ADG98] and Zhang et al. [ZC06], we distinguish between steady-state behavior and reconfiguration behavior. The steady-state behavior defines the behavior that is executed by the feedback controllers on the controller level and by the reflective operator based on a particular software architecture without considering reconfigurations. The reconfiguration behavior defines possible modifications of the software architecture. Using the reflective loop, self-adaptive systems continuously monitor their own Page 38 Chapter 2 An alternative for specifying safety and liveness properties is given by linear-time temporal logic (LTL, [Pnu77, HR04]). LTL uses a linear time model based on paths that do not consider branching. Therefore, the temporal connectives of LTL only use a temporal operator but no path quantifier. We discuss preservation of LTL formulas for our refinement check, but do not use LTL for specifying safety and liveness properties as part of this thesis because timed variants of LTL like the metric temporal logic (MTL, [Koy90]) are not decidable for the dense time model used by NTAs presented above [AH92] and, thus, no model checkers exist. 2.2.3 Model Checking Procedure A timed model checking procedure decides whether a given timed automata or NTA fulfills a given TCTL property [HNSY94, BDM+98, BY04]. Therefore, the model checking procedure computes a zone graph for the timed automaton or the NTA. Then, it successively labels the resulting states with the atomic propositions and the subformulas that hold for a given state. The timed automaton or the NTA fulfills the TCTL property if and only if the formula is true for the initial state of the zone graph. If the TCTL property is not fulfilled, the model checker returns a counterexample. A counterexample is a trace of the zone graph that caused that the TCTL property is not fulfilled. In the course of this thesis, we use the model checker UPPAAL [LPY95, BDL+06b] for verifying TCTL properties for NTAs. 2.3 Graph-Based Specifications The theory of graph transformation systems (GTS, [Roz97]) is based on graphs. Intuitively, graphs consist of nodes and edges connecting the nodes. GTS define a language consisting of words where each word is a graph. Productions of a GTS are given by graph transformation rules that formally specify how one graph may be transformed into another one. In this thesis, we use GTS as a basic formalism for formalizing reconfiguration operations of MECHATRONICUML that modify the software architecture of a self-adaptive mechatronic system. This, in turn, enables to formally verify reconfiguration operations of MECHATRONICUML, which we exploit in our reconfiguration approach introduced in Chapter 4. In a general GTS, the nodes and edges of a graph do not have a predefined correspondence to a real-world or software entity. For defining reconfigurations of a software architecture by graph transformations, we need to define a correspondence between nodes and edges of a graph and the components and connectors of the software architecture. This a achieved by using typed attributed GTS that we introduce in Section 2.3.1. Story diagrams as introduced in Section 2.3.2 extend typed attributed graph transformation rules by the ability to specify control flow. This enables to specify more complex reconfiguration operations. Therefore, story diagrams are the basis for specifying reconfiguration operations in MECHATRONICUML as defined in Section 3.3. Foundations Page 39 2.3.1 Typed Attributed Graph Transformations Systems Typed attributed GTS [EEPT06] extend GTS by a type graph and node attributes. The type graph defines which types of nodes exist and by which types of edges they may be connected. Node attributes enable to store values like integers or strings inside a node. Both features are essential for modeling reconfiguration (cf. Section 3.3). Figure 2.6 shows an example of a simple type graph that defines two nodes types and six edge types. The two nodes types, RailCab and TrackSection, represent RailCabs and track sections. The node type RailCab defines an attribute of type Integer that stores the size of the convoy that the RailCab is currently driving in. The edge types define how nodes of type RailCab and TrackSection may be connected. RailCab convoySize : int railcabs on 0..* 1 TrackSection next0..1 0..1 prev 0..1 coordinator 0..* member Figure 2.6: Example of a Type Graph ATrackSection has a next and a prev TrackSection. These edge types define the outline of the track system. In addition, the edge type railcabs is used to refer to all RailCabs currently driving on a track section. The edge type on enables to define on which Track- Section aRailCab is currently located. Finally, coordinator and member enable a RailCab to refer to its coordinator or its members. Atyped attributed graph is always typed over exactly one type graph, while an arbitrary number of typed attributed graphs may use the same type graph. All nodes and edges of a typed attributed graph must be typed over exactly one node type or edge type, respectively, of the type graph. The type of a node or edge is immutable. In the course of this thesis, we will assume that the type graph is given by a metamodel [Küh06]. Figure 2.7 shows an example of a typed attributed graph that is typed over the type graph in Figure 2.6. It contains five nodes and five edges. It specifies the situation where two RailCabs drive on two consecutive track sections. The RailCabs are not yet driving in a convoy because they are not connected with each other by a coordinator or member edge. ts3 : TrackSection rc1 : RailCab convoySize = 0 prev ts2 : TrackSection next ts1 : TrackSection prev next rc2 : RailCab convoySize = 0 onon railcabs railcabs Figure 2.7: Typed Attributed Graph Page 40 Chapter 2 Each node of a typed attributed graph has values for all of its attributes. In Figure 2.7, the nodes rc1 and rc2 both have value 0for their convoySize attribute. A typed attributed GTS consists of a type graph, an initial graph that is typed over the type graph, and a set of graph transformation rules that define how graphs may be modified. A graph transformation rule specifies a left hand side (LHS), a right hand side (RHS), a so-called rule morphism, and a set of negative application conditions (NAC) [EEPT06]. LHS, RHS, and NACs are typed attributed graphs based on the type graph. The rule morphism associates nodes in the LHS to nodes in the RHS to denote which nodes are the same. In addition, each NAC defines its own morphism that associates nodes in the LHS to nodes in the NAC. Rule: startConvoy LHS ::= RHS NAC1 ts2 : TrackSection rc1 : RailCab ts1 : TrackSection next rc2 : RailCab onon ts2 : TrackSection rc1 : RailCab convoySize = convoySize + 1 ts1 : TrackSection next rc2 : RailCab onon coordinator member rc3 : RailCabrc2 : RailCab coordinator NAC2 rc1 : RailCabrc2 : RailCab member Figure 2.8: Graph Transformation Rule for Starting a Convoy Figure 2.8 shows an example of a graph transformation rule startConvoy that starts a convoy between two RailCabs that are positioned on two consecutive track sections. The LHS specifies this situation. The RHS specifies the same situation but rc2 is now a member of a convoy that is coordinated by rc1. In our example, we implicitly define the rule morphism by using the same names, e.g., rc1 and rc2 for nodes in the LHS and RHS. The graph transformation rule startConvoy defines two NACs. NAC1defines a situation where rc2 is already a member of a convoy that is coordinated by a different RailCab rc3. NAC2defines a situation where rc2 is already a member of a convoy that is coordinated by rc1. The application of a graph transformation rule such as startConvoy to a typed attributed graph is performed in three steps. In the first step, we search a match of the LHS to the typed attributed graph, the so-called host graph. Basically, a match is an occurrence of the LHS in the host graph. The match needs to consider both, the type of the node and the attribute values of the node. That means, nodes of type RailCab in the LHS may only be matched to nodes of type RailCab in the host graph. If a node in the LHS specifies an attribute value, the matched node in the host graph needs to have the same attribute value. Attributes that are not used in the LHS are ignored while searching the match. A match for a graph transformation rule is only valid, if no NAC of the graph transformation rule can be matched to the host graph. In the second step, we remove all nodes and edges that occur in the LHS but not in the RHS of the graph transformation Foundations Page 41 rule. To determine this set of nodes, we use the rule morphism. In the third step, we add all nodes and edges that occur in the RHS but not in the LHS. In this step, we also modify attribute values if necessary. When applying the graph transformation rule startConvoy in Figure 2.8 to the typed attributed graph in Figure 2.7, we proceed as follows. For obtaining a match, we search for an occurrence of the LHS in the graph. The occurrence is given by the nodes rc1,rc2, ts2, and ts3 in Figure 2.7. Next, we need to check whether this match may be extended such that any NAC is completely matched. This is not the case because rc2 in Figure 2.7 is not yet member of a convoy. Thus, startConvoy has been successfully matched and we perform the graph rewriting. Therefore, we create a coordinator edge from rc2 to rc1 and a member edge from rc1 to rc2. In addition, we update the value of the attribute convoySize of rc1 by incrementing it by 1. For the application of graph transformation rules, we follow the single pushout approach with injective matches (SPO, [Roz97]). In essence, that means that different nodes of the LHS need to be matched to different nodes in the host graph. For example, rc1 and rc2 in the LHS of startConvoy need to be matched to different RailCab nodes in the host graph. In addition, if the graph transformation rule specifies to delete a node without deleting all of its incident edges, then the incident edges are implicitly deleted as well to avoid dangling edges. 2.3.2 Story Driven Modeling Story driven modeling (SDM, [Zün01]) is an approach for the object-oriented and model-driven software development. One essential part of SDM are story diagrams [FNTZ00, Zün01] that are used in the design phase for formally specifying operations of an object-oriented program. They combine an imperative control flow specification based on UML Activity Diagrams [Gro11c] with a formal, declarative specification of object manipulation based on typed attributed graph transformations, called story patterns. Story diagrams may also be used as an endogenous in-place model transformation language [CH06] and form the basis for defining reconfiguration operations in our approach as described in Section 3.3. In the following, we give a brief overview of story patterns (cf. Section 2.3.2.1) and story diagrams (cf. Section 2.3.2.2) based on the latest version by von Detten et al. [vDHP+12a]. 2.3.2.1 Story Patterns A story pattern consists of object variables and link variables that correspond to the nodes and edges of a typed attributed graph transformation rule. Object variables and link variables are typed over a metamodel [Küh06]. Story patterns use a concise notation of the typed attributed graph transformation rule that visualizes LHS, RHS, and NACs in a single graph. As an example, consider the story pattern in Figure 2.9 that is equivalent to the typed attributed graph transformation rule in Figure 2.8. Page 42 Chapter 2 rc2 convoySize := convoySize + 1 rc1 ts2 : TrackSection ts1 : TrackSection next ► ▼ on ▼ on coordinator ► «create» ◄ member «create» ◄ member r3 : RailCab ◄ coordinator Figure 2.9: Story Pattern Objects variables and link variables that shall be created by the story pattern are labelled with a «create» annotation such as the link variables coordinator and member in Figure 2.9. Object variables and link variables that shall be deleted are labeled with «destroy». All object variables and link variables not carrying an annotation are not changed by the graph rewriting. Furthermore, object variables have a binding state. In particular, we distinguish between bound and unbound object variables. An unbound object variable needs to be matched by the graph matching when the story pattern is applied. A bound object variable has already been matched to an object of the host graph during the application of another story pattern. This matching is not changed while matching the unbound object variables of the story pattern. In our example, the object variables ts1,ts2, and r3 are unbound, while rc1 and rc2 are bound. In the concrete syntax, unbound variables visualize both, their name and their type, whereas bound variables only visualize their name. Story patterns that are embedded in a story diagram always need to have at least one bound object variable. In addition, any unbound object variable must be reachable from at least one bound object variable by traversing link variables. The objective of this restriction is to reduce the matching effort for story patterns compared to typed attributed graph transformation rules. In general, deriving a matching for a typed attributed graph transformation rule is equivalent to the NP-complete subgraph isomorphism problem and, thus, requires exponential runtime. The bound object variables, however, provide starting points for the graph matcher and, in combination with the type graph, reduce the number of possible matchings and, thus, the runtime for deriving a valid matching significantly [SWZ95, Zün95, pp. 195ff.]. NACs are represented by so-called negative variables that are crossed out in the concrete syntax. In our example, the negative object variable rc3 and the negative link variable coordinator between rc2 and rc3 correspond to NAC1in Figure 2.8. They denote that rc2 does not have a coordinator reference to another RailCab. The negative link variable member from rc1 to rc2 corresponds to NAC2and defines that rc2 must not already be a member of rc1. Object variables may contain conditions on and assignments to object attributes as in typed attributed graph transformation rules. In our example, the value of the attribute convoySize of rc1 is set to one. As in typed attributed graph transformation rules, condi- Foundations Page 43 tions on object attributes are part of the LHS, while assignments to attributed values are part of the RHS. 2.3.2.2 Story Diagrams A story diagram consists of activity nodes and activity edges for specifying the control flow such as sequential and conditional execution as well as loops. As part of this thesis, we use different kinds of activity nodes and activity edges that we illustrate below. The kinds of activity nodes that we consider are initial nodes, final nodes, story nodes, decision nodes, activity call nodes, and statement nodes. Each story diagram contains exactly one initial node that marks the starting point of its execution. In addition, each story diagram has at least one final node that marks the end of its execution. A story node contains a story pattern and, thus, defines a modification of an object structure. Decision nodes enable to define complex branch and merge structures for the control flow. An activity call node [BvDHR11] enables to invoke another story diagram. Finally, statement nodes contain source code and may be used, for example, to define local counter variables. rc1 as Coordinator [failure] startConvoy(RailCab rc1,RailCab rc2) : Boolean result rc2 convoySize := convoySize + 1 rc1 ts2 : TrackSection ts1 : TrackSection next ► ▼ on ▼ on coordinator ► «create» ◄ member result := false [success] result := true «create» ◄ member r3 : RailCab ◄ coordinator Call rc1.enableCoordination(); [else] [rc1.convoySize == 1] Figure 2.10: Story Diagram with Control Flow As an example, consider the story diagram shown in Figure 2.10. The story diagram specifies the behavior of starting a convoy. It embeds the story pattern shown in Figure 2.9 in the story node named rc1 as Coordinator.Ifrc2 is the first member of rc1 as specified by the decision node below the story node, we additionally invoke enableCoordination on rc1 via the activity call node at the bottom of the figure. Activity edges connect the activity nodes and define how the execution of the story diagram proceeds after executing an activity node. Story diagrams support different kinds of activity edges that are distinguished by their labels in the concrete syntax. The Page 44 Chapter 2 kind and number of outgoing activity edges depend on the kind of the source activity node. Initial nodes and activity call nodes always have exactly one outgoing default activity edge but no other outgoing activity edges. A default activity edge has no label. Final nodes have no outgoing edges. A story node may either have one outgoing default activity edge or it may have one outgoing success activity edge, identified by the label [success], and one outgoing failure activity edge, identified by the label [failure]. The success activity edge is taken if the story pattern in the story node has been matched successfully. The failure activity edge is taken if the story pattern could not be matched. Finally, a decision node may have either one outgoing default activity edge (merge node) or it has noutgoing activity edges where n≥2(branch node). In the latter case, n−1 of the outgoing activity edges must carry a Boolean condition, while the remaining one is an else activity edge that has the label [else]. In this case, the activity edge with a satisfied condition is executed or, if none of the Boolean conditions is fulfilled, the else activity edge is executed. In addition to defining the control flow, the activity edges define how matchings are propagated through a story diagram. An initial matching of a story diagram is provided by the input parameters. The story diagram in Figure 2.10 has two input parameters rc1 and rc2 of type RailCab. This matching is propagated to the story node via the default activity edge. The story pattern, which is embedded in the story node, uses rc1 and rc2 as bound variables. If the story pattern can be applied successfully, the matching is extended by all matched and created variables. Destroyed object variables are removed from the matching. Then, the matching is propagated via the success activity edge to the subsequent node. If the story pattern cannot be matched, the matching is propagated unmodified via the failure activity edge. Decision nodes never change a matching. The Boolean conditions at the outgoing activity edges may refer to any object variables in the current matching and to their attributes. At a final node, object variables contained in the current matching can be assigned to the output parameters. In our example, however, we only assign the literals true and false to the output parameter result depending on whether the creation of the convoy was successful. Story diagrams may be defined as an implementation of an operation of a class of the metamodel. In this case, the story diagram may be invoked by calling the operation for an object of the corresponding type. In our example in Figure 2.10, the activity call node invokes the operation enableCoordination on the object rc1 of type RailCab. In this case, rc1 serves as an implicit parameter for the story diagram and may be used as a bound variable with the name this in the embedded story patterns. For defining loops, story nodes may be marked as for-each story nodes. A for-each story node is iteratively applied to any matching that may be obtained for the embedded story pattern in the host graph but guarantees that no matching is used twice. A foreach story node always has one outgoing end activity edge that is taken if no further matching may be obtained for the story pattern in the for-each story node (labeled with Foundations Page 45 [end]). Optionally, a for-each story node may have an additional each time activity edge (labeled with [each time]) that is taken for each matching of the embedded story pattern. Bind each Member... [end] RailCab::breakConvoy() this member : RailCab ▼ member … and remove it! this convoySize := convoySize –1 member ▼ member [each time] «destroy» Figure 2.11: Story Diagram with for-each Activity Node Figure 2.11 shows the story diagram breakConvoy. The story diagram may be invoked on an object of type RailCab, represented by the this variable, for dissolving a convoy. For the RailCab the for-each story node Bind each member..., which is visualized with a cascaded border line, matches any member of the RailCab. For each match, we exit the for-each story node via the each time activity edge. The second story node destroys the link to the member and decreases the convoySize by 1. 2.4 MechatronicUML MECHATRONICUML [GTB+03, EHH+13, BDG+14a] is a model-driven software engineering method for developing event-discrete software of self-adaptive mechatronic systems. It adapts the concepts of UML 2.4 [Gro11c] for defining a component-based software architecture, state-based behavior, and runtime reconfiguration of a self-adap- tive mechatronic system. In the course of this thesis, we integrate all of our contributions into MECHATRONICUML and provide an example model for the RailCab system based on MECHATRONICUML in Appendix A. In the following, we briefly review the most important parts for specifying platformindependent models based on MECHATRONICUML that we use as part of this thesis. In particular, we introduce Real-Time Coordination Protocols (Section 2.4.1), Real- Time Statecharts (Section 2.4.2), and the assumptions on quality-of-service characteristics that are employed by MECHATRONICUML. For a detailed description of these parts of MECHATRONICUML, we refer to the MECHATRONICUML language specification [BDG+14b]. We discuss the component model of MECHATRONICUML and the specification and execution reconfigurations in detail in Chapters 3 and 4. 2.4.1 Real-Time Coordination Protocols MECHATRONICUML uses Real-Time Coordination Protocols (RTCPs) for formally specifying asynchronous message-based communication between two communication Page 46 Chapter 2 partners [GTB+03, EHH+13]. RTCPs may be used in the reflective operator and in the cognitive operator of the OCM for defining message-based communication between different AMS but also between different components inside a single AMS. An RTCP defines a name and two named roles that represent the communication partners. Each role has a behavior specification in terms of a Real-Time Statechart (cf. Section 2.4.2) that defines its behavior. The roles are connected by a role connector that specifies requirements to the physical connection such as the maximum transmission delay for a message and the possibility of message loss (cf. Section 2.4.3). provider receiver DistanceTransmission [0..*] [1] in-buffer size: 1 in-buffer size: 1 delay: 1 ms single rolemulti role role connector coordination protocol role name label Figure 2.12: Declaration of the RTCP DistanceTransmission Figure 2.12 shows the declaration of a RTCP named DistanceTransmission that is used by a convoy coordinator for periodically transmitting new reference data to the members [HH11a, EHH+13]. The RTCP has two roles named provider and receiver. The RTCP is represented by the dashed ellipse, while the roles are represented by the dashed squares including the connection to the pattern ellipse. In our example, the role connector specifies a transmission delay of 1ms for each message. Each role defines a set of message types that it may send or receive. Message types are used to type the messages that are exchanged at runtime. They have a name and an optional list of typed, named parameters. Which messages may be sent or received at a particular point in time is defined by the Real-Time Statecharts of the roles, which we present in Section 2.4.2. If a role only receives messages, it is an in-role. If it only sends messages, it is an out-role. If it both sends and receives messages, it is an in/outrole [BDG+14b]. In our example in Figure 2.12, both roles are in/out-roles which is denoted by the two triangles inside the squares. Received messages are stored in a message buffer that we call in-buffer. In this work, we restrict ourselves to FIFO-queues as in-buffers where all the received messages are stored in the same queue. Each role specifies a buffer size for its in-buffer [BDG+14b]. In our example, both roles specify a buffer size of 1, i.e., they can store at most one message in their in-buffer. In addition, each role specifies a cardinality using a Min-Max-Notation as defined by Coad and Yourdon [CY90, p. 127]. Thus, the cardinality of a role defines with how many instances of the other role it may communicate at least and at most. If the upper bound of the cardinality equals 1, then we call it a single role. If the upper bound is greater than 1, we call it a multi role [EHH+13, BDG+14b]. In our example, the role receiver Foundations Page 47 defines a cardinality of [1] while provider defines a cardinality of [0..∗]. Consequently, an instance of the multi role provider may communicate with 0to many receiver’s while any instance of the single role receiver may only communicate with exactly one provider. At runtime, an instance of a multi role contains of a set of subrole instances as shown in Figure 2.13. Each subrole instance is connected via a single-cast connector to one instance of the single role and manages the communication with it. Due to the singlecast connectors, each subrole instance may only exchange messages with one particular single role instance. :receiver :provider :receiver :receiver :DistanceTransmission protocol instance label role instance label role instance label role connector instance single role instance multi role instance subrole instance Figure 2.13: Instance of the RTCP DistanceTransmission (cf. [BDG+14b]) Multi role instances are ordered, i.e., there exists a total order of the subrole instances. One subrole instance is the first one in the ordering, another one is the last one in the order. Adjacent subrole instances in the order have a successor-predecessor relationship. In our example in Figure 2.13, we may assume that the top most subrole instance is the first one while the bottom most subrole instance is the last one. The subrole instance in the middle is the successor of the first one and the predecessor of the last one. 2.4.2 Real-Time Statecharts Real-Time Statecharts (RTSCs) as defined by Becker et al. [BDG+14b] are a combination of UML statemachines [Gro11c] and timed automata (cf. Section 2.2.1). Thus, they enable to specify hierarchical, state-based real-time behavior. Basically, RTSCs consist of states and transitions. They use clocks with corresponding invariants, time guards, and resets as defined for timed automata (cf. Section 2.2.1). In addition, they may use variables for storing data and operations for encapsulating complex computations. As in UML statemachines, states may define actions that are executed upon entering (entry event) or leaving (exit event) a state. As an example, we provide the RTSCs of the roles receiver and provider of the RTCP DistanceTransmission in Figures 2.14 and 2.15, respectively. They implement the behavior Page 54 Chapter 3 Both existing component models do not fulfill all of the aforementioned requirements. The component model by Burmester, Giese, and Hirsch provides no support for instantiating embedded components more than once. This and the fact that all software architectures need to be enumerated lead to large models, in particular, if a component may have several architectures at runtime. This makes the models hard to handle for a developer. The component model by Tichy does not distinguish between software components and feedback controllers in the type graph that is used for specifying component story diagrams. As a result, component story diagrams cannot specify the reconfiguration of feedback controllers. In addition, both component models do not enable to connect software components to feedback controllers and to establish connections between different AMS [HB14]. In this chapter, we derive a consolidated component model for MECHATRONICUML that combines the features of the two existing component models. In particular, we extend the concept of the type graph used by Tichy such that the component model may include feedback controllers and such that they may interact with software components. As a result, we can specify software architectures on the reflective operator and controller levels of the OCM. In addition, we extend component story diagrams such that they can reconfigure feedback controllers as defined by Burmester and Giese [GBSO04, Bur06, BGO06]. Finally, we provide a concept for establishing connections between AMS. As a result, our new component model enables for concise and formal specifications of components, their integration with feedback controllers, and their reconfiguration behavior. In the following, we illustrate our component model based on a software architecture for the driving module of a RailCab that includes the behavior for building convoys. The requirements for the convoy behavior have been presented in our technical report [Hei12]. In our example, we use ideas presented by Hirsch [Hir08], Tichy [Tic09], and Flaßkamp et al. [FHK+13]. These ideas have been significantly extended as part of this thesis. The remainder of this chapter is structured as follows. We start by defining how components (Section 3.1), component instances (Section 3.2), and reconfiguration operations (Section 3.3) are specified. Thereafter, we introduce our concepts for establishing connections between AMS (Section 3.4) and for specifying architectural constraints (Section 3.5). Next, we describe how the new component model has been implemented as part of the MECHATRONICUML Tool Suite (Section 3.6). Finally, we discuss related approaches (Section 3.7) and summarize the chapter (Section 3.8). 3.1 Modeling Components "A [..] component is a software element that conforms to a component model and can be independently deployed and composed without modification according to a composition MechatronicUML Component Model Page 55 standard." [HC01, p. 7] In accordance to UML [Gro11c], components are either implemented directly or they are assembled from other components. We refer to the former as atomic components and to the latter as structured components. In both cases, the internals of a component are hidden from the outside world. This is denoted as component encapsulation [SGM02]. Access to the capabilities or data of a component is only allowed via its ports. This enables to replace one component by another one with a compatible interface without affecting any other component in a system. In addition, component encapsulation is one of the key enablers of compositional verification [BCC98, GTB+03] because it guarantees that there may not exist more dependencies to other components than those captured by ports. We will exploit this in Chapter 5. Our component model explicitly distinguishes between component types and component instances. The component types are instantiated to component instances for representing the software architecture of a system. In the following, we refer to component types simply as components. We introduce component instances in detail in Section 3.2. We illustrate the specification of components and component instances based on examples given in concrete syntax. A formalization of the component model is given by a metamodel [SV06, ch. 4] whose abstract syntax is defined in Appendix D.1. The static semantics has been formalized based on constraints in the object constraint language (OCL, [Gro12]) that are contained in the metamodel. The OCL constraints are listed in the MECHATRONICUML language specification [BDG+14b]. In the following, we first introduce the different kinds of ports that we support in our component model (Section 3.1.1). They differ in the kind of information they process and in their purpose. Based on the different kinds of ports, we define different kinds of atomic components (Section 3.1.2) and structured components (Section 3.1.3). Thereafter, we define how components may be connected via their ports using connectors (Section 3.1.4). As an extension to the previous component models, our component model supports that a component may expose a set of component properties (Section 3.1.5) that we need for our reconfiguration concept presented in Chapter 4. The concepts presented in this section have successively been integrated into the MECHATRONICUML language specifications [BDG+11, BBD+12, BBB+12, BDG+14b]. 3.1.1 Ports In our component model, we distinguish between six kinds of ports based on their purpose and the kind of data they process. We use discrete and continuous ports as defined by Burmester and Giese [GBSO04, Bur06, BGO06]. Additionally, we use hybrid ports that enable to connect discrete software components and feedback controllers. Furthermore, we use broadcast ports for instantiating RTCPs between AMS. Finally, we use two kinds of reconfiguration ports, namely reconfiguration message ports (RM ports) and reconfiguration execution ports (RE ports), that enable to execute reconfigurations Page 56 Chapter 3 involving several component instances. Figure 3.1 summarizes the concrete syntax of the different kinds of ports. in-port out-port in/out-port discrete continuous hybrid n/A n/A RM/RE broadcast n/A n/A n/A n/A B RM RE (a) Mandatory Single Ports in-port out-port in/out-port discrete continuous hybrid n/A n/A RM / RE broadcast n/A n/A n/A n/A B n/A (b) Optional Single Ports in-port out-port in/out-port discrete continuous hybrid n/A n/A RM/RE broadcast n/A n/A n/A n/A n/A n/A n/A n/A n/A RM RE (c) Mandatory Multi Ports in-port out-port in/out-port discrete continuous hybrid n/A n/A RM / RE broadcast n/A n/A n/A n/A n/A n/A n/A n/A n/A n/A (d) Optional Multi Ports Figure 3.1: Kinds of Ports (cf. [BDG+14b]) Each port defines a cardinality that defines how many instances of it may be created in one component instance. The previous component models only supported three fixed cardinalities that defined that the port can be instantiated at most once ([0..1]), exactly once ([1]), or arbitrary often ([0..∗]). We extend the concept of cardinalities by enabling to specify precise cardinalities using an integer for lower and upper bound. Again, we allow ∗as an upper bound to indicate that the port may be instantiated arbitrary often. If the cardinality has a lower bound of 0, we call it an optional port and visualize it with unfilled triangles (cf. Figures 3.1b and 3.1d) according to Giese and Schäfer [GS13]. If the lower bound of the cardinality is greater or equal to 1, we call it a mandatory port and visualize it with filled triangles (cf. Figures 3.1a and 3.1c). Ports with an upper bound of 1are called single ports while ports with an upper bound greater than 1are called multi ports in accordance to Hirsch [Hir08, HHG08]. We visualize multi ports with a cascaded border line as shown in Figures 3.1c and 3.1d [Hir08, HHG08, Tic09]. MechatronicUML Component Model Page 57 In the following, we introduce the different kinds of ports in more detail. 3.1.1.1 Discrete Port Discrete ports send and receive asynchronous messages. Therefore, each discrete port defines a set of message types that it may send or receive. A message type has a name and an ordered set of typed, named parameters. In contrast to the existing component models, we do not provide explicit interfaces in terms of required and provided interfaces. Instead, we use a port-based specification of the interface where we directly assign message types to the ports [CSVC11]. This approach introduces flexibility that we need for introducing hierarchical reconfiguration in Chapter 4. If a discrete port only sends messages, it is an in-port which is denoted by a small triangle pointing "into" the component similar to the notation of Koala [vOvdLKM00]. If it only sends messages, it is an out-port as denoted by the small triangle pointing "outside" the component. If it both sends and receives messages, it is an in/out-port denoted by two embedded triangles. Discrete ports define a message buffer in the same fashion as a role of a RTCP (cf. Section 2.4.1). Each discrete port needs to refine a role of an RTCP (cf. Section 2.4.1). Then, the discrete port needs to send and receive the same message types as the role. In our concrete syntax, we enable to visualize the role that is refined by a port by a dashed line that is attached to the port as shown in Figure 3.5 on Page 63. Visualizing the refined role of a port is optional. A discrete port has a behavior specification in terms of an RTSC. The behavior that is defined by the port’s RTSC needs to be compliant to the behavior that is defined by the role. We describe how the RTSC of a role may be refined to an RTSC of a port in detail in Chapter 5. The RTSC of a multi port has the same structure as the RTSC of a multi role (cf. Section 2.4.2). 3.1.1.2 Reconfiguration Message Port and Reconfiguration Execution Port Reconfiguration message ports (RM ports) and reconfiguration execution ports (RE ports) are special kinds of discrete ports. We use these kinds of ports for realizing the communication that is necessary for our concept of transactional execution of reconfiguration in structured components as described in Chapter 4. In the concrete syntax, we visualize RM ports and RE ports by squares that embed the letter "RM" and "RE", respectively. Compared to discrete ports, RM ports and RE ports have extended interface specifications that provide additional information for the messages types that may be sent or received. We introduce the interface specification in detail in Section 4.3. Page 58 Chapter 3 RM ports and RE ports have message buffers and their behavior is defined by a RTSC as for discrete ports. However, RM ports and RE ports are always mandatory in/out ports. Both may be used as multi ports as we explain in Section 4.1. 3.1.1.3 Broadcast Port Broadcast ports are a special kind of discrete port. We use broadcast ports only for instantiating RTCPs between different AMS as explained in Section 3.4. In the concrete syntax, we visualize broadcast ports by squares that embed the letter "B". Analogously to discrete ports, broadcast ports define a set of message types that they may send and receive as well as a message buffer. Their behavior is defined by a RTSC. In contrast to discrete ports, broadcast ports are always in/out-ports and may only be used as single ports. In addition, they do not refine a role of a RTCP. 3.1.1.4 Continuous Port Continuous ports send (out-port) or receive (in-port) a signal value. "A signal is a time varying quantity that has values at all points in time" [Matf]. The data type of the signal must be a primitive data type or an array of primitive types. Continuous ports are either in-ports or out-ports. In addition, continuous ports may be optional, but we currently do not support continuous multi ports. In the concrete syntax, continuous ports are visualized as isosceles triangles where the top of the triangle either points into the component (in-port) or outside the component (out-port). 3.1.1.5 Hybrid Port Hybrid ports send (out-port) or receive (in-port) a signal value similar to a continuous port. They enable that a discrete component sends a signal to or receives a signal from a feedback controller. As for a continuous port, the data type of the signal must be a primitive data type or an array of primitive types. Thus, we define a new semantics of hybrid ports compared to Burmester [Bur06]. Burmester introduced hybrid ports as "multiple discrete and continuous ports as syntactic construct to reduce visual complexity" [Bur06, p. 56] but did not define them. Hybrid ports are either in-ports or out-ports. Then, the RTSC of the component may read (in-port) or write (out-port) the value of the hybrid port like a normal variable. In addition, hybrid ports may be optional, but we currently do not support hybrid multi ports. For keeping the behavior specification of a discrete component discrete, hybrid ports define a sampling interval. Then, the value of the signal only changes at the rate of the sampling interval and we do not make any assumptions on how the value may change. MechatronicUML Component Model Page 59 In the concrete syntax, hybrid ports are visualized as squares that embed an isosceles triangle. The top of the triangle either points into the component (in-port) or outside the component (out-port). 3.1.2 Atomic Components An atomic component directly contains a behavior specification and does not embed other components. Our component model distinguishes three kinds of atomic components that differ in their purpose and their behavior specification. In accordance to Burmester and Giese [GBSO04, Bur06, BGO06], we distinguish between discrete and continuous atomic components. Discrete atomic components define discrete, event-based behavior while continuous atomic components represent the feedback controllers of the system. In addition, we introduce a new kind of atomic component: the fading component [Vol13]. MemberControl refDist speedProvider member distReceiver (a) Discrete Atomic Component StandaloneDrive refSpeed curSpeed force (b) Continuous Atomic Component +- ConvoyFading standalone convoy force (c) Fading Component Figure 3.2: Kinds of Atomic Components Figure 3.2 illustrates the concrete syntax of the different kinds of atomic components. In accordance to the UML [Gro11c], components are represented by rectangles with a component icon in the upper right corner and a name label in the center. At the border of the component, we visualize the ports of the component. In contrast to the previous component models, we distinguish the different kinds of atomic components by using different component icons to increase semiotic clarity. Semiotic clarity requires that different semantic constructs of a language need to be represented by different graphical symbols for reducing the potential for misinterpretation [Moo09]. In the following, we introduce all three kinds of atomic components in more detail. 3.1.2.1 Discrete Atomic Component Discrete atomic components define the discrete, event-based real-time behavior of the system. As a result, a discrete component operates on time-discrete values and imple- Page 60 Chapter 3 ments message-based communication. Thus, discrete atomic components are used for defining the behavior of the reflective operator of the OCM. A discrete atomic component may use discrete ports for interacting with other components based on RTCPs. In addition, it may use hybrid ports for interacting with continuous atomic components (cf. Section 3.1.2.2) and broadcast ports if it implements the instantiation of RTCPs between AMS. If the component is reconfigurable, it has one RM port and one RE port. MemberControl MemberControl_Main member distReceiver speedProvider Synchronization1 Figure 3.3: Structure of a RTSC of a Discrete Atomic Component The behavior of a discrete atomic component is defined by a RTSC that has a fixed, hierarchical structure [Hir08, p. 133]. Figure 3.3 illustrates this structure for the component MemberControl shown in Figure 3.2a. The RTSC always contains one hierarchical state. This state contains one region for each discrete port that embeds the port’s RTSC. In the example, we obtain regions for the discrete ports member,distReceiver, and speedProvider. In addition, the RTSC may contain an arbitrary number of so-called synchronization RTSCs that may be used to synchronize the port RTSCs [GTB+03]. 3.1.2.2 Continuous Atomic Component Continuous atomic components represent the feedback controllers of the system that are located of the controller level of the OCM. They operate on time-continuous values that are represented by signals. Their behavior is typically defined "by block-diagrams, differential equations, or transfer functions" [Bur06, p. 56]. A continuous atomic component may only use continuous ports for exchanging signals with other components. In accordance to Burmester et al. [BGH+07], we only specify the interface of the continuous component based on its ports but not the component’s behavior. The behavior of continuous atomic components is specified in a control engineering tool such as MATLAB/Simulink [Matg]. As an example, consider the continuous atomic component StandaloneDrive shown in Figure 3.2b. It implements a feedback controller that lets a RailCab drive at a constant MechatronicUML Component Model Page 61 speed. It receives a reference speed via refSpeed and the current speed of the RailCab via curSpeed. By modifying force of the electric drive emitted via force, it modifies the speed of the RailCab such that curSpeed eventually equals refSpeed. This control strategy, however, needs to be implemented in MATLAB/Simulink. 3.1.2.3 Fading Component A fading component enables to switch between continuous component instances as part of a reconfiguration if the continuous component instances produce the same output signal. Thus, fading components operate on time-continuous values like continuous atomic components and are located on the controller level of the OCM. As an example, consider that the continuous component StandaloneDrive shown in Figure 3.2b is to be replaced by a continuous component ConvoyDrive as illustrated in Figure 3.4. The ConvoyDrive component implements a feedback controller that additionally considers a reference distance (refDist) and the current distance (curDist) to the preceding RailCab. It needs to be used by all RailCabs that are convoy members. Thus, any Rail- Cab that wants to join a convoy needs to perform this replacement at runtime as part of a reconfiguration. Physical Machine :StandaloneDrive :refSpeed :curSpeed :curDist :ConvoyDrive :refSpeed :curSpeed :refDist :force :force «destroy» «create» Figure 3.4: Illustration of Exchanging a Controller without Fading Function In general, continuous component instances must not be replaced instantaneously if they produce the same output signal such as force in Figure 3.4. In the figure, the green graphs illustrate the computed value of force over time while the vertical yellow bar denotes the point in time where the continuous component instances are replaced instantaneously. In this case, a jump in the value of the controlled variable force occurs at the engine and may damage it. For preventing such jumps, previous works integrated fading functions based on cross fading [BGO06] and flatness-based switching [OMT+08] into MECHATRONICUML. These are two strategies for smoothing the output signal while replacing continuous component instances. The actual behavior of the fading function or the flatness-based switching is specified in a control engineering tool such as MATLAB/Simulink [Matg]. Page 62 Chapter 3 In our component model, we encapsulate fading functions and flatness-based switching in fading components such as ConvoyFading shown in Figure 3.2c. The fading component has one continuous out-port for the output signal and one continuous in-port for any continuous component that may produce this output signal. Thus, ConvoyFading has one out-port force and in-ports standalone and convoy for the two continuous components StandaloneDrive and ConvoyDrive, respectively. In addition to the ports, the fading component defines a set of fading functions. Each fading function fades from the input signal of one in-port to the input signal of another inport. In the example in Figure 3.4, the ConvoyFading would need to fade from standalone to convoy. At this point, we do not need to distinguish whether the fading function implements a cross fading [BGO06] or flatness-based switching [OMT+08]. We only need to specify how long it takes to execute the fading function. If the fading component does not execute a fading function, it forwards the input signal unmodified to its out-port. 3.1.3 Structured Components Astructured component embeds other component types by means of component parts as defined in the component model by Tichy [Tic09]. Component parts are defined as an association to another component [Gro11c], i.e., the same component may be embedded multiple times in a structured component. Component parts define a name and a cardinality. Structured components only define a reconfiguration behavior but no functional behavior. This enables separation of concerns between reconfiguration behavior and functional behavior. According to McKinley et al. [MSKC04], this is one of the three key enablers for successfully developing self-adaptive systems. With respect to the OCM given in Section 2.1.2, structured components belong to the reflective operator. In contrast to the existing component models, our component model distinguishes between two kinds of structured components based on the kinds of components they embed. These are discrete structured components (cf. Section 3.1.3.1) and hybrid structured components (Section 3.1.3.2). The differentiation between two kinds of structured components is helpful for defining our transactional reconfiguration approach in Chapter 4. 3.1.3.1 Discrete Structured Component A discrete structured component (recursively) embeds discrete components only. Consequently, a discrete structured component may use all kinds of ports except continuous ports analogous to discrete atomic components (cf. Section 3.2a). Figure 3.5 shows an example of a discrete structured component named ConvoyCoordination. It contains the behavior of a convoy coordinator, i.e., it provides behavior for adding and removing RailCabs to/from the convoy and for announcing all acceleration MechatronicUML Component Model Page 63 and breaking maneuvers to the convoy members. ConvoyCoordination embeds two components ConvoyManagement and RefGen using two component parts named man and ref- Gen, respectively. Both of which are discrete components. ConvoyCoordination man : ConvoyManagement [1] coordinator coordinator refDistProvider refDistProvider refGen : RefGen [1..*] speedProvider speedProvider prev next strategy receiver curPoscurPos profileProvider profileReceiver ConvoyCoordination.coordinator DistanceTransmission.provider StrategyTransmission.receiver SpeedTransmission.provider Figure 3.5: The structured component type ConvoyCoordination Our component model allows for a precise specification of cardinalities using integers for lower and upper bound, but still enables to use an asterisk to support an arbitrary number of instances. Supporting precise cardinalities is especially useful for simulations in a simulation tool as MATLAB/Simulink as presented in Chapter 6. In Figure 3.5, the component part man has a cardinality of [1]. That means any instance of ConvoyCoordination contains exactly one instance of ConvoyManagement. We call this a single part. refGen has a cardinality of [1..∗]such that an instance of ConvoyCoordination has arbitrary many but at least one instance of RefGen. In accordance to Tichy, we call this a multi part. In the concrete syntax, multi parts are visualized by a cascaded border line [Tic09, p. 38]. In ConvoyCoordination, the ConvoyManagement is responsible for adding and removing convoy members to the convoy and for negotiating the maximum speed of the convoy. The interaction with the convoy members is implemented in the port coordinator that refines the role coordinator of the RTCP ConvoyCoordination [FHK+13, FHK+14]. We present the RTCP ConvoyCoordination in Appendix A.1.2. For each convoy member, the ConvoyCoordination has one instance of the RefGen multi part that generates reference data for the convoy member (cf. [Tic09]). RefGen receives information about the corresponding convoy member and the negotiated speeds from ConvoyManagement via profileReceiver. The information about the convoy members is encapsulated in so-called profiles [Hir08, FHK+13, FHK+14]. The RefGen instance for the first convoy member additionally receives the position of the coordinator RailCab via curPos. Then, RefGen computes a reference distance to the preceding RailCab based on the position of this preceding RailCab and the profile of the RailCab. This can be used to adapt the distances between RailCabs within the convoy to changing environmental conditions such as higher speeds, strong wind, or slopes. RefGen sends the new refer- Page 70 Chapter 3 parent component instance. Port instances of structured component instances have an additional delegation connector instance to a port instance of an embedded component instance. Continuous and hybrid port instances need to fulfill the same properties, but two exceptions apply. A continuous or hybrid out-port may have more than one outgoing connector instance, i.e., the signal value may be send to several other component instances. In addition, continuous in-ports of a structured component instance may be delegated to several embedded component instances. A continuous or hybrid port instance may also have no connector instance if it is directly attached to hardware as, e.g., instances of the port force of VelocityController. In any case, component instances that are embedded in a structured component instance may only be connected by connector instances if the corresponding port types are connected by a connector in the structured component type. In addition, our component model uses three implicit composite aggregations for component instances. First, a component instance that is embedded in a structured component instance cannot exist without its parent. Second, a port instance cannot exist without its surrounding component instance. Third, a connector instance cannot exist without being attached to exactly two port instances [Tic09, p. 42]. Figure 3.10 shows an instance of ConvoyCoordination that is executed in a coordinator RailCab with one member. It contains an instance cm of type ConvoyManagement and, since the convoy has one member, one instance rg1 of type RefGen. Since rg1 is associated to the first convoy member, it receives the current position of the coordinator RailCab via curPos. Furthermore, cc has instances of the coordinator and refDistProvider multi ports for communicating with the member. cc : ConvoyCoordination cm / man : ConvoyManagement rg1 / refGen : RefGen :curPos:curPos r1:refDistProvider :refDistProvider c1:coordinator c1:coordinator :speedProvider :speedProvider :strategy :receiver p1:profileProvider :profileReceiver Figure 3.10: Component Instance of Component ConvoyCoordination for a Convoy with 1 Member Hirsch [Hir08] and Tichy [Tic09] did not distinguish between single port instances and multi port instances in the concrete syntax. However, a multi port instance has the same structure as a multi role instance (cf. Section 2.4.1), i.e., it contains several subport instances that belong together. Therefore, we propose to visualize the multi port instance by a dashed square that groups its subport instances as shown for the instances of coordinator,refDistProvider, and profileProvider in Figure 3.10. The subport instances are visualized as port instances as before. MechatronicUML Component Model Page 71 We present additional component instances for coordinator RailCabs and member Rail- Cabs in Appendix A.4. 3.3 Modeling Reconfiguration The existing component models defined two modeling languages for specifying reconfiguration behavior of reconfigurable structured components. The component model by Tichy uses component story diagrams (CSDs, [THHO08, Tic09]), which enable a rule-based specification of reconfiguration behavior based on story diagrams (cf. Section 2.3.2). They enable formal, modular, and concise models. In contrast, hybrid reconfiguration charts as proposed by Burmester and Giese [GBSO04, BGO06, Bur06] provide a state-based model where each state contains one configuration of a structured component instance. Hybrid reconfiguration charts quickly become very large and unmaintainable if a component instance has several configurations. This is the case, for example, for the component ConvoyCoordination in Figure 3.5 where we have a sequence of RefGen instances that reflects the order of the convoy members on track. As a result, we chose to use CSDs for specifying reconfiguration of structured and atomic component instances in our component model. We refer to Schubert [Sch12] and our technical report [HB14] for a detailed comparison of hybrid reconfiguration charts and CSDs. In the following, we first introduce CSDs as they have been defined by Tichy (cf. Section 3.3.1). Thereafter, we introduce three extensions to CSDs that we developed as part of this thesis. These are controller exchange nodes (cf. Section 3.3.2), constraints for multi port variables (cf. Section 3.3.3), and CSDs for atomic components (cf. Section 3.3.4). These extensions add features to CSDs that are necessary for specifying reconfiguration behavior in our component model. We illustrate these features based on examples given in concrete syntax. A formalization of CSDs is given by a metamodel [SV06, ch. 4] whose abstract syntax is defined in Appendix D.2. The static semantics has been formalized based on OCL constraints [Gro12]. The operational semantics of CSDs has already been defined by Tichy [Tic09, pp. 71ff] in form of a translational semantics [SK95] by defining a transformation of CSDs to story diagrams. Our extensions only extend the type system that is used for the story diagrams and do not require a new definition of the operational semantics. 3.3.1 Component Story Diagrams In our component model, we use CSDs [THHO08, Tic09] for modeling reconfiguration of component instances. Each component contains a set of CSDs that define how instances of the component may be reconfigured at runtime. We define how and when CSDs are executed for a component instance in Chapter 4. CSDs are based on story diagrams (cf. Section 2.3.2.2) and support the same constructs for specifying control flow including a set of input and output parameters. The Page 72 Chapter 3 story nodes of a CSD, however, contain component story patterns instead of story patterns [Tic09]. A component story pattern defines the modification of a component instance and, in case of a structured component instance, its embedded CIC. We use the components that are defined in our component model as a type graph to type the variables of the component story pattern. Then, all variables and links of the component story pattern are typed by the components, ports, and connectors that are defined by the component model. Thereby we can ensure that component instances remain syntactically correct after applying a component story pattern. In particular, we can ensure that a component story pattern can only be executed if its modifications do not violate the cardinalities of ports and component parts. Each component story pattern contains exactly one this component variable. The this variable is typed by the component that contains the corresponding CSD. At runtime, the this variable is automatically bound to the component instance that invoked the CSD on itself. Thus, it is a implicit input parameter of any CSD [Tic09]. Figure 3.11 shows a CSD becomeMember of the component RailCabDriveControl. The CSD reconfigures an instance of RailCabDriveControl of a RailCab driving alone (cf. Figure 3.9) to an instance of a RailCab driving as a member of a convoy (cf. Figure A.31). The CSD has two story nodes. In the first story node, we match the embedded component instances of types OperationStategy,DriveLogic, and VelocityController. We destroy the assembly connector instance between os and dl. In addition, we invoke the reconfiguration applyMemberStrategy on os that destroys the speedProvider port instance. We explain this CSD in more detail in Section 3.3.4. In addition, we invoke the reconfiguration switchToConvoy on vc that reconfigures the feedback controllers for driving as a convoy member. We introduce this CSD in more detail in Section 3.3.2. In the second story node, we create an instance of MemberControl. In addition, we create an instance of DistanceSensor and connect it to vc by an assembly connector instance. Finally, we create port instances of member and refDistReceiver on this and connect all port instances of mc. A CSD may specify invocations of further CSDs on embedded component instances. The invocation is directly attached to the corresponding component variable [Tic09, p. 62] as shown in the first story node of the CSD becomeMember in Figure 3.11. We define how such invocations are executed with respect to the component hierarchy in Chapter 4. In our component model, we restrict CSDs such that they respect component encapsulation. In particular, we forbid that a CSD directly creates or destroys port instances of embedded component instances as it is allowed by Tichy [Tic09, p. 55]. Such port instances may only be created by the embedded component instance itself. The corresponding CSD that creates the port instance needs to be invoked on the embedded component instance as shown in Figure 3.11. MechatronicUML Component Model Page 73 this Switch Operation Strategy and destroy Assembly Create MemberControl and Sensor, Connect Ports mc / member : MemberControl this vc :curDist :refDist :refDist dl :speedProvider :member :member :distReceiver :refDistReceiver :maxSpeed ds / dist : DistanceSensor :distance «create» «create» «create» «create» «create» «create» «create» «create» os / strategy : OperationStrategy applyMemberStrategy() dl / drive : DriveLogic :maxSpeed :speedProvider «destroy» vc / ctrl : VelocityController switchToConvoy() RailCabDriveControl::becomeMember() Figure 3.11: CSD for Component RailCabDriveControl that Reconfigures the Component Instance to Serve as a Member In accordance to Tichy, a component may define one or more constructor CSDs. A constructor CSD defines how instances of the component are initialized upon instantiation. Then, a component variable with stereotype «create» may invoke a constructor [Tic09, p. 62]. In addition, every component defines an implicit constructor that instantiates all ports and embedded components according to their minimum cardinality. The implicit constructor is always used if no explicit constructor is invoked for a coponent variable with stereotype «create». In Figure 3.11, we used implicit constructors for both, ds and mc. We provide an example of an explicit constructor in Appendix A.6.2. 3.3.2 Controller Exchange Nodes The component model by Tichy does not distinguish between different kinds of components [Tic09]. Consequently, it does not enable to use fading functions, which are typically required when replacing continuous component instances as explained in Section 3.1.2.3. Page 74 Chapter 3 As a solution, Schubert [Sch12] introduced controller exchange nodes for enabling the reconfiguration of continuous components. A controller exchange node is a special kind of story node that enables safe execution of fading functions. It has a fixed structure that consists of exactly three component variables. Two of which reference continuous components where one is destroyed and one is created. The third component variable refers to the fading component that is connected to the two continuous components. The component variable referring to the fading component additionally specifies which fading function needs to be executed. Perform fading to convoy controller VelocityController::switchToConvoy() +- [150 ms;180 ms] +- this sd / standalone_ctrl : StandaloneDrive :refSpeed :curSpeed :curDist cd / convoy_ctrl : ConvoyDrive :refSpeed :curSpeed :refDist :force :force :curDist :refSpeed :curSpeed :refDist f / fade : ConvoyFading fadeToConvoy() :standalone :convoy «destroy» «create» «create» «create» «create» «create» «create» «destroy» «destroy» «destroy» «create» «create» Figure 3.12: CSD for Component VelocityController that Reconfigures the Component Instance to Serve as a Member Figure 3.12 shows the CSD switchToConvoy that uses a controller exchange node. It is invoked by becomeMember and reconfigures an instance of VelocityController such that it uses an instance of ConvoyDrive instead of StandaloneDrive. Consequently, it destroys the latter and creates a new instance of the former. Since both continuous components provide a signal force, we need to use the fading component ConvoyFading to fade between both signals. In the controller exchange node of switchToConvoy, we therefore select the fading function fadeToConvoy for the reconfiguration as specified within the fading component variable. As indicated in the upper right corner of the controller exchange node, the fading takes between 150 ms and 180ms. 3.3.3 Constraints for Multi Port Variables Multi ports are ordered, i.e., the subport instances are arranged in a sequence as it has been defined for multi roles (cf. Section 2.4.1). Up to now, this order cannot be used in MechatronicUML Component Model Page 75 component story pattern, for example, for creating a subport instance as a successor of another subport instance. As an example, consider the component ConvoyCoordinator shown in Figure 3.5 on Page 63. The subport instances of an instance of the multi port coordinator shall have the same order as the corresponding convoy members on track. Thus, if a new member joins the convoy at a particular position, we need to insert a subport instance at the same position into the multi port instance. Therefore, we extend component story patterns by constraints for multi port variables that refer to the order of the subport instances [Hei14]. They are inspired by so-called link constraints of story diagrams [vDHP+12a]. In accordance to these link constraints, we distinguish between multi port position constraints and multi port order constraints. Both of which are illustrated in Figure 3.13. Order Constraints ... ... :port1 this «next» «first» «last» Figure 3.13: Order Constraints for Multi Port Variables A multi port position constraint enables to refer to the first (or last) subport instance of a multi port instance. In our concrete syntax, we visualize it by attaching a stereotype «first» (or «last») to the corresponding subport variable. In Figure 3.13, the upper subport variable matches the first subport instance while the lower subport variable matches the last subport instance. A multi port order constraint enables to refer to the relative order of the subport instances. We enable to define that a subport instance is a direct successor (or predecessor) of another subport instance. In our concrete syntax, we visualize these constraints by a dashed arrow annotated with the stereotype «next» (or «prev») to denote that the target subport instance is a direct successor (or direct predecessor) of the source subport instance. In Figure 3.13, the lower subport instance has to be a direct successor of the upper subport instance of the multi port instance of type port1 for successfully matching the component story pattern. Multi port position constraints and multi port order constraints may be part of the LHS or RHS of the component story pattern. A multi port position constraint is part of the LHS if it is attached to a subport variable with no stereotype or with stereotype «destroy».In this case, the matched subport variable needs to fulfill the multi port position constraint for a successful matching. A multi port position constraint is part of the RHS if it Page 76 Chapter 3 int i := 1; if (next != null){ tmpRefGen := next; next := null; tmpC := c; c := null} [i < position] i++; [success] [else] [else] [position == 1] [failure] cPort := newC, rPort := newR ConvoyCoordination::addConvoyMemberAtPos(int position) : (coordinator cPort, refDistProvider rPort) Get next RefGen cm tmpC this tmpRefGen c:coordinator «next» next / refGen : RefGen :next :prev tmpP:profileProvider :profileReceiver Create Embedded Ports cm (embC, embP) := createMemberPortsAfter(tmpC, tmpP) this Create Embedded Ports cm (embC, embP) := createFirstMemberPorts() this Create RefGen cm this tmpRefGen c newRefGen / refGen : RefGen :next :prev :refDistProvider :refDistProvider «create» «create» :refDistProvider newR: refDistProvider «next» «create» «create» embP :profileReceiver «create» newC:coordinator «create» «create» next / refGen : RefGen :next :prev tmpC :refDistProvider :refDistProvider «next» «create» «destroy» «next» «next» embC Create RefGen at Beginning cm this newRefGen / refGen : RefGen embC «next» tmpRefGen :next :prev :curPos:curPos newR: refDistProvider :refDistProvider «first» «create» «create» «create» «create» :refDistProvider :refDistProvider «next» «create» :curPos :curPos «destroy» «destroy» «destroy» «create» embP :profileReceiver «create» newC: coordinator «first» «create» «create» «first» Get first RefGen cm / man : ConvoyManagement tmpC:coordinator this «first» tmpRefGen / refGen : RefGen :curPos:curPos Figure 3.14: CSD for Adding a Convoy Member (cf. [Tic09, Sch12]) MechatronicUML Component Model Page 77 is attached to a subport variable with stereotype «create». In this case, the created subport instance is inserted at the specified position into the multi port, i.e., either at first or last position. A multi port order constraint is part of the RHS if at least one of the attached subport variables carries a «create» stereotype. It is part of the LHS in all other cases. It is not allowed to connect a subport variable stereotyped with «create» and a subport variable stereotyped with «destroy» by a multi port order constraint. Figure 3.14 shows an example of a complex CSD of the component ConvoyCoordination that implements the aforementioned use case of adding a new convoy member at a specific position of the convoy. The CSD takes a position as its input and returns the subport instances that have been created for the multi ports coordinator and refDistProvider of ConvoyCoordination. In addition to the subport instances, the CSD also creates an instance of the RefGen multi part. The behavior of the CSD addConvoyMemberAtPosition is as follows. The first story node matches the first RefGen instance which is the only one having an instance of the curPos port. Matching this story node will always succeed because the corresponding component parts are both mandatory. Thereafter, the statement node initializes a counter variable ithat is used for iterating over the list of RefGen instances until the instance at the position given as parameter has been found. The iteration is performed via the story node and the two statement nodes in the upper right corner. The component story pattern in the story node uses a multi port order constraint for iterating over the subport instances of coordinator. If the correct position has been found, the story node in the lower left corner inserts an instance of refGen at the beginning of the list, while the story node in the lower right inserts an instance of refGen at any other position. Along with the instance of RefGen, we create subport instances for the multi ports coordinator and refDistProvider of this and insert them at the corresponding positions. In the story node Create RefGen at Beginning, we use the «first» stereotype two times within the same multi port variable. This is allowed because one is part of the LHS for matching the previously first subport instance while the other one is part of the RHS. Finally, the final node assigns the created subport instances newC of type coordinator and newR of type refDistProvider to the output parameters cPort and rPort, respectively. 3.3.4 Reconfiguration of Atomic Components In our component model, we use CSDs for reconfiguring atomic components as well. Tichy neither explicitly defined nor restricted CSDs in that way [Tic09]. The only difference to a CSD of a structured component is that we visualize the this component variable as an atomic component. Then, the this component variable may only contain port variables but no embedded component variables (cf. [BDG+14b]). Figure 3.15 shows the CSD applyMemberStrategy that is invoked in the first story node of becomeMember shown in Figure 3.11. OperationStrategy is an atomic component and, Page 78 Chapter 3 Delete speedProvider Port OperationStrategy::applyMemberStrategy() this «destroy» :speedProvider Figure 3.15: CSD for Component OperationStrategy that Reconfigures the Ports for Being Member therefore, the this variable has no embedded component variables. The CSD deletes the speedProvider port instance because the reference speed of a member is defined by the coordinator and not by its own operation strategy. 3.4 Instantiating Real-Time Coordination Protocols on System Level RTCPs on the system level define the communication between different AMS while they collaborate in an NMS. Since NMS are virtual, there does not exist a component that contains both AMS and that may instantiate an RTCP between the AMS. Consequently, the instantiation cannot be described by CSDs, but the AMS need to agree on instantiating a particular RTCP via message-based communication. This, however, requires at least one of the AMS to know about the existence of the other AMS. Then, one of the AMS may initiate the communication for agreeing on the instantiation. This communication, however, cannot be handled by the discrete ports and connectors introduced in Section 3.1 because their instances already require a connector with a RTCP. For solving this problem, we need to relax the strict requirement of MECHATRONICUML that all communication between AMS is exclusively handled by RTCPs with single-cast connectors [GTB+03, EHH+13]. In particular, we use broadcast ports as introduced in Section 3.1.1.3 that enable for broadcast communication. Whenever an AMS sends a message via a broadcast port, the message is received by all other broadcast ports "in reach" that can process this message. Which broadcast ports are in reach depends on the spatial distribution of the AMS as well as the transmission medium. In general, it is not known at design time which ports will receive a message and which will not. In order to retain the safety guarantees provided by the use of RTCPs, we only allow the use of broadcast ports for two special purposes. First, for gaining knowledge about the existence of other systems and, second, for instantiating one particular RTCP called ProtocolInstantiation. This RTCP then enables to instantiate further RTCPs. No further broadcast ports are allowed in a MECHATRONICUML model. MechatronicUML Component Model Page 79 Following the terminology of Baresi et. al. [BDNG06], gaining knowledge about other systems is only required in so-called open-world scenarios. In an open-world scenario, systems do not know each other in advance and the possible communication partners change frequently over time. For example, RailCabs move along the track system and do not know when or where they meet which other RailCab. In this case, we may need to use a broadcast port that executes a so-called discovery protocol [NNSS07] that detects and gathers knowledge about the systems in the environment. This information needs to be stored in an environment model that may be used by the cognitive operator of the OCM for deciding which other systems are suitable for which cooperation. We present a simple discovery protocol and environment model in Appendix A.2.1, but we do not consider this use case in detail as part of this thesis. In the following, we illustrate how we use a broadcast port for instantiating the RTCP ProtocolInstantiation for two AMS (Section 3.4.1). Thereafter, we show how to use the RTCP ProtocolInstantiation for instantiating further RTCPs (Section 3.4.2). 3.4.1 Instantiating the RTCP ProtocolInstantiation An AMS may use its protocolInst broadcast port for contacting another AMS for instantiating a connector including the ProtocolInstantiation RTCP. ProtocolInstantiation is the only RTCP that may be instantiated via broadcast communication. All other RTCPs need to be instantiated via ProtocolInstantiation or as part of another, user-defined RTCP. Assumptions For instantiating the RTCP ProtocolInstantiation, the AMS that initiates the instantiation needs to know the other system in its environment model. Based on this, we apply the following assumptions to the instantiation process: 1. Each AMS has a unique ID that is known to the RTSC of the broadcast port. 2. There may exist different versions of this message exchange that only differ in their timing constraints as, e.g., timeouts, where each version has a unique identifier. The broadcast port knows the ID of the version that it implements. 3. The IDs are represented using a data type that can be sent as a parameter of a message. 4. No message loss occurs during the interaction. 5. No eavesdropper tries to compromise or prevent the connection setup. Since the different versions only differ in their timing constraints, the message exchange for instantiating the RTCP ProtocolInstantiation may be used in different systems without modification. Page 86 Chapter 3 cc, ps then 0 RailCabDriveControl::isStandalone this cc / convoy : ConvoyCoordination :curPos ps / pos : PositionSensor :position mc this mc / member : MemberControl then else 01 else Figure 3.20: Component SDD isStandalone for Component RailCabDriveControl evaluation needs to terminate at a (1)-node for any matching that can be obtained for the universal pattern node. The invariant component SDD convoyOrder shown in Figure 3.21 specifies that any two successive subport instances of refDistProvider are delegated to successive subport instances of ConvoyCoordination. This ensures that reference speeds and distances can always be distributed within the convoy in the right order. In the component SDD, the first pattern node matches an instance of ConvoyCoordination that is embedded in RailCab- DriveControl. The second pattern node is a universal pattern node that matches all pairs of successive refDistProvider port instances. For any match that may be obtained for this pattern node, the third pattern node needs to be matched as well such that the execution terminates at the (1)-node. If there exists no matching for the universal pattern node, then the component SDD is fulfilled. For this reason, we only visualize one outgoing then-edge for an universal pattern node as a shorthand notation [Sta08, p. 63]. A component SDD may require that an embedded component instance has a component property with a particular value. This component property may be specified, again, using a component SDD. This enables to connect architectural constraints through the different hierarchy levels of the component model. In Figure 3.21, the part variable cc in the universal pattern node requires that the component property convoyOrder is true for the component instance matched to cc. MechatronicUML Component Model Page 87 1 cc then «invariant» RailCabDriveControl::convoyOrder rdp1, rdp2 this cc [convoyOrder] rdp1:refDistProvider «next» rdp2:refDistProvider this cc / convoy : ConvoyCoordination then else rdp3, rdp4 this cc rdp1 rdp2 rdp3:refDistProvider «next» rdp4:refDistProvider then else 01 Figure 3.21: Component SDD convoyOrder for Component RailCabDriveControl Page 88 Chapter 3 3.6 Implementation The concepts presented in this chapter have been implemented as part of the MECHATRONICUML Tool Suite1[DGB+14]. We have built a metamodel (cf. Appendix D) and several diagram editors for creating models based on our component model. In contrast to the previous version of the tool, called Fujaba Real-Time Tool Suite [PTH+10], the metamodel has been developed using the Eclipse Modeling Framework (EMF, [SBPM08]). The static semantics has been completely encoded in the metamodel using OCL [Gro12]. Figure 3.22 provides a conceptual overview of the Eclipse plugins that have been created. «de.uni_paderborn.fujaba» muml «org.storydriven» storydiagrams «de.uni_paderborn.fujaba.muml» reconfiguration «de.uni_paderborn.fujaba.muml» componentstorypattern «de.uni_paderborn.fujaba.muml» componentstorydiagram «de.uni_paderborn.fujaba.muml.verification.sdd» componentSDD «de.uni_paderborn.fujaba.muml» component.diagram «de.uni_paderborn.fujaba.muml» componentinstance configuration.diagram «de.uni_paderborn.fujaba.muml» reconfiguration.ui «de.uni_paderborn.fujaba.muml.verification.sdd» componentSDD.diagram «de.uni_paderborn.fujaba.muml» componentstorydiagram.diagram «extends» «extends»«extends» «extends» «extends» «extends» «extends» «extends» «uses» «uses» «uses» «uses» «uses» «package» plugin name «package» plugin name Legend: Metamodel Plugin Diagram Editor Plugin Figure 3.22: Plugins Implementing the Concepts of the Component Model The plugin muml contains the core metamodel of MECHATRONICUML. It enables to specify components and CICs including RTCPs and RTSCs. In muml, we only support non-reconfigurable components in order to have a core language that can be used for simple, non-adaptive systems. Reconfigurable components are modeled in the plugin reconfiguration. This plugin also contains the metamodel for broadcast ports. The metamodel for CSDs has been split into two plugins. The first one, called componentstorypattern, enables to specify component story patterns based on reconfigurable components. The componentstorydiagram plugin adds the story nodes that are special for CSDs. The metamodel for CSDs extends the story diagram metamodel [HRvD+11] contained in the plugin storydiagrams and reuses as much of the implementation as possible. In addition, we reuse the componentstorypattern metamodel for specifying component SDDs. The corresponding plugin componentSDD only defines the nodes and edges of component SDDs and uses the same component story pattern implementation as CSDs. We present class diagrams for our metamodels in Appendix D. 1https://trac.cs.upb.de/mechatronicuml MechatronicUML Component Model Page 89 Based on the metamodels, we developed four diagram editors using the graphical modeling framework (GMF, [Gro09]). In particular, we created editors for specifying components, CICs, CSDs, and component SDDs. The reconfiguration.ui plugin extends the component editor such that it may also be used for modeling reconfigurable components. At present, our implementation does not yet support the specification component properties for a component. Component SDDs are currently only used as part of our transactional reconfiguration approach as discussed in Chapter 4. Statement nodes of CSDs are not yet supported as well. 3.7 Related Work This section relates our new component model for MECHATRONICUML to other approaches for defining software architectures. First, we compare it to other software component models (Section 3.7.1). Second, we relate it to architecture description languages (ADLs, [MT00]) for self-adaptive systems (Section 3.7.2). Finally, we discuss related works regarding the specification of architectural constraints for a componentbased system (Section 3.7.3). 3.7.1 Software Component Models The surveys by Lau [LW07] and Crnkovi´ c et al. [CSVC11] review different kinds of component models. They distinguish between general purpose component models as, for example, CORBA [Gro11a] and EJB [Ora13], and specialized component models for particular domains. The latter usually address business information systems or embedded real-time systems. In this section, we focus primarily on component models for embedded real-time systems and on component models that support runtime reconfiguration. Hošek et al. [HPB+10] surveyed component models for embedded real-time systems. Only few of which support runtime reconfiguration including SOFA-HI, MyCCM-HI, ProCom, BlueArX, and AUTOSAR. All of these component models are restricted to mode changes [HKMU06] where a component instance moves from one implementation to another one. SOFA-HI [PWT+08, PKH+11] is an extension of the SOFA 2.0 [HP06, HB07] component model for real-time systems. It enables to specify hierarchical components that are considered to be implemented manually in C. In contrast to SOFA 2.0, reconfigurations in SOFA-HI cannot change connectors at runtime [PWT+08, HPB+10]. MyCCM-HI [BFHP09] extends the OMG CORBA Component Model (CCM, [Gro11a]) for specifying adaptive embedded systems with a textual syntax. It enables a detailed specification of tasks and their activation but does not define how the behavior of tasks is implemented. A mode change of a structured component may reconfigure connectors. The BlueArX component model by Bosch [KKH+08, KRKH09] also provides the specification of hierarchical components with mode changes. In BlueArX, the behavior Page 90 Chapter 3 of a component is defined by signal flows. In addition, each component defines a set of tasks including a scheduling of these tasks. A mode switch may either change the signal flow inside a component or it may change the task scheduling. Mode changes cannot be composed hierarchically. The ProCom component model [VSC+09] has recently been extended to support hierarchical reconfiguration based on mode changes as well [HQCH13]. We discuss this approach in detail in Section 4.8 along with our transactional reconfiguration approach. For automotive systems, the AUTOSAR standard [FMB+09] defines a component model for specifying hierarchical components. AUTOSAR does not specify how application software components are implemented [AUT14c]. As of version 4.0, AUTOSAR supports modes [AUT14a] and a timing specification [AUT14b]. Modes only enable to activate and deactivate trigger events in atomic software components thereby changing their behavior. The timing specification enables to define periods and orders for events as well as end-to-end deadlines for chains of events. All of these component models have in common that they do not provide means to specify and verify asynchronous message-based communication with real-time properties and that they only provide limited reconfiguration capabilities. In contrast, CSDs of MECHATRONICUML provide a more powerful and flexible specification of reconfigurations that includes control flow and reconfigurations across different levels of hierarchy (see also Chapter 4). Fractal [BCL+06, LLC10] provides the definition of hierarchical components including runtime reconfiguration of structured components. Each component consists of a membrane and a content area. The content area embeds other components while the membrane contains so-called controllers that enable introspection and reconfiguration. Although Fractal provides a C-implementation called Think [AHJ+09], it does not provide the ability to specify clock-based real-time properties for components or to verify the functional behavior or the reconfiguration specification. The DEECo component model [BGH+13] provides non-hierarchical components for soft real-time systems based on ensembles. While being in an ensemble, components may communicate and exchange knowledge. The communication, however, is not explicitly modeled in their approach. Components declaratively specify conditions for being part of an ensemble and a shared runtime framework automatically constructs and dissolves ensembles based on these conditions. De Nicola et al. [DNFLP13] present a textual language named SCEL that enables to express these conditions as policies including the necessary modifications of the software architecture for establishing the ensemble. In contrast to MECHATRONICUML, both approaches neither provide further reconfigurations of components and nor real-time constraints in their behavior specification. In [BBCP13], Barnat et al. introduce DCCL that is a formal component specification implementing the concepts of DEECo. They provide an LTL model checking of ensembles proving properties concerning the knowledge of components but not their behavior or the structure of the ensembles. CompoSE [KKTS09, ASTPH10] defines a hierarchical component model for modeling embedded systems. Atomic components may be implemented in a different language MechatronicUML Component Model Page 91 comparable to our continuous components. Each atomic component defines a set of configurations each consisting of a set of ports and a computation that defines the behavior. Structured components specify configurations based on combinations of ports and embedded component instances. At runtime, a component may switch between configurations. In contrast to MECHATRONICUML, the approach does not support using fading functions and message-based communication. EAST-ADL2 [CFJ+10] is an architecture description language targeted to the development of automotive systems. It provides a component specification where components refer to an external implementation, e.g., specified in MATLAB/Simulink [Matg]. The component model can be mapped to the AUTOSAR component model but does not yet support modes. Similar to MECHATRONICUML, it focuses on the integration of feedback controllers but provides no means for formal verification or runtime reconfiguration. Other component models for embedded real-time systems like Koala [vOvdLKM00], Robocop [Maa05], SaveCCM [CHP06, ÅCF+07], Rubus [HMTN+08], COMDES-II [KSA07], PECOS [GCW+02], and CHESS [PV14] provide the ability to specify realtime behavior on a low level of abstraction. They support formal analysis as our component model but neither support message-based communication (except COMDES-II) nor runtime reconfiguration. All of the mentioned approaches except DEECo do not provide a concept for instantiating connectors on system level. 3.7.2 ADLs for Self-Adaptive Systems ADLs [MT00] specify software architectures based on components and connectors, although the term component is less strictly defined as for component models. Connectors define the interaction of components, constraints define restrictions that the architecture needs to follow while it evolves, and architectural styles are families of related architectures [GMW00]. Bradbury et al. [BCDW04] survey ADLs that enable runtime reconfiguration of the software architecture. They classify these ADLs into three categories: graph-based, process algebra-based, and formal logic-based. Graph-based approaches define an initial configuration that is modified by graph rewriting rules. Examples include CHAM [IW95] and the approaches by Le Métayer [LM98] and Hirsch et al. [HIM98]. MECHATRONICUML also belongs to this category. Process algebra-based approaches like Dynamic Wright [ADG98], Darwin [KM98], or the approach by Bartels and Kleine [BK11] specify processes for each configuration using a process algebra like the π-calculus [MPW92] (Darwin) or CSP [Hoa85] (Dynamic Wright, Bartels and Kleine). At runtime, components switch between processes to execute reconfigurations. Formal-logic-based approaches like the approach by Aguirre and Maibaum [AM02] or GeReL [EW92] declaratively specify component behavior and constraints based on first-order logic. All of Page 92 Chapter 3 the mentioned approaches rely on a textual specification and enable checking for architectural constraints. However, they do not support real-time constraints for functional or reconfiguration behavior. Most approaches discussed above (except Darwin and GeReL) do not support structured components. The approach by Kacem et al. [KKJ12] specifies a system model using UML 2.0 components [Gro05]. They specify reconfigurations by graph transformations using the concrete syntax of components that are guarded by OCL constraints [Gro12]. In contrast to MECHATRONICUML, they do not support control flow in their rules. They support verifying constraints by translating their specification to Z [Spi92]. In contrast to MECHATRONICUML, they do not support hierarchical components and real-time properties. 3.7.3 Constraint Languages We compare our approach for modeling architectural constraints by component SDDs to two kinds of constraints languages. First, we compare it to object-based constraints languages that are defined based on classes and objects (cf. Section 3.7.3.1). Second, we compare component SDDs to constraint languages that were defined based on components, mostly as part of an architecture description language (cf. Section 3.7.3.2). 3.7.3.1 Object-Based Constraint Languages Approaches in this category enable to specify constraints for approaches that are based on classes, references, and objects. Probably the most well-known example is OCL [Gro12]. OCL supports the textual specification of complex structural properties for classes, e.g., using iterators, sets, and selections. In [FHTW05], Fish et.al. compare two visualizations of OCL: visual OCL [BKPPT01, KTW02] and constraint diagrams [Ken97]. Visual OCL uses a graph-based syntax for visualizing OCL constraints which is derived from the UML 1.4 notation [Gro01]. Constraint diagrams [Ken97] use a visual notation that is inspired by UML and Venn diagrams [Ven80]. In [FFH05], constraint diagrams are extended by a partial order for quantifiers and their semantics is defined based on first-order predicate logic. All of these approaches support the specification of architectural constraints based on the abstract syntax of the component model. That requires the developer, who specifies components based on concrete syntax, to translate the constraints to the abstract syntax of the component model. This introduces additional complexity for a developer that keeps him from effectively specifying constraints. 3.7.3.2 Component-Based Constraint Languages Approaches in this category enable to specify constraints based on a component specification either provided by an architecture description language or a component model. MechatronicUML Component Model Page 93 The ADL Dynamic Wright [ADG98] supports the specification of constraints based on first-order logic using a textual notation. The constraints directly refer to the components and connectors defined by the architectural style. Armani [Mon01] is a constraint language for the Acme ADL [GMW00]. It allows to specify architectural constraints in a first-order predicate logic using a textual concrete syntax. In contrast to our approach, neither Dynamic Wright nor Armani enable to refer to properties of embedded components. FPath [DLLC09] is a textual query language based on the Fractal component model. It is inspired by XPath [W3C10] and allows to select a set of embedded components in a hierarchical Fractal component across different levels of hierarchy. Therefore, it requires knowledge of the implementation of all components thereby breaking encapsulation. FPath is not explicitly defined as a constraint language, but may be used like one. The ACL family of architecture constraint languages [TFS10, TSDF11] enables the specification of constraints for components independent of a concrete component model. It supports two levels of abstraction: an object level using an OCL-like language called CCL (core constraint language) and an architecture-level constraint language. In the latter, constraints are modeled as special constraint components that are connected to the functional components by special non-functional or constraint ports even across different levels of hierarchy. The constraints are then verified at design-time to ensure that components are correctly assembled and implemented. In contrast to our approach, they do not enable to evaluate their constraints during runtime. 3.8 Summary In this chapter, we introduce a consolidated component model for MECHATRONICUML that enables to specify software architectures for self-adaptive mechatronic systems. Thereby, our component model primarily addresses the reflective operator of the OCM reference architecture but also includes the interface to the feedback controllers on the controller level. Therefore, it combines and enhances two existing component models for MECHATRONICUML that have been created by Burmester, Giese, and Hirsch [GTB+03, GBSO04, BGO06, HHG08, GS13] as well as Tichy [THHO08, Tic09]. In a little more detail, we use the necessary distinction of discrete atomic components and continuous atomic components representing feedback controllers from Burmester and Giese [GBSO04, BGO06]. In addition, we use the specification of structured components by means of component parts from Tichy [Tic09]. Compared to the previous component models, our new component model guarantees component encapsulation, enforces a separation of concerns between functional and reconfiguration behavior, and improves semiotic clarity [Moo09] of the concrete syntax. In our component model, we use CSDs [THHO08, Tic09] for specifying reconfigurations of components because they enable for a more concise specification compared to hybrid reconfiguration charts [GBSO04, BGO06]. Furthermore, we introduce a concept for instantiating RTCPs between AMS that are not yet connected with each other. Finally, we defined Page 94 Chapter 3 component SDDs that enable to specify architectural constraints and component properties based on the software architecture. We underpin the suitability of our component model for specifying software architectures of self-adaptive mechatronic systems by providing a software architecture of the RailCab system (cf. Section 1.1) focussing on the convoy mode. Our example includes the component definitions and the necessary CSDs for realizing RailCab convoys. Additional CICs and CSDs of the example scenario are given in Appendix A. We use this example as a basis for illustrating the further contributions of this thesis in the subsequent chapters. Transactional Execution of Hierarchical Reconfigurations Page 95 4 Transactional Execution of Hierarchical Reconfigurations Reconfigurations in a hierarchical component model often require the reconfiguration of several components that are located on different levels of hierarchy. As an example, the reconfiguration of a structured component instance may require the upfront reconfiguration of one or more of its children as it has been shown in the example of Figure 3.11. In this example, creating the instance mc of MemberControl requires to reconfigure the instances of OperationStrategy and VelocityController first. Then, the port instances created by these reconfigurations are connected by RailCabDriveControl. In general, we distinguish two use cases for such reconfigurations. In Use Case 1, an embedded component instance, in the following referred to as child, detects a situation that requires a reconfiguration that it cannot handle by itself. In our example in Figure 3.6, the OperationStrategy component negotiates that the RailCab enters a convoy, but it does not know how to do this itself. Thus, it needs to send a request to the embedding structured component instance of type RailCabDriveControl to handle that situation and to execute the necessary reconfiguration. We will refer to the embedding structured component instance as parent in the following. In Use Case 2, a structured component instance executes a reconfiguration that requires the reconfiguration of one or more of its children. In our example, becoming a member of a convoy requires a reconfiguration of the RailCabDriveControl (cf. Figure A.31). Executing this reconfiguration, however, requires that the OperationStrategy changes its port instances and that the VelocityController switches to the ConvoyDrive component instance (cf. Figure 3.12). Therefore, RailCabDriveControl needs to trigger the corresponding reconfigurations on its children. For both use cases, executing such reconfigurations safely demands that all component instances, which are required to reconfigure, perform their reconfiguration in a coordinated way. The necessary conditions for executing a hierarchical reconfiguration safely are given by the ACI-properties (atomicity, consistency, and isolation) of database systems [BHG87, LLC10] and a correct timing. Atomicity requires that either all or no component instances, which need to reconfigure, execute their reconfiguration. If reconfigurations are only executed partially, the system is usually unsafe. Consistency requires that any component instance has a valid architecture before and after each reconfiguration. Isolation ensures that reconfigurations do not interfere with each other. Interference of reconfigurations results in invalid architectures. A correct timing demands that if a hard deadline for executing a reconfiguration exists, the system needs to make sure that it meets the deadline before starting to reconfigure. For the remainder, we refer to these properties as ACI-T properties. If a reconfiguration is executed according to ACI-T properties, we denote this as transactional execution. Page 102 Chapter 4 4.2.2 Three-Phase Execution Single-phase execution of reconfigurations as described in the previous section cannot be applied if the reconfiguration involves replacing continuous components. As an example, consider the reconfiguration for becoming a convoy member shown in Figure 3.11. The reconfiguration requires that the VelocityController switches from the StandaloneDrive to the ConvoyDrive feedback controller (cf. Figure 3.7). Figure 4.7 shows an intermediate CIC that would occur if we executed this reconfiguration according to single-phase execution. As part of the execution phase, rc1 already queried the execution on vc1. As a result, vc1 started executing the CSD shown in Figure 3.12. vc1 already created the ConvoyDrive instance and currently executes the fadeTo- Convoy fading function in the fading component. At this point of time, both continuous component instances are executed in parallel. However, the ConvoyDrive instance will not properly work because the input ports refDist and curDist have no defined values. The reason is that these port instances are delegated by vc1 and needed to be connected in rc1 before starting to execute the fading. In particular, we needed to create instances of the SpeedSensor and the MemberControl in rc1 prior to executing the fading function. rc1 : RailCabDriveControl vc1 / ctrl : VelocityController :refSpeed :curSpeed :force os / strategy : OperationStrategy dl / drive : DriveLogic :speedProvider :refSpeed B :protocolInst B :protocolInst :section1 :section1 :section2 :section2 :maxSpeed sp / sp : SpeedSensor :speed vc1 : VelocityController :curDist :refDist +- sd / standalone_ctrl : StandaloneDrive :refSpeed :curSpeed :curDist cd / convoy_ctrl : ConvoyDrive :refSpeed :curSpeed :refDist :force :force :curDist :refSpeed :curSpeed :refDist f/fade: ConvoyFading fadeToConvoy() :standalone :convoy :force :force RM :reconfExec RE :reconfMsg RM :reconfExec RE :reconfMsg Figure 4.7: Problems when Replacing Continuous Component Instances using Single- Phase Execution Transactional Execution of Hierarchical Reconfigurations Page 103 As a solution to this problem, we split the execution phase of our 2-phase-commit protocol into three sub-phases as proposed by Volk [Vol13] if the reconfiguration replaces continuous components. These sub-phases are setup,fading, and teardown. Each of these sub-phases executes part of the reconfiguration. Figure 4.8 illustrates how these sub-phases are executed in a structured component instance. A filled bar denotes that the instance is currently executing reconfiguration behavior, while an unfilled bar denotes that the instance is idle. We explain this figure in more detail along with the different phases in the following Sections 4.2.2.1 to 4.2.2.3. The voting phase of the 2-phase-commit is executed as for single-phase execution (cf. Section 4.2.1) and will not be described here. Instance Phase Parent :RailCabDriveControl :VelocityController Setup Fading Teardown Figure 4.8: Illustration of Three-Phase Execution [Vol13] 4.2.2.1 Setup The three-phase execution starts with the setup phase. The setup phase (hierarchically) reconfigures a component instance such that all preconditions for executing the fading functions are established. Therefore, it changes the software architecture of the mechatronic system, but it does not change the exhibited behavior of the mechatronic system. The setup phase is executed bottom-up as shown in Figure 4.8, i.e., a component first triggers its children in parallel and executes its own setup behavior after all children are finished. In the setup phase, each component instance that is affected by the reconfiguration creates all discrete, continuous, and hybrid port instances as specified by the reconfiguration rule. In addition, structured component instances create all embedded component instances and all connector instances between continuous and hybrid port instances. Discrete component instances and ports are kept in a suspended mode, i.e., their RTSCs are not being executed and their clocks do not yet progress. All hybrid port instances that have been created during setup already emit their default value though. All affected fading components still forward the unmodified value of the continuous component that is to be replaced. Figure 4.9 shows component instances of RailCabDriveControl and VelocityController after performing the setup phase for the reconfiguration becomeMember shown in Figure 3.11. The corresponding CSD is applied on the component instance of RailCabDriveControl for driving alone shown in Figure 3.9. Page 104 Chapter 4 rc1 : RailCabDriveControl vc1 / ctrl : VelocityController :curSpeed :force os / strategy : OperationStrategy dl / drive : DriveLogic :speedProvider B :protocolInst B :protocolInst :section1 :section1 :section2 :section2 :maxSpeed sp / sp : SpeedSensor :speed :curDist ds / dist : DistanceSensor :distance :refSpeed :refSpeed :refDist mc / member : MemberControl :refDist :speedProvider :member :member :distReceiver :refDistReceiver vc1 : VelocityController +- sd / standalone_ctrl : StandaloneDrive :refSpeed :curSpeed :curDist cd / convoy_ctrl : ConvoyDrive :refSpeed :curSpeed :refDist :force :force :curDist :refSpeed :curSpeed :refDist f / fade : ConvoyFading fadeToConvoy() :standalone :convoy :force :force RM :reconfExec RE :reconfMsg RM :reconfExec RE :reconfMsg Figure 4.9: RailCabDriveControl after Executing the Setup Phase for the Reconfiguration becomeMember Since the setup phase is executed bottom-up, the execution starts at vc1.vc1 creates an instance of ConvoyDrive including the port instances refDist and curDist. In addition, it delegates all in-ports to the corresponding port instances of the new component instance cd. Finally, it creates the port convoy at the fading component including the assembly instance. As a result, vc1 contains all necessary component instances, port instances, and connector instances for executing the fading function. After vc1 finished, rc1 executes its setup phase. According to the CSD in Figure 3.11, rc1 creates instances of DistanceSensor and MemberControl. Since MemberControl is a discrete component, the instance mc remains suspended and only emits the default reference distance via its hybrid refDist port instance. In addition, rc1 creates the port instances member and refDistReceiver, but it does not yet create the corresponding delegation instances. Finally, rc1 creates the assembly connector instances between the continuous and hybrid port instances for connecting DistanceSensor and MemberControl to vc1. Transactional Execution of Hierarchical Reconfigurations Page 105 As it can be inferred from Figure 4.9, all in-ports of vc1 are properly connected. Thus, the fading function can now be executed and provide a meaningful result. Up to now, the behavior of rc1 and vc1 has not been changed because vc1 still emits the force value of sd and because the discrete connector instances in rc1 have not yet been modified and MemberControl is still suspended. 4.2.2.2 Fading In the fading phase, the behavior of the mechatronic system changes, but its software architecture does not change. In particular, we execute the fading functions of all affected fading components. As shown in Figure 4.8, we execute all fading functions in parallel, i.e., the fading components now emit the values of the fading functions that combine their input values. Discrete components remain idle during this phase. In our example in Figure 4.9, the fading component fexecutes the switchToConvoy fading as specified by the CSD in Figure 3.12. 4.2.2.3 Teardown The execution of the reconfiguration finishes with the teardown phase. In this phase, both, the behavior and the software architecture of the mechatronic system change. The teardown phase is executed top-down as shown in Figure 4.8, i.e., a component first executes its own teardown behavior before it triggers its children in parallel. In the teardown phase, we destroy all component instances, port instances, and connector instances as specified by the reconfiguration rule. Furthermore, we activate all discrete component instances and port instances that were created in the setup phase including the connector instances between discrete port instances. The fading components now forward the unmodified value of the continuous component instance that has been created. Continuing our example in Figure 4.9, we now destroy the StandaloneDrive instance including all of its port instances and adjacent connector instances. In rc1, we destroy the assembly between speedProvider of os and maxSpeed of dl. Additionally, os destroys its speedProvider port instance. Furthermore, we create delegation connector instances that delegate the port instances member and distReceiver of mc to the corresponding port instances of rc1. Finally, we create the assembly connector instance between speedProvider of mc and maxSpeed of dl. The result is, as expected, equivalent to the component instance Member shown in Figure A.31. 4.2.3 Quiescence Component instances and port instances may not be deleted at any point in time. In particular, they may not be deleted if they currently perform a computation or if they are Page 106 Chapter 4 engaged in executing a communication protocol that is required for the safe operation of the system. Quiescence [KM98, ZC06] defines whether it is safe to delete a component instance or one of its port instances at a certain point of time. Then, executing a reconfiguration safely demands that all affected component instances are quiescent. As an example, consider a member RailCab that leaves a convoy. As a consequence, the RailCab will destroy its instance of MemberControl and it will switch back to the StandaloneDrive feedback controller (cf. Section 4.2.2). However, the RailCab may not perform this reconfiguration if it is still driving closely behind another RailCab. If it performs the reconfiguration, it will not be notified about braking maneuvers of the convoy and, thus, a crash is likely to occur. Therefore, we need a concept for defining quiescence of component instances in MECHATRONICUML. In particular, we need to define quiescence of discrete atomic component instances. For continuous atomic component instances, the fading functions define how they may be safely replaced. A structured component instance is quiescent with respect to a particular reconfiguration if all children that are affected by this reconfiguration are quiescent. The concept for quiescence of discrete atomic component instances needs to answer the following three questions for being usable in our 2-phase-commit protocol. 1. Is the component instance quiescent? 2. If the component instance is quiescent, how long will it remain quiescent? 3. If the component instance is not quiescent, when will it be quiescent again? These questions need to be answered by the discrete atomic component instance during the voting phase of the 2-phase-commit protocol. Question 1 and 3 are important for deriving the voting result. A discrete atomic component instance may only vote for commit if it is presently quiescent or if it will become quiescent early enough. Question 2 is important for deriving the commit time that defines how long the component instance will stick to its commit. However, the component instance will only vote for commit if the commit time is above a threshold that is defined by the developer as we discuss in Section 4.3.4. An approach that may answer the three questions given above for a self-adaptive mechatronic system has been developed as part of a Master’s thesis [Sch15]. We will sketch its core ideas in the following. Our ideas are inspired by the approach of Zhang and Cheng [ZC06]. Their approach considers a state-based functional behavior specification of components based on petri nets (cf. [ZC06]) or UML Statecharts (cf. [RC08]), but they do not consider real-time constraints or properties of the physical system in their specification. For performing a reconfiguration, the system switches between source and target functional behaviors by executing an adaptation behavior (cf. Section 2.1.2). In our approach, the source and target functional behaviors correspond to the CICs before Transactional Execution of Hierarchical Reconfigurations Page 107 and after executing a reconfiguration, while the adaptation behavior is represented by our 2-phase-commit protocol. For guaranteeing quiescence, Zhang and Cheng define a set of global invariants using temporal logic that need to be fulfilled during the adaptation process. Then, a state sof the source functional behavior is quiescent if there exists a state tin the target functional behavior such that the adaptation from sto tdoes not violate any global invariant [ZC06]. This is ensured at design time by model checking the functional behaviors and the adaptation behavior [ZGC09]. Then, all states sof the source functional behavior are marked as quiescent with respect to a given adaptation. In a self-adaptive mechatronic system, the state of a component instance is not only determined by the active state of its RTSC but also by the current clock values of the RTSC and, potentially, the physical state of the mechatronic system. The physical state of a mechatronic system is given, for example, by its current spatial position, its speed, or its acceleration. Consider a member RailCab that wants to leave a convoy as an example. There, we need to consider the RailCab’s distance to the preceding RailCab and its current speed for deciding whether the component instance is quiescent. Therefore, it is not possible to simply mark states of an RTSC as quiescent as proposed by Zhang and Cheng. As an additional problem, considering the clock values and the physical state of the system induces a so-called hybrid model checking problem [Hen96]. Such model checking problems cannot be solved efficiently with current techniques [ERNF12] as we discuss in more detail in Chapter 6. As a possible solution, we can use our approach of motion profiles [FHK+13, FHK+14] for avoiding hybrid verification. A motion profiles gives an assertion on the limits of a change of the physical parameters of the mechatronic system in the future. Each motion profile is defined with respect to a particular control strategy, with respect to the current driving maneuver, e.g., braking or accelerating, and with respect to optimization criteria, e.g., braking strongly vs. braking smoothly. As a result, each system is equipped with a multitude of motion profiles. However, even in this case the state-space that needs to be explored is significantly larger compared to Zhang et al. [ZGC09] because we need to consider clocks and all possible motion profiles of the RailCab based on each possible point in time of the maneuver that is defined by the motion profile. Therefore, our idea is to identify quiescent states at runtime as a part of the voting phase of our 2-phase-commit protocol. This is more efficient than computing all possible symbolic states at design time [GCZ08] because we only need to check a few symbolic states. In particular, we only need to consider symbolic states that are reachable from the current snapshot of the component instance in a short period of time. In addition, we only need to consider the currently applied motion profile instead of considering all navailable motion profiles which reduces the state space by factor n. Figure 4.10 summarizes the idea of our approach. Page 108 Chapter 4 At design time, the developer needs to specify a set of conditions for quiescence. These conditions refer to the different parts of the atomic component instance, e.g., an active state of the RTSC, messages that are located in the message buffer of a port instance, or values regarding the physical state of the system that are received via a hybrid port instance. In our example, we might require that the distance of the member RailCab to the RailCab directly driving in front of it must be larger than 50m. Then, any symbolic state of the RTSC that fulfills all of the imposed conditions at runtime is considered to be quiescent. Thus, the conditions correspond to the invariants used by Zhang et al. [ZGC09]. For supporting the developer, we provide him with a checklist for typical influence factors that need to be considered for quiescence. The checklist will be derived by analyzing influence factors on quiescence in different self-adaptive mechatronic systems such as RailCabs or self-coordinating cars [PHMG14]. Design Time Runtime Discrete Atomic Component Checklist for Influence Factors Developer Set of Conditions for Quiescence refers to Evaluation of Conditions via Reachability Analysis model@runtime Vote Commit Time of Figure 4.10: Approach for Identifying Quiescent States in MECHATRONICUML At runtime, we use our model@runtime of the atomic component instance for evaluating the conditions as a part of the voting phase of the 2-phase-commit protocol. If the atomic component instance is requested to execute a reconfiguration by its parent, we start a reachability analysis on the current snapshot of the model@runtime. Then, we calculate the symbolic states that the atomic component instance may reach in a short time frame starting from the current snapshot. The time frame that needs to be considered is defined by the time for execution of our 2-phase-commit protocol and the threshold for the commit time. For each of the symbolic states, we evaluate the conditions that the developer has specified at design time. The result is a zone graph (cf. Section 2.2.1) where each symbolic state is marked as quiescent or non-quiescent. Thereby, we only need to consider the currently active motion profile and the current physical state of the system. Based on the clock values of the symbolic states, we may utilize the paths of the Transactional Execution of Hierarchical Reconfigurations Page 109 zone graph for calculating whether the component instance is quiescent and how long it will remain quiescent. From this information, we derive the voting result and the commit time that are passed to the parent. The reachability analysis may be carried out by a variant of the reachability analysis for RTSCs introduced in Appendix C.3 that is optimized for being executed on embedded computing devices. This rechability analysis needs to be implemented such that its runtime is predictable. This is necessary for guaranteeing that the component instance will obtain a voting result within a given time that the component asserts to its parent as we describe in more detail in Section 4.3.4. Predictability may be achieved, e.g., by limiting the number of symbolic states that are investigated for each trace of the zone graph as proposed by bounded model checking techniques [BCC+03]. 4.3 Declarative, Table-based Specification of the Reconfiguration Controller In our approach, we provide a declarative specification of the behavior of the reconfiguration controller based on tables. These tables extend the component model introduced in Chapter 3 by additional syntactical elements that are tailored the 2-phase-commit protocol. More technically speaking, the tables relieve the developer from manually specifying RTSCs for RM ports, RE port, manager, and executor. In a little more detail, the developer needs to specify one table for each RM port and for each RE port of a reconfigurable component. This table enhances the interface of the port, i.e., which messages the port may send or receive, with timing constraints for the messages that are relevant for executing the 2-phase-commit protocol. In addition, the developer needs to specify one table for the manager and for the executor of each reconfigurable structured component. The entries in these tables define conditions that express when to execute which reconfiguration, but they do not specify how the conditions are checked and how reconfigurations are executed according to the 2-phase-commit protocol. The timing constraints that are contained in our declarative, table-based specification are requirements for an execution of the reconfiguration behavior on a hardware platform. For a self-adaptive mechatronic system, these requirements originate from three sources. First, they originate from conditions that are imposed by the physical environment. As an example, consider a convoy build-up at a switch. In this case, the reconfigurations for becoming a coordinator or member, respectively, need to be finished before coming too close to the switch. Second, timing requirements are defined by the functional safety specification. In case of a hardware failure, a reconfiguration that implements a self-healing operation needs to be finished within a particular time in order to prevent a hazard. This particular time may be obtained by performing a timed hazard analysis [PST13]. Third, timing requirements originate from the quiescence criteria. The component instances that are affected by a reconfiguration need to remain quiescent Page 110 Chapter 4 throughout the reconfiguration (cf. Section 4.2.3). As a result, the reconfiguration needs to be finished before the component instance needs to execute some non-quiescent behavior that is necessary for safely operating the system. In the following, we provide details regarding our declarative, table-based specifications of manager and executor as well as of the interfaces of RM ports and RE ports in Sections 4.3.1 to 4.3.3. 4.3.1 Interface Specification of RM Ports An RM port is a special kind of discrete port (cf. Section 3.1.1.2) that is solely used for communication between the managers of reconfigurable components. Its interface is defined by a table with four columns. The first column defines the message types that may be sent to the parent. The second column gives additional information on the semantics of the message using a type. We distinguish two types of messages: info messages and requests. An info message is only provided for information and does not necessarily require a reconfiguration. A request is sent in situations where a reconfiguration is necessary from the perspective of the sending component and where it cannot solve the situation itself. In case of a request, the developer of a component may specify an expected response time in the third column. It defines the point in time where the component needs the information whether a reconfiguration has been executed by the parent. The fourth column optionally contains a human readable description of the reported situation for a developer. Each interface entry corresponds to one row in the table. Message Type Description drivingAtHighSpeed RailCab travels at high speed. Type info Expected Response Time drivingAtNormalSpeed RailCab travels at normal speed. info --- --- distanceSensorFailure Distance sensor is broken. request 200 ms Figure 4.11: RM Port Specification of the RailCabDriveControl Component (cf. [HB13]) Figure 4.11 shows an example of an RM port specification for the RM port of the Rail- CabDriveControl component shown in Figure 4.3. It contains three entries. First, the RailCabDriveControl informs its parent about its speed profile using the messages drivingAtHighSpeed and drivingAtNormalSpeed of type info. This information may be used to adapt the sensing of obstacles depending on the speed. If the speed is high, obstacles need to be sensed in larger distances to brake early enough. In addition, RailCabDrive- Control sends a request positionSensorFailure, which denotes that the distance sensor is broken. This request triggers a self-healing operation (cf. [Pri13, PST13]) and needs to be finished in 200ms for guaranteeing the convoy safety. Transactional Execution of Hierarchical Reconfigurations Page 111 4.3.2 Manager Specification The behavior of a manager is specified declaratively using a table with eight columns. We refer to each row of the table as an entry of the manager specification. The entries of the manager specification define how the manager needs to react if it receives a particular message. In our approach, the manager only reacts to messages that it receives from the children or from the executor. We did not yet include dedicated monitoring capabilities for structured components in our approach. The manager specification needs to contain exactly one entry for each message that the manager may receive from the children or from the executor. In the manager specification, the first column contains a message type that the manager may receive either from a child or from the executor. The second and third column define whether the manager treats the message or whether it propagates the message to its parent. A message that is received from the executor always needs to be treated. We allow, however, that the manager operates as a sink with respect to messages sent by a child by neither treating nor propagating them. We do not allow to treat and propagate a message at the same time because that may lead to conflicting reconfiguration decisions on different levels of hierarchy in the component model. All messages that are specified as propagated in the manager specification need to appear in the interface specification of the RM port parent of the corresponding reconfigurable component. If the specification defines that a message is treated, the developer must specify a reconfiguration rule to be executed by the executor in the fourth column. Whether a reconfiguration may be executed at runtime depends on three conditions that are specified in columns five to seven: (1) whether it is allowed to execute the reconfiguration (column Structural Condition), (2) whether it is safe to execute the reconfiguration (column Safety Relevant), and (3) whether it is useful to execute the reconfiguration (column Invoke Planner). Only if all three conditions evaluate to true during runtime, the manager will trigger the executor to execute the reconfiguration. We explain these conditions in more detail in the following. For each entry of the manager specification, the developer needs to define a structural condition. The structural condition specifies a condition on the embedded component instances that must be fulfilled for executing the reconfiguration. Currently, we only support specifying structural conditions based on component SDDs (cf. Section 3.5). It is only allowed to execute a reconfiguration if the structural condition is fulfilled. If the execution of the reconfiguration shall not be restricted, true may be used as a structural condition as for Entries 4, 6, 7, and 8. A reconfiguration may affect the functional safety [IEC10, ISO11a] of the system. An example for such reconfiguration is joining a convoy as a member. The functional safety specification puts a limit on the risk that a dangerous situation may occur during runtime. If a RailCab joins a convoy, the risk of a collision rises due to the small distances between the RailCabs. If, in addition, one of the sensors necessary for a convoy drive is broken, the risk of a collision may become too high to be acceptable. In such cases, Page 118 Chapter 4 reconfiguration can no longer be executed. This is the case if the time needed for executing the reconfiguration exceeds the expected response time. In this case, the subport sends an occupied message to the child indicating that the reconfiguration is currently not possible. The state ReceivedMsgX may also be left via the transition to DeliverMsg. That transition initiates a synchronization via the synchronization channel syncX. The synchronization channel syncX is generated for each message xthat is either propagated or treated by the manager. The transition synchronizes either with the internal behavior if the message is treated or with the parent if the message is propagated. If the message is propagated, the subport synchronizes with the parent. Then, the parent switches from Idle to Propagated and sends the message xto the parent. If the message is a request, the parent switches to AwaitReply while the subport switches to AwaitParentReply. When the parent answers, either by success or failure or occupied. Then, the parent uses the synchronization channel parentReply to report the result back to the subport which, in turn, sends the result back to the child. If the message received by the subport is treated, the synchronization via syncX causes the internal behavior to switch to CheckX. As its transition action, the transition checks the structural condition of the message xby calling the operation checkStructuralConditionX. This operation implements the structural condition that is specified in the manager specification (cf. Section 4.3.2). If the reconfiguration is safety relevant, then the operation isBlocked checks whether the reconfiguration with the given id is currently blocked by the runtime risk manager. Therefore, it uses the variable blockedReconfigurations that is set by the riskManager any time the runtime risk manager provides new data via updateRiskData. If the structural condition is not fulfilled or the reconfiguration is currently blocked, then the internal behavior immediately switches to Fail. Then it reports the result via the synchronization channel reply to the subport if the message is a request. If it is not a request, both RTSCs return to their Idle states without synchronization. If the structural condition is fulfilled and the reconfiguration is not blocked, the internal behavior switches to Plan and optionally invokes a planner. If the reconfiguration should be executed, the internal behavior synchronizes with the executor region using the synchronization channel executeReconf. Then, the internal behavior waits in state Execute for the result of the execution. The synchronization via executeReconf causes the executor region to switch from Idle to ExecuteReconf. The corresponding transition sends a message executeReconf to the executor. The reconfiguration to be executed is referred by its ID from the executor specification and encoded by an integer parameter of the message. Then, the executor performs the 2-phase commit protocol and reports the result, either success or failed,to the manager. The executor region reports the result to the internal behavior using the synchronization channel executed. Then, the executor region takes the lower transition from Finished back to Idle. If the message has been a request, the internal behavior reports the result to the instance of the subport that initiated the reconfiguration via the Transactional Execution of Hierarchical Reconfigurations Page 119 synchronization channel reply. The instance of the subport waits for that synchronization in the state AwaitReply and sends the result, either success or failed, back to the child. This finishes Use Case 1. In Use Case 2, the executor sends a message xto the manager. This message is processed by the executor RTSC at the transition from Idle to Request. Such transition is generated for each message offered by the RE port of the structured component. This transition, however, may only fire if a synchronization via the synchronization channel syncX with the internal behavior is possible. That, in turn, is only possible if currently no other reconfiguration is executed. Thus, we use the synchronization channel syncX for serializing the messages inside the manager. If the synchronization is possible, the execution proceeds as for Use Case 1. If the executor region reaches state Finished,however, it takes one of the upper two transitions back to Idle. These transitions synchronize with the transitions from Success to Idle and Fail to Idle in the internal behavior. These transitions enable to treat Use Cases 1 and 2 identical within the internal behavior. This finishes Use Case 2. 4.4.2 Executor Specification Figures 4.16 and 4.17 show the generation template for the executor RTSC. The template includes the behavior for both, single-phase execution and three-phase execution. The template implements the 2-phase-commit protocol including many variation points that depend on the executor and RE port specification. In the RTSC, all black states and transitions form the general frame of the RTSC. As for the manager generation template, they are always present and will only be generated once for every executor RTSC. The colored parts are variable and depend on the executor and RE port specification. We generate the blue parts for each message that is offered by the RE port of the component. The purple parts are generated for each reconfiguration rule that the executor may execute. Finally, the brown parts are generated for every reconfiguration rule that is offered by a child in its RE port. For realizing Use Case 1, the information flows as follows through the executor RTSC: The executor is initially triggered by the manager and receives the request in the events region. The events region triggers the internal behavior that initializes the 2-phase- commit protocol. The implementation of the 2-phase-commit protocol is mainly located in the adaptation region of embeddedCI. The adaptation computes the children that are affected by the reconfiguration. Then it performs the voting by triggering the corresponding subport instances that are connected to the affected children. Then, the reconfiguration is executed. In case of single-phase execution, the adaptation region triggers the subport instances again. After the execution of the child reconfigurations is finished, the adaptation reports the result to the internal behavior. Then, the internal behavior executes the reconfiguration for the structured component. In case of three-phase execution, the adaptation and the internal behavior execute the three phases of the reconfiguration. The adaptation triggers the subport instances that are connected to the affected children while Page 120 Chapter 4 Executor Executor_Main variable: boolean singlePhase, int reconfiguration, int tmpCommitTime, boolean twoPCResult; 2 1 clock: c2; channel: checkX, execute[boolean], startExecution, votingComplete[boolean], doAbort, finished, performReconf, finish[boolean], init2PC[int], finished2PC, localSetup, localFading, localTeardown, localFinish; parent events internal behavior embeddedCI 3 4 variable: int deadline, boolean fromParent, boolean abortedReqWaiting; clock: c1; operation: Y(); variable: Port subPort, int tmpMsg, boolean tmpCommit, int [Z.name]Msg := z.id; γ = x.timeForDecision –α α = X.timeForPlanning + timeForGuardChecking+ 2* internalMessageDelay Idle CheckX c2 ≤ γ x/ {reset: c2;} / abort() CheckSelf checkX! / execute[false]? / AwaitVoting execute[true]? / finished? / finished() SendAbort U WaitForParent votingComplete[false]? votingComplete[true]? / confirm(tmpCommitTime) Execution execute performReconf! / abort doAbort! / Aborted FinalizeAbort doAbort! / abort() finished? / [c2 ≥ γ]/ StartExecution startExecution! / U ExecuteSetupWaitFadingExecuteFadingWaitTeardownExecuteTeardown finished? / finished() teardown performTeardown! / finishPhase? / finished() fading performFading! / finishPhase? / finished() setup performSetup! / Idle entry/ fromParent := {false;} Check c1 ≤ deadline checkX? / {deadline := α; reset: c1; fromParent := true} x() confirmRequest execute[true]! / {reconfiguration := execute.reconf;} Busy declineRequest execute[false]! / failed() executeReconf startExecution!/ {reconfiguration := executeReconf.reconf;} Finished finish[false]? / failed() finish[true]? / success() [fromParent = false && abortedReqWaiting = false] / [fromParent = true] finished! / AwaitVoting DoAbort DoExecute votingComplete[false]? / [singlePhase] votingComplete[true]? / doAbort! / performReconf! / TimeOut [c1 = deadline] execute[false]! / confirmRequest / failed() AbortParentReq executeReconf execute[false]!/ {reconfiguration := executeReconf.reconf;} startExecution! / {abortedReqWaiting := true;} WaitForAnswer [abortedReqWaiting = true] AnswerReceived U UdeclineRequest / confirmRequest / / {abortedReqWaiting := false;} failed() U executeReconf {reconfiguration := executeReconf.reconf;} declineRequest / failed() executeReconf {reconfiguration := executeReconf.reconf;} DoSetup BusySetup DoFading BusyFading DoTeardown [not singlePhase] votingComplete[true]? / performSetup! / finishPhase? / performFading! / finishPhase? / performTeardown! / Idle [reconfiguration == Y1.id || ...] startExecution? / {singlePhase := true;} Start UWait init2PC[reconfiguration]! / Execute finished2PC? / U [twoPCResult == false] finish[false]! / Report U [singlePhase && twoPCResult && reconfiguration == Y1.id] / {Y1()} finish[true]! / LocalExecuteY2 Setup localFinish! / WaitFading {Y2_setup();} localFading? / {Y2_fading();} operation: Y2_setup(), Y2_fading(), Y2_teardown(); [not singlePhase] / Fading WaitTeardown localFinish! / Teardown localTeardown? / {Y2_teardown();} Finish localFinish! /finished2PC? / [reconfiguration == Y2.id] localSetup? / [reconfiguration == Y2.id || ...] startExecution? / {singlePhase := false;} Legend: Generated only once and are used by all reconfiguration rules Generated for each reconfiguration message X that is offered via RE port Generated for each reconfiguration message Z that is offered by an embedded child Generated for each reconfiguration rule Y that is executed by the executor Generated additionally for each reconfiguration Y1/Z1 that is executed using single-phase execution Generated additionally for each reconfiguration Y2/Z2 that is executed using three-phase execution Figure 4.16: Generation Template for the Executor RTSC (Pt. 1) Transactional Execution of Hierarchical Reconfigurations Page 121 embeddedCI 4 variable: Port subPort, int tmpMsg, boolean tmpCommit, int [Z.name]Msg := z.id; embeddedCI_Main adaptation subport 2 1 channel: sendRequest[Port], replyReceived, sendCommit[Port], sendAbort[Port], sendSetup[Port], sendFading[Port], sendTeardown[Port], reconfFinished; variable: AffectedComponents ac, int executionTime, int minCommitTime, Port curPort; operation: Port getNextPortInstanceForAction(AffectedComponents ac), Port allActionsPerformed(AffectedComponents ac), void setFinished(AffectedComponents ac, Port port), boolean allEmbeddedFinished(AffectedComponents ac); variable: int commitTime, int timeForDecision, int timeForExecution, int timeForSetup, int timeForFading, int timeForTeardown; clock: c2; Idle PrepareY init2PC[Y.id]? / Abort Execute_SinglePhase Vote Start / {ac := computeAffected ChildrenForY(); executionTime := Y.executionTime;} U Finished U [finished] finished2PC! / Report U WaitForParent votingComplete[TwoPCResult]! / {tmpCommitTime := minCommitTime;} [singlePhase] performReconf?/ doAbort?/ [finished] finished2PC! / Wait entry / {finished := allEmbeddedFinished(ac)} [finished] / {finished := false} variable: boolean finished := false; operation: AffectedComponents computeAffectedChildrenForY(); variable: boolean finished := false; operation: void storeMinCommitTime(int commitTime), Port getNextPortInstanceForRequest(AffectedComponents ac), int getMessage(AffectedComponents ac, Port port), boolean allRepliesReceived(AffectedComponents ac), void setReply(AffectedComponents ac, Port port, boolean commit), boolean canCommit(); variable: boolean finished := false; [not finished] reconfFinished? / {setFinished(ac, subPort);} SendAbort entry / {curPort := getNextPortInstanceForAction(ac); finished := allActionsPerformed(ac);} [not finished] sendAbort[curPort]! / U SendExecute entry / {curPort := getNextPortInstanceForAction(ac); finished := allActionsPerformed(ac);} U [not finished] sendCommit[curPort]! / GetReplies entry / {finished := allRepliesReceived(ac)} [not finished] replyReceived? / {setReply(ac, subPort, tmpCommit); storeMinCommitTime(tmpCommitTime)} [curPort == null] / {minCommitTime := 0} CheckResult entry / {TwoPCResult := canCommit();} U [finished] TriggerSubPort entry / {curPort := getNextPortInstanceForRequest(ac); tmpMsg := getMessage(ac, curPort);} sendRequest[curPort]! / U Execute_ThreePhase [not singlePhase] performSetup?/ WaitForResponse c2 ≤ timeForDecision Idle entry/ {commitTime := 0;} [tmpMsg == [Z.name]Msg] sendRequest[self]? / {timeForDecision := Z.timeForDecision; timeForExecution := Z1.timeForExecution; timeForSetup := Z2.timeForSetup; timeForFading := Z2.timeForFading; timeForTeardown := Z2.timeForTeardown; reset: c2;} z() VotedCommit abort /[c2 ≥ timeForDecision] confirm / {reset: c2; commitTime := confirm.t; } Execute c2 ≤ timeForExecution sendAbort[self]? / abort() finished reconfFinished! / {subPort := self;} VotedAbort ReplyReceived c2 ≤ commitTime AwaitFinish replyReceived! / {subPort := self; tmpCommit := false; tmpCommitTime := 0;} sendAbort[self]? / replyReceived! / {subPort := self; tmpCommit := true; tmpCommitTime := commitTime;} ExecuteSetup c2 ≤ timeForSetup sendCommit[self]? / {reset: c2} execute() sendSetup[self]? / {reset: c2} setup() WaitFading finished reconfFinished! / {subPort := self;} ExecuteFading c2 ≤ timeForFading sendFading[self]? / {reset: c2} fading() WaitTeardown finished reconfFinished! / {subPort := self;} ExecuteTeardown c2 ≤ timeForTeardown sendTeardown[self]? / {reset: c2} teardown() finished reconfFinished! / {subPort := self;} Figure 4.17: Generation Template for the Executor RTSC (Pt. 2) Page 122 Chapter 4 the internal behavior executes the local reconfiguration operations. After the reconfiguration has been completely executed, the internal behavior notifies the events region that the reconfiguration is completed. Then, the events region notifies the manager. This finishes Use Case 1 for the executor. In Use Case 2, the parent region receives a message from the parent. This message is forwarded to the events region which, in turn, forwards the message to the manager. Then, the manager answers with the decision and, if the request is confirmed, with the reconfiguration to be executed. Then, the 2-phase-commit protocol is executed as in Use Case 1 except for one difference. After finishing the voting phase, the adaptation triggers the parent region for sending the voting result back to the parent. Then, the parent region waits for the answer of the parent and triggers the adaptation region after the answer has been received. In case of three-phase execution, this is repeated for each of the three phases. Finally, the parent region informs the parent that the reconfiguration has been completed. This finishes Use Case 2. In the following, we provide a detailed, technical description of the generation template and explain how the Use Cases 1 and 2 are encoded in the template. An example of a generated executor RTSC is given in Appendix A.6.3.2 for the component RailCabDrive- Control. In Use Case 1, the events region receives a message executeReconf from the manager. This message is processed by the transition from Idle to AwaitVoting. The message contains the ID of the reconfiguration rule to be executed as a parameter. In addition, the transition from Idle to AwaitVoting synchronizes with the internal behavior via startExecution. The corresponding transitions from Idle to Start set the variable singlePhase to true if the reconfiguration needs to be executed with single-phase execution or false if the reconfiguration needs to be executed with three-phase execution. Then, the internal behavior starts the 2-phase-commit protocol using the transition from Start to Wait by synchronizing with the adaptation RTSC in embeddedCI via init2PC. The reconfiguration to be executed is encoded in the selector expression. The RTSC of the multi-port embeddedCI encodes the main logic for executing the 2- phase-commit protocol and controlling its different stages. We use the adaptation RTSC for synchronizing the communication with the children that are affected by the reconfiguration. The actual communication with the children is contained in the subport RTSC. If the adaptation RTSC is triggered via init2PC, it enters the PrepareY state. We generate such state for each reconfiguration Ythat can be executed by the executor. In this state, we compute which children are affected by the reconfiguration using the function computeAffectedChildrenY(). The result is saved in a temporary data structure of type AffectedComponents that contains the information which reconfiguration needs to be executed on which child. By using this data structure, we achieve that the remainder of the adaptation RTSC is independent of the actual reconfiguration that is executed. We present the definition of AffectedComponents in Appendix A.6.4.1 and an example for Transactional Execution of Hierarchical Reconfigurations Page 123 computeAffectedChildrenY() in Appendix A.6.4.2. All functions that are recursively contained in embeddedCI are formally specified using story diagrams that we present in Appendix A.6.4.3. After PrepareY, the adaptation switches to the Vote state. In the Vote state, the votes of all affected children for executing their reconfiguration are requested and collected. In TriggerSubPort, all subport instances communicating with an affected child are triggered by the self-transition using the synchronization channel sendRequest. The subport RTSC contains one transition from Idle to WaitForResponse for each message zthat is offered by a child. The message zto be sent to the particular child is stored in the variable tmpMsg of embeddedCI. The adaptation RTSC stores this message in the variable tmpMsg during its entry action in state TriggerSubPort. Upon synchronization via sendRequest, the subport RTSC uses this variable in its guard for sending the corresponding message zto the child. If the child does not answer in time or answers abort, the subport switches to VotedAbort. If the child answers commit, the subport switches to VotedCommit and stores the commit time in an internal variable. The adaptation switches from TriggerSubPort to GetReplies after all subports have been triggered. In GetReplies, the adaptation synchronizes with the subport, again, to receive their voting results. We use the synchronization replyReceived for that purpose and transfer the voting results using the variables tmpCommit and tmpCommitTime. After collecting all votes, the adaptation switches to CheckResult and calls the function canCommit() upon entry. The function determines whether all children voted for executing the reconfiguration and whether the minimum commit time sent by the children is greater than the time needed for executing the reconfiguration. If so, it is possible to execute the reconfiguration. After the voting phase has been finished, the adaptation reports the voting result via votingComplete to the events region. The RTSC either switches to DoAbort or DoExecute, respectively, and triggers either the execution via performReconf or the abortion via doAbort. Then, it waits in state Busy until the execution of the 2-phase-commit protocol has been finished. The further behavior of the adaptation depends on the voting result and whether the reconfiguration is executed with single-phase or three-phase execution. If the reconfiguration is aborted, adaptation enters the Abort state and triggers all affected subport instances, again, for sending the message to the corresponding children. The subport sends abort at the transition from ReplyReceived to Idle. If the reconfiguration is executed with single-phase execution, the adaptation enters the Execute_SinglePhase state. In this case, the adaptation triggers all affected subport instances for sending execute to the corresponding children at the transition from ReplyReceived to Execute. If the child executed, it answers with finished after successfully executing the reconfiguration. Then, the subport reports to the adaptation that the child has finished executing the reconfiguration using the synchronization finished. The adaptation Page 124 Chapter 4 waits for these synchronizations in substate Wait of Execute. After all child replies have been received, the adaptation synchronizes with the internal behavior via the synchronization channel finished2PC to report that all child reconfigurations have been completed. Execute_ThreePhase Wait entry / {finished := allEmbeddedFinished(ac)} [finished = true] / {finished := false} var: boolean finished := false; op: void resetActionPerformed(AffectedComponents ac); [finished = false] reconfFinished? / {setFinished(ac, subPort);} SendSetup entry / {curPort := getNextPortInstanceForAction(ac); finished := allActionsPerformed(ac);} U [finished = false] sendSetup[curPort]! / ExecuteLocalSetup [finished = true] localSetup! / FinishedSetup localFinish? / UWaitFading finishPhase! / {finished := false; resetActionPerformed(ac);} Wait entry / {finished := allEmbeddedFinished(ac)} [finished = true] / {finished := false} [finished = false] reconfFinished? / {setFinished(ac, subPort);} SendSetup entry / {curPort := getNextPortInstanceForAction(ac); finished := allActionsPerformed(ac);} U [finished = false] sendFading[curPort]! / FinishedFading [finished = true] localFinish? / U performFading? / ExecuteLocalFading UlocalFading! / WaitTeardown finishPhase! / {finished := false; resetActionPerformed(ac);} Wait entry / {finished := allEmbeddedFinished(ac)} [finished = true] / {finished := false} [finished = false] reconfFinished? / {setFinished(ac, subPort);} SendTeardown entry / {curPort := getNextPortInstanceForAction(ac); finished := allActionsPerformed(ac);} U [finished = false] sendTeardown[curPort]! / [finished = true] . finished2PC! / ExecuteLocalTeardown localTeardown! / performTeardown? / WaitLocal localFinish? / U Figure 4.18: Internal Structure of the Execute_ThreePhase State If the reconfiguration is executed with three-phase execution, the adaptation enters the Execute_ThreePhase state. The internal structure of this state is shown in Figure 4.18. The execution starts in Execute_Setup for executing the setup phase. First, the adaptation triggers all affected subport instances for sending setup to the corresponding children at the transition from ReplyReceived to ExecuteSetup. If the child executed, it answers with finished after successfully executing the setup phase. Again, the adapatation waits in substate Wait of Execute_Setup for the replies of the subport instances. After all children have performed their setup, the adaptation synchronizes with the internal behavior via localSetup. This causes the internal behavior to enter the LocalExecuteY2 state and to execute the local setup. After it is finished, it synchronizes via localFinished and the adaptation finishes the setup phase. It reports that the phase has been finished to the events region via finishedPhase and waits for the next phase to start. The remaining phases are executed in the same fashion. There are only two notable differences. In the fading phase, the adaptation first triggers the local fading. Without waiting for the finish of the local fading, it triggers the subport instances such that all fading functions are executed in parallel. In the teardown phase, the adaptation also triggers the local teardown first, but waits for the local teardown to finish. After the local teardown is finished, it triggers the subport instances for the last time. After all children have performed their teardown, Transactional Execution of Hierarchical Reconfigurations Page 125 the adaptation synchronizes via finished2PC with the internal behavior to report that the reconfiguration has been executed successfully. In case of three-phase execution, the synchronization via finished2PC causes the internal behavior to switch from Finished to Execute. Since singlePhase is false in this case, it immediately proceeds to Report. In case of single-phase execution, the synchronization via finished2PC causes the internal behavior to switch from Wait to Execute.IftwoPCResult, which stores the decision on whether to execute or not, is false, the internal behavior switches back to Idle.IftwoPCResult is true, then the internal behavior switches to Report and calls the own reconfiguration rule in the transition action. The transition back to Idle synchronizes with the events region to indicate that the execution has been finished. The synchronization finish causes the events RTSC to switch from Busy to Finished. This transition also sends a message success or failed to the manager in case that the reconfiguration has been executed or aborted, respectively. Finally, the RTSC fires the upper transition from Finished to Idle which finishes Use Case 1. In Use Case 2, messages reach the executor via the parent port and are processed by the corresponding RTSC in region parent. For each message xthat the component offers via its RE port, we generate one state CheckX including transitions from Idle to CheckX and from CheckX to CheckSelf and SendAbort. The transition from Idle to CheckX receives the message x.InCheckX, the parent tries to synchronize via checkX with the RTSC in the events region. The state CheckX contains an invariant c2 ≤γ.γis the time for decision specified in the RE port minus the time actually needed for deriving a decision in the manager. If γis exceeded, it is no longer possible to check whether the reconfiguration can be executed within the time for decision and the RTSC switches to SendAbort. This case will usually happen if the executor is already executing a reconfiguration when the message xarrives. In this case, a synchronization with the events region via checkX is not possible. If the synchronization via checkX is possible, the parent triggers the events region and switches to CheckSelf. The RTSC in the events region switches from Idle to Check and forwards message xto the manager. We generate such transition from Idle to Check for each message xin the RE port specification. In Check, the events region waits for the decision of the manager. If the manager sends declineRequest, the events region reports the result via the synchronization channel execute and the parent switches to SendAbort. If the manager sends confirmRequest, then the reconfiguration may be executed. The events region reports that result via execute to the parent which switches to AwaitVoting and triggers the internal behavior. Then, the voting phase is performed as in Use Case 1. In contrast to Use Case 1, the voting result is returned to the parent that sends the voting result to the parent component. If the component needs to abort, the parent switches via Aborted to FinalizeAbort.InFinalizeAbort, it synchronizes via finished with the events region and both RTSCs return to their Idle states. If the component has committed the reconfiguration, the parent waits in WaitForParent for the decision of the parent component. If the parent component aborts the reconfiguration, the parent FinalizeAbort. The Page 126 Chapter 4 transition from WaitForParent to FinalizeAbort synchronizes with the adaptation RTSC of embeddedCI via doAbort to abort the child reconfigurations. Afterwards, it synchronizes with the events region via finished as described above. If the parent decided to execute the reconfiguration, the parent region switches from WaitForParent to either Execution or to ExecuteSetup depending on whether the reconfiguration is executed with single-phase or three-phase execution. The corresponding transitions synchronize via performReconf with the adaptation RTSC of embeddedCI. Then, the child reconfigurations are triggered as in Use Case 1. In three-phase execution, the adaptation synchronizes with parent via finishPhase after completely executing one of the phases. The parent then reports that the phase has been finished to the parent. After all child reconfigurations and the own reconfiguration have been performed, the internal behavior synchronizes with the events region that informs the manager about the result of the execution. Finally, events takes the lower transition from Finished to Idle and synchronizes with parent via finished. That synchronization causes the transition from Execution to Idle to fire. This transition sends finished to the parent component which finishes Use Case 2. In the executor it may happen that two requests arrive at the same time: one from the parent component, the other one from the manager. These interleavings are handled in the events region using the states AbortParentReq,WaitForAnswer, and AnswerReceived as well as the variable abortedReqWaiting. If the events region is in state Check as part of Use Case 2, it may happen that the manager sends executeReconf instead of confirmRequest. In this case, the manager already treated a child request according to Use Case 1 when the executor forwarded the parent request. Then, the events region first treats the reconfiguration that was requested by the manager according to Use Case 1. Therefore, it switches from Check to AbortParentReq. This transition aborts the parent request by synchronizing via execute with the parent. As a result, the parent switches to SendAbort and finishes the request. However, the request by the parent still resides in the message queue of the manager. Therefore, after finishing the reconfiguration, the events region does not return to Idle, but it switches to WaitForAnswer. In this state, it waits for the confirmRequest or declineRequest message from the manager. If one of these messages is received, the events RTSC switches to AnswerReceived and immediately replies failed to the manager. In WaitForAnswer, it may also happen that another executeReconf message arrives. Then, the manager has treated another child request before the request of the executor. Then, the events RTSC switches back to AbortParentReq and the procedure repeats as described before. 4.5 Verifying the Reconfiguration Specification We need to verify that the specified reconfiguration behavior of a structured component fulfills all of the ACI-T properties of the 2-phase-commit protocol. These properties guarantee that the reconfiguration behavior of the structure component is correct and, thus, safe. In our approach, formal verification is enabled by the operational behavior specifications for manager and executor in terms of RTSCs. Transactional Execution of Hierarchical Reconfigurations Page 127 For verifying the ACI-T properties of the 2-phase-commit protocol, we need to verify the following yet informal properties: 1. If the executor decides to execute (abort), then all affected children execute (abort) (Atomicity). 2. The reconfiguration rules cannot produce an inconsistent CIC (Consistency). 3. The executor will execute no other reconfiguration than the one requested by the manager (Consistency). 4. At any time, at most one reconfiguration is executed (Isolation). 5. The RTSCs of manager and executor are free from deadlocks (Timing). 6. Each reconfiguration is executable (Timing). Properties 1, 3, and 4 can already be guaranteed by the correctness of the generation templates given in Section 4.4. Therefore, they do not need to be verified again for a particular structured component. The correctness of the generation templates with respect to these three properties has been verified using UPPAAL [HB13, Vol13]. Property 2 specifies that reconfigurations may not produce an inconsistent CIC. A CIC may either be syntactically inconsistent or semantically inconsistent. A CIC is syntactically inconsistent if it violates the conditions for syntactical correctness that we introduced in Section 3.2. In our approach, the CSDs guarantee that CICs remain syntactically consistent after a reconfiguration due to syntactic restrictions. Thus, no further check is necessary. A CIC is semantically inconsistent if the instantiated component instances, port instances, and connector instances do not constitute a desired functional behavior. In the worst case, the component may even be unsafe. As an example, consider a RailCab that drives as part of a convoy as a member but which does not have an instance of MemberControl (cf. Figure 4.7) although it switched the controller. Such situations cannot be prevented by syntactic rules but need to be verified for each structured component as we describe in Section 4.5.1. Finally, Properties 5 and 6 specify the conditions for a correct timing specification. In a platform-independent model, we may verify whether the timing requirements provided in our declarative, table-based specification are satisfiable. If they are satisfiable, there may exist a hardware platform that enables to execute the reconfiguration behavior without violating the timing requirements. After deriving a platform-specific model that includes a platform model and a deployment of components to hardware nodes [PMDB14], we may already check at design-time whether the execution of the reconfigurations on the hardware platform fulfills the imposed requirements. We describe the verification of the timing specification in detail in Section 4.5.2. In combination, both verification steps and the verified generation templates enable to verify the reconfiguration behavior of our components completely with respect to the ACI-T properties. The only part of the reconfiguration behavior that cannot be formally verified using model checking is given by the implementations of the fading functions. Page 134 Chapter 4 Minimum Commit Time Finally, the minimum commit time dct denotes the minimum time that the component sticks to a commit. A structured component instance may only stick to the commit at most as long as the children do. Thus, we need to consider the minimum among the minimum commit times dsub ct of all affected children. In addition, we need to subtract two times the message delay msub because the commit time starts after the child sent the commit and the query to execute needs to reach the child before the commit time expires. Thus, the minimum commit time dct of a structured component must be less or equal to dct ≤min i{dsub ct,i −2·msub i} where dsub ct,i refers to the minimum commit time of the ith child that is affected by this reconfiguration and msub iis the message delay for a message sent to that child. 4.6 Implementation We implemented the concepts introduced in this chapter as part of the MECHATRONICUML Tool Suite. In particular, we integrated the implementation into the plugins reconfiguration and reconfiguration.ui shown in Figure 3.22 on page 88. We extended the metamodel in plugin reconfiguration such that it includes our reconfiguration controller including the declarative, table-based specification. A class diagram of this metamodel is presented in Appendix D.2.1. The plugin reconfiguration.ui extends the component editor such that it enables to specify reconfigurable components including their reconfiguration controllers. In addition, it contains the generator that enables to generate RTSCs for manager and executor based on the generation templates given in Section 4.4. The generator has been implemented in QVT Operational [Gro11b]. In addition, we support to convert a non-reconfigurable component into a reconfigurable component. 4.7 Assumptions and Limitations Our approach for the transactional execution of reconfiguration underlies the following assumptions and limitations: •Any reconfiguration that has been started can be finished successfully. In particular, we assume that no hardware failures occur while executing a reconfiguration. •All monitoring is performed by atomic components that accumulate the monitoring data and provide accumulated data to the manager of the parent component. •The reconfiguration controller and the generation templates for deriving an operational behavior specification for manager and executor have only been defined for structured components because of the missing concept of quiescence for atomic components in MECHATRONICUML (cf. Section 4.2.3). Transactional Execution of Hierarchical Reconfigurations Page 135 •We may only trigger at most one reconfiguration on each child of a structured component instance when executing a CSD for the structured component instance. In addition, our implementation underlies the following limitations: •The generation templates do not support input and output parameters of CSDs as they are used, e.g., by the CSD in Figure 3.14 on Page 76. •The concept for verifying consistency introduced in Section 4.5.1 has not yet been implemented. 4.8 Related Work Section 3.7 reviewed component models and architecture description languages that support reconfiguration of the software architecture at runtime. Only few of them consider reconfiguration of hierarchical components supporting a transactional execution of reconfigurations. We review their reconfiguration capabilites in Section 4.8.1. Thereafter, we discuss related approaches for achieving quiescence in a system in Section 4.8.2. 4.8.1 Approaches Supporting Reconfiguration of Hierarchical Components Our approach is inspired by the reconfiguration concepts of Fractal [BCL+06, LLC10] which has been extended to distributed execution in [BHR09]. Their concept extends each reconfigurable component with a reconfiguration interface and a reconfiguration executor for executing reconfiguration scripts. We have adopted the concept of a reconfiguration executor and extended the remote reconfiguration invocation. In contrast to our approach, Fractal starts reconfigurations optimistically and performs a roll-back in case that the reconfiguration is not possible. As described in Section 4.2, this is not safe in mechatronic systems. Their approach achieves ACI properties as well, but does not consider timing of reconfigurations. In addition, we support a higher level modeling language for modeling reconfigurations rather than implementing them as a script. The approach by Boyer et al. [BGP13] also follows a roll-back approach for achieving reliable reconfiguration, but their approach neither treats hierarchy nor achieves any of the ACI-T properties. The SOFA 2.0 component uses component controllers similar to Fractal and to our approach, called micro-components, but does not provide a transactional execution of reconfigurations [HB07]. The architecture description language GeReL [EW92] supports a separation of concerns between functional and reconfiguration behavior. It uses a first-order logic to determine whether a reconfiguration can be executed or not. This ensures consistency of the modified system, while their execution model guarantees atomicity of reconfigurations. Their approach, however, does explicitly support hierarchical components. In addition, they do not consider real-time properties. Page 136 Chapter 4 Pop et al. [PPO+12] introduce a mode change operation of embedded real-time systems based on the SOFA-HI [PWT+08] component model. In their approach, each mode of a component instance corresponds to a configuration. They also separate functional and reconfiguration behavior and enable mode changes across different levels of hierarchy. Consistent modes of a component and its children are specified by property networks. In contrast to our approach, they cannot ensure atomicity if a child is currently not able to reconfigure and they do not provide a formal verification support for checking for a correct timing of reconfigurations. The approach by Hang et al. [HCH12, HQCH13] implements a composable mode change operator based on the ProCom component model [VSC+09]. As in [PPO+12], modes correspond to component configurations. Similar to our approach, they use dedicated reconfiguration components that are hierarchically connected. Reconfiguration requests may traverse the hierarchy bottom-up or top-down. In [HH13], they adopted our approach for executing reconfigurations in two phases and use our verification approach introduced in Section 4.5.2. In contrast to our approach, they do not provide explicit real-time properties regarding the execution of reconfigurations in their specification. The framework by de Oliveira et al. [DOLS13] uses several autonomic managers for adapting cloud applications in a coordinated fashion. Their autonomic managers have a similar purpose as our reconfiguration controller but are horizontally composed. They share information using event-based coordination protocols for improving adaptation decisions but do not consider transactional execution or real-time properties. The Rainbow framework [GCH+04, CGS09] provides an implementation of the reference architecture MAPE-K [IBM06] that targets business information systems. Their concept defines an adaptation manager and an adaptation executor that closely correspond to the manager and executor in our approach. However, their approach does not respect component encapsulation for a hierarchical component architecture. In addition, their approach does neither support real-time properties nor guarantee ACI-T properties. Similarly, Zhang et al. [ZCYM05] provide an approach for safe adaptation of component-based systems. Their approach uses one central adaptation manager that orchestrates the adaptation process, and several agents that are attached to the components and perform their modification. If an adaptation cannot be finished successfully, they perform a roll-back to the previous configuration. Thus, their approach guarantees ACI properties for the execution of reconfigurations but no real-time properties. In addition, their approach does not explicitly consider hierarchical components. The approach by Edwards et al. [EGT+09] uses meta-level components for implementing a self-adaptation control loop similar to MAPE-K [IBM06] based on a hierarchical component model. The meta-level components fulfill a similar purpose as our reconfiguration controller by monitoring the components on the hierarchy level below, by evaluating whether and how to adapt, and by executing the resulting adaptation plan. Similarly, Vromant et al. [VWMA11] connect several MAPE control loops that are located on the same hierarchy level following a master-slave pattern. Then, the control Transactional Execution of Hierarchical Reconfigurations Page 137 loops communicate for deriving a consistent adaptation strategy. Both approaches do not explicitly connect meta-level component or MAPE control loops, respectively, on different hierarchy levels such that hierarchical execution are not supported and ACI-T properties cannot be guaranteed. EUREMA [VG14] supports the specification of self-adaptation feedback loops based on MAPE-K [IBM06] using a graphical notation called feedback loop diagrams. The approach supports to use and to coordinate multiple feedback loops in a single system. In addition, feedback loops on different architectural levels may be connected and coordinated by using layer diagrams. Weyns et al. [WSG+13] discuss different design patterns for connecting multiple MAPE feedback loops in a system. With respect to their pattern, our approach is based on the hierarchical control pattern. In contrast to our approach, the approaches do not support real-time constraints and do not explicitly consider ACI-T properties. However, EUREMA satisfies isolation of adaptations. Finally, the fault-tolerant component model by de Lemos et al. [dLdCGFR06] partitions component behavior into normal and abnormal (exception) behavior. We follow the same idea by separating normal behavior and reconfiguration behavior. Their approach provides horizontal propagation of exceptions, but not propagation to parent components. With a similar objective, Strunk and Knight [SK06] provide a dependable reconfiguration approach for hard real-time systems where a system moves from one configuration to another one with degraded functionality in case of a failure. The approach, however, neither considers components nor hierarchy, but it ensures by formal proofs that any reconfiguration can be executed successfully. 4.8.2 Quiescence of Components In the approach by Kramer and Magee [KM98], the conditions for quiescence require all affected component instances and all component instances that are connected to them to be passive. In essence, this means that the component instances are shut down and no longer executed. After the reconfiguration has been finished, they are started, again. Given an NMS such as a convoy of RailCabs, this is not a viable approach. In the worst case, it requires that all the RailCabs in a convoy need to shutdown if one RailCab needs to perform a reconfiguration. This, in turn, requires the RailCab to stop for each reconfiguration, which is not desirable. The concept of tranquility [VEBD07] relaxes the conditions on quiescence by Kramer and Magee [KM98]. The major drawback of their approach is that tranquility is not predictable, i.e., it cannot be decided whether a component instance will become tranquil in a given amount of time. The approaches by Chen et al. [CHS01], Ghafari et al. [GJSH12], and Panzica La Manna [PLM12] support the evolution of a software architecture of a business information system where component instances are upgraded to a new version implements the same behavior. The new component instance either fixes bugs of the old component instance or provides quality of service that suites better to the current requirements. The approaches by Chen et al. and Ghafari et al. work similar to our fading functions. The component Page 138 Chapter 4 instance to be removed and the new component instance are executed in parallel. Then, new transactions are handled by the new component instance while the old component instance remains active until it has processed all pending transactions. The approach by Panzica La Manna tries to transfer the complete state of the old component instance to the new one such that the new component instance may continue processing all transactions that have been started using the old component instance. If this is not possible, the approach applies a version consistent update as defined by Ma et al. [MBG+11] that applies a similar strategy as the approaches by Chen et al. and Ghafari et al. In essence, all of these approaches try to preserve the functional behavior of the system during and after the update with the exception of corrected bugs and improved quality of service characteristics. In contrast, our approach explicitly aims at modifying the functional behavior, e.g, if a RailCab joins a convoy. Therefore, we require to add or to entirely remove component instances from the software architecture, which is not supported by these approaches. In addition, they do not consider the real-time constraints and the physical movement of the system, e.g., its current speed or its distance to other vehicles. 4.9 Summary This section introduces an approach for executing reconfigurations in a hierarchical component model for self-adaptive mechatronic systems. On the syntactic level, we extend each structured component by a dedicated reconfiguration controller that contains the reconfiguration behavior. The reconfiguration controller contains a manager, an executor, and an optional runtime risk manager. The manager defines whether and how the component shall reconfigure. The executor is responsible for executing reconfigurations with respect to hierarchy. The runtime risk manager defines which reconfigurations may be executed such that the functional safety of the system is retained. On the semantic level, our reconfiguration controller implements a variant of the 2-phase-commit protocol [BHG87, ch. 7] that has been adapted to the domain of mechatronic systems. As a result, our approach satisfies ACI-T properties for the execution of reconfigurations, i.e., atomicity, consistency, isolation, and a correct timing, even for reconfigurations spanning vertical compositions of components. Furthermore, our approach respects encapsulation of components. For the execution of the reconfiguration, our approach supports a single-phase execution for reconfiguring discrete component instance and a three-phase execution for safely replacing continuous components that contains feedback controllers. Our approach relieves the component developer from specifying the complex implementation of the 2-phase-commit protocol by hand for each component. Instead, we provide a concise declarative specification of the behavior of manager and executor based on tables. These tables specify the conditions when to execute which reconfiguration. Then, these tables are used as an input of a generator that automatically derives an implementation of the 2-phase-commit protocol based on RTSCs. The generated RTSCs fulfill atomicity and isolation by construction. In addition, the generated RTSCs and the CSDs Transactional Execution of Hierarchical Reconfigurations Page 139 that define the modification of the CIC serve as inputs for our verification procedure that verifies consistency and a correct timing of the reconfiguration behavior. Verifying Refinements based on Test Automata Page 141 5 Verifying Refinements based on Test Automata Self-adaptive mechatronic systems are often intended to operate as part of an NMS. As an example, RailCabs are intended to operate in convoys. Then, the correct functionality of the self-adaptive mechatronic system and, in particular, its safety do not only depend on its own correctness but also on the correct interaction with other AMS inside the NMS. The interaction, in turn, is typically defined by complex application-level communication protocols. These communication protocols define which messages are needed to be exchanged and in which order and time intervals for realizing the intended functionality. Equally, defining the behavior of a single AMS requires to connect the different components of its software architecture using application-level communication protocol as well. As an example, consider the component instances of a RailCab given in Section 3.2 and Appendix A.4. Due to the safety critical nature of self-adaptive mechatronic systems, we need to formally verify their behavior based on model checking [CGP00, BK08] for guaranteeing their correctness. On the one hand, this requires to verify the reconfiguration behavior of the components as discussed in Section 4.5. On the other hand, this requires to verify the functional behavior specification of each discrete atomic component that is used in the software architecture. However, the correctness of a single component does not only depend on its own behavior specification but also on the behavior specifications of the components that it needs to interact with. The resulting software architecture as given by a CIC consists of several interconnected component instances. Such CIC, however, cannot be verified using standard model checking tools like UPPAAL [BDL+06b] due to the state-explosion problem [CGP00]. Compositional verification approaches [BCC98] based on the assume/guarantee principle [CGP00, ch. 12] tackle the state explosion problem by decomposing the system into smaller units for verification. Previous works defined such compositional verification approach for MECHATRONICUML as well [GTB+03, Gie03, GS13]. The basic idea of MECHATRONICUML’s compositional verification approach is a syntactic decomposition of the functional behavior into RTCPs and components. It requires that RTCPs are specified independent of components. Then, each discrete port of a discrete atomic component refines one role of a RTCP, which results in one RTSC for each discrete port. These port RTSCs are then composed to a component RTSC as illustrated in Figure 3.3. This allows to verify the functional behavior of large components or even of complete an NMS in three steps as illustrated in Figure 5.1. In the following, we illustrate the three steps of MECHATRONICUML’s compositional verification approach based on the RailCab system using the RTCP EnterSection.In the RailCab system, RailCabs travel on a track system that is subdivided into different types of sections including switches and railroad crossings. Before entering a section, a RailCab needs to query the section whether it is allowed to enter it using EnterSection. This is necessary for realizing collision avoidance because sensors in a RailCab may not Page 142 Chapter 5 1. Verify Abstract Protocol via Model Checking |= I 1,…, I n 3. Verify each Component seperately via Model Checking (at least for deadlock freedom) 2. Verify Refinement |= I 1,…, I n AG (A¬railcab.enterSection Wsection.enterAllowed) I 1 delay: 20ms :section2 :left railcab section EnterSection «refines»«refines» Abstract ProtocolRefined Protocol in-buffer size: 1 in-buffer size: 1 RailCab 1 : RailCab ts3:Switch Figure 5.1: Overview of the Refinement Approach [HBDS15] detect other RailCabs if they are hidden behind a bend or some other obstacle. Therefore, RailCabs communicate with a section for getting permission to enter it. In the first step of the compositional verification approach, the developer needs to verify all RTCPs that he used in the system for safety and liveness properties. The verification may either be carried out using model checking based on UPPAAL as described by Gerking [Ger13] or using a graph-based verification technique [EHH+13, SHS11]. In our RailCab example, this step includes verification of the RTCP EnterSection beside others. For the remainder of this chapter, we refer to the behavior implemented by the roles of the RTCP as the abstract protocol. In the second step, we verify whether the ports of a component correctly refine the roles of the RTCP. This is necessary because the ports usually need to extend the role behavior by additional computations. In our example, a port of a track section may not decide on its own whether the track section is free. If several ports of a track section communicate with different RailCabs, the ports need to be synchronized such that only one port allows a RailCab to enter at a time. Despite the necessary modifications, the behavior of a port must be compliant to the specified role behavior, i.e., it must be a legal refinement according to a refinement definition. In the following, we refer to the behavior implemented by the discrete ports as the refined protocol. In the third step, we combine the port RTSCs to a component RTSC using additional synchronization RTSCs (cf. Section 3.1.2.1). Then, we need to verify for each component RTSC that it is free of deadlocks [Gie03]. We may verify additional safety and liveness properties referring to a correct interaction of the different ports of a component if necessary. In our RailCab example, we may verify the aforementioned property that the track section gives permission to only one RailCab to enter at a time. Approaches for resolving such dependencies automatically have beeen introduced by Eckardt and Henkler [EH10] and Goschin et al. [Gos14, DGB14]. Verifying Refinements based on Test Automata Page 143 Verifying the correctness of the refinement in the second step of the compositional verification approach requires a formal refinement definition. It guarantees that all properties that have been verified for the RTCP also hold for the interaction of components via their discrete ports. A suitable refinement definition leaves the developer with as much flexibility on refining the model as possible, but is as restrictive as necessary for guaranteeing that no verified property is violated. This enables to use the same RTCP for different components. In the RailCab example, it is particularly useful to use the RTCP EnterSection for all types of track sections. Then, the type of track section is opaque for a RailCab. Each kind of track section, however, requires the behavior of a section to be refined differently. In literature, different refinement definitions have been proposed [WL97, JLS00, HH11a]. Each of which provides a different compromise between preserved properties and allowed modifications. Depending on the particular type of RTCP that is refined, all of them might be useful when building a system. As a consequence, there does not exist one refinement definition that is suitable of all RTCPs. Instead, a compositional verification approach should support several refinement definitions. Presently, the compositional verification approach supports only one particular kind of timed simulation [Gie03], which is not sufficient to handle the example sketched above. In this chapter, we extend the compositional verification approach of MECHATRONICUML by supporting a total of six different refinement definitions. As our main contribution, we present a refinement check that enables to verify all six refinement definitions for a given role of a RTCP and a discrete port of a component. Our refinement check extends the approach by Jensen et al. [JLS00] that is based on so-called test automata. A test automaton encodes both the behavior of the role and the conditions for a correct refinement. If (and only if) the port behavior violates the conditions for a correct refinement, the test automaton enters a special error location indicating a negative verification result. We parameterized and extended the original construction such that we may verify all refinement definitions in a single algorithm that may easily be extended to include additional refinement definitions if necessary. As a byproduct, our refinement check may automatically detect which refinement definition is suitable for a given pair of role and port behavior including the verified properties. Although the compositional verification approach of MECHATRONICUML is primarily intended for verifying the software that is used in the reflective operator of the OCM [GS13], our refinement check may also be used for checking refinements of RTCPs that are used in the cognitive operator. In the remainder of this chapter, we first describe the behavior of the RTCP EnterSection including refined port RTSCs for the different types of track sections in Section 5.1. Section 5.2 reviews the six refinement definitions that we consider in our approach. Then, we introduce our refinement check based on test automata in Section 5.3 and its implementation in Section 5.4. Thereafter, we discuss the assumptions and limitations of our approach in Section 5.5. We evaluate our refinement check using a case study based on the RTCP EnterSection (Section 5.6). Finally, we discuss related work (Section 5.7) and summarize the results (Section 5.8). Supervised Thesis Page 247 Supervised Thesis [AAB+11] AHMADIAN, A. S.; AYDOGAN, C.; BRAUN, D.; BUSTAMANTE, L. G.; GERKING, C.; ISSIZ, S.; KOPECKI, L.; PRESCHER, P.: Developer documentation of the Project Group SafeBots I. Project group, University of Paderborn, September 2011. [Bre10] BRENNER, C.: Analyse von mechatronischen Systemen mittels Testautomaten. Master’s thesis, University of Paderborn, August 2010. [Brö11] BRÖKER, K.: Modellierung und Verifikation von Kommunikationsprotokollen für den Betrieb des RailCab Systems. Master’s thesis, University of Paderborn, November 2011. [Dre11] DREISING, C.: Reconfiguration of MechatronicUML component architectures. Bachelor’s thesis, University of Paderborn, November 2011. [Pin12] PINES, A.: Transformation von rekonfigurierbaren MechatronicUML-Mo- dellen nach MATLAB/Simulink. Bachelor’s thesis, University of Paderborn, June 2012. [Sch12] SCHUBERT, D.: Integration von Modellierungssprachen für Rekonfiguration in MechatronicUML. Bachelor’s thesis, University of Paderborn, June 2012. [Sch15] SCHUBERT, D.: Identification of safe states for reconfiguration in MechatronicUML. Master’s thesis, University of Paderborn, July 2015. [Suc11] SUCK, J.: Model Checking zeitbehafteter Graphtransformationssysteme. Master’s thesis, University of Paderborn, May 2011. [Vol13] VOLK, A.: Hybride, rekonfigurierbare, hierarchische Komponentenstrukturen in MATLAB/Simulink. Master’s thesis, University of Paderborn, December 2013. Literature Page 249 Literature [ABBL03] ACETO, L.; BOUYER,P.;BURGUEÑO, A.; LARSEN,K.G.: The power of reachability testing for timed automata. Theoretical Computer Science, 300(1-3):411–475, May 2003. ISSN:0304-3975. doi:10.1016/s0304-3975(02)00334-1. [ABRW09] ANGERMANN, A.; BEUSCHEL, M.; RAU, M.; WOHLFARTH,U.: MATLAB – Simulink – Stateflow, Grundlagen, Toolboxen, Beispiele. Oldenbourg Verlag, München, 6 edition, 2009. ISBN:978-3-486- 59546-8. [ACD93] ALUR, R.; COURCOUBETIS, C.; DILL, D. L.: Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993. ISSN:0890-5401. doi:10.1006/inco.1993.1024. [ÅCF+07] ÅKERHOLM, M.; CARLSON, J.; FREDRIKSSON, J.; HANSSON, H.; HÅKANSSON, J.; MÖLLER, A.; PETTERSSON,P.;TIVOLI, M.: The SAVE approach to component-based development of vehicular systems. Journal of Systems and Software, 80(5):655 – 667, May 2007. ISSN:0164-1212. doi:10.1016/j.jss.2006.08.016. [AD94] ALUR, R.; DILL, D. L.: A theory of timed automata. Theoretical Computer Science, 126(2):183–235, April 1994. ISSN:0304-3975. doi:10.1016/0304-3975(94)90010-8. [ADG98] ALLEN, R.; DOUENCE, R.; GARLAN, D.: Specifying and analyzing dynamic software architectures. Lecture Notes in Computer Science, 1382:21–37, 1998. [ADI06] ALUR, R.; DANG,T.;IVAN ˇ CI´ C, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Transactions on Embedded Computing Systems (TECS), 5:152–199, February 2006. ISSN:1539- 9087. doi:10.1145/1132357.1132363. [ADM01] ASARIN, E.; DANG,T.;MALER, O.: d/dt: A tool for reachability analysis of continuous and hybrid systems. In Proceedings of the 5th IFAC Symposium Nonlinear Control Systems, NOLCOS, pages 3–34, July 2001. ISBN:978-0-08-043560-2. [ADM02] ASARIN, E.; DANG,T.;MALER, O.: The d/dt tool for verification of hybrid systems. In BRINKSMA, E.; LARSEN, K. G. (Eds.), Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, pages 365–370. Springer Berlin Heidelberg, 2002. ISBN:978-3-540- 43997-4. doi:10.1007/3-540-45657-0_30. Page 250 [ÅEM98] ÅSTRÖM, K. J.; ELMQVIST, H.; MATTSON, S. E.: Evolution of continuous-time modeling and simulation. In Proceedings of the 12th European Simulation Multiconference on Simulation - Past, Present and Future, pages 9–18. SCS Europe, 1998. ISBN:1-56555-148-6. [AH92] ALUR, R.; HENZINGER, T. A.: Logics and models of real time: A survey. In DE BAKKER,J.W.;HUIZING, C.; DE ROEVER, W.-P.; ROZENBERG, G. (Eds.), Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74–106. Springer Berlin Heidelberg, June 1992. ISBN:978-3-540-55564-3. doi:10.1007/bfb0031988. [AHJ+09] ANNE, M.; HE, R.; JARBOUI,T.;LACOSTE, M.; LOBRY, O.; LORANT, G.; LOUVEL, M.; NAVAS, J.; OLIVE,V.;POLAKOVIC, J.; POULHIÈS, M.; PULOU, J.; SEYVOZ, S.; TOUS, J.; WATTEYNE,T.: Think: View-based support of non-functional properties in embedded systems. In International Conference on Embedded Software and Systems, ICESS ’09, pages 147 –156. IEEE Computer Society, May 2009. ISBN:978-1-4244-4359-8. doi:10.1109/icess.2009.30. [AHKV98] ALUR, R.; HENZINGER, T. A.; KUPFERMAN, O.; VARDI, M. Y.: Alternating refinement relations. In SANGIORGI, D.; SIMONE, R. (Eds.), CONCUR’98 Concurrency Theory, volume 1466 of Lecture Notes in Computer Science, pages 163–178. Springer Berlin Heidelberg, 1998. ISBN:978-3-540-64896-3. doi:10.1007/bfb0055622. [Alu99] ALUR, R.: Timed automata. In HALBWACHS, N.; PELED,D.A. (Eds.), Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 8–22. Springer Berlin Heidelberg, July 1999. ISBN:978-3-540-66202-0. doi:10.1007/3-540-48683-6_3. [Alu11] ALUR, R.: Formal verification of hybrid systems. In Proceedings of the ninth ACM international conference on Embedded software, EMSOFT ’11, pages 273–278, New York, NY, USA, 2011. ACM. ISBN:978-1- 4503-0714-7. doi:10.1145/2038642.2038685. [AM02] AGUIRRE, N.; MAIBAUM, T.: A temporal logic approach to the specification of reconfigurable component-based systems. In Proceedings of the 17th IEEE International Conference on Automated Software Engineering, ASE 2002, pages 271–274, Los Alamitos, CA, USA, 2002. IEEE Computer Society. ISBN:0-7695-1736-6. doi:10.1109/ase.2002.1115028. [Arb04] ARBAB, F.: Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14(3):329–366, May 2004. ISSN:1469-8072. doi:10.1017/s0960129504004153. Literature Page 251 [ASTPH10] ADLER, R.; SCHAEFER, I.; TRAPP, M.; POETZSCH-HEFFTER,A.: Component-based modeling and verification of dynamic adaptation in safety-critical embedded systems. ACM Transactions on Embedded Computing Systems, 10(2):20:1–20:39, December 2010. ISSN:1539- 9087. doi:10.1145/1880050.1880056. [AUT11] AUTOSARAUTOSAR 3.2 - Technical Overview, April 2011. Document Identification No. 067, Version 2.2.2. URL: http://www.autosar.org/fileadmin/files/releases/ 3-2/main/auxiliary/AUTOSAR_TechnicalOverview.pdf [cited March 14, 2015]. [AUT14a] AUTOSARAUTOSAR 4.1 - Guide to Modemanagement, March 2014. Document Identification No. 440, Version 2.2.0. URL: http: //www.autosar.org/fileadmin/files/releases/4-1/ software-architecture/system-services/auxiliary/ AUTOSAR_EXP_ModemanagementGuide.pdf [cited March 14, 2015]. [AUT14b] AUTOSARAUTOSAR 4.1 - Specification of Timing Extensions, March 2014. Document Identification No. 411, Version 2.1.1. URL: http://www.autosar.org/fileadmin/files/releases/ 4-1/methodology-templates/templates/standard/ AUTOSAR_TPS_TimingExtensions.pdf [cited March 14, 2015]. [AUT14c] AUTOSARAUTOSAR 4.1 - Virtual Functional Bus, March 2014. Document Identification No. 056, Version 3.2.0. URL: http://www.autosar.org/fileadmin/files/releases/ 4-1/main/auxiliary/AUTOSAR_EXP_VFB.pdf [cited March 14, 2015]. [BB08] BAUMANN, G.; BROST, M.: Testverfahren für Elektronik und Embedded Software in der Automobilentwicklung. In GIESE, H.; HUHN, M.; NICKEL, U. A.; SCHÄTZ, B. (Eds.), Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme IV, Schloss Dagstuhl, Germany, 7.-9. April 2008, Tagungsband Modellbasierte Entwicklung eingebetteter Systeme, number 2008-2 in Informatik-Bericht, pages 13–19. TU Braunschweig, Institut für Software Systems Engineering, April 2008. [BBCP13] BARNAT, J.; BENEŠ, N.; CERNÁ, I.; PETRUCHOVÁ, Z.: DCCL: verification of component systems with ensembles. In Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, CBSE ’13, pages 43–52, New York, NY, USA, June 2013. ACM. ISBN:978-1-4503-2122-8. doi:10.1145/2465449.2465453. Page 252 [BBF09] BLAIR, G.; BENCOMO, N.; FRANCE, R. B.: Models@ run.time. Computer, 42(10):22 –27, October 2009. ISSN:0018-9162. doi:10.1109/mc.2009.326. [BBG+06] BECKER, B.; BEYER, D.; GIESE, H.; KLEIN,F.;SCHILLING,D.: Symbolic invariant verification for systems with dynamic structural adaptation. In Proceedings of the 28th International Conference on Software Engineering, ICSE ’06, pages 72–81, New York, NY, USA, May 2006. ACM. ISBN:1-59593-375-1. doi:10.1145/1134285.1134297. [BC12] BOUISSOU, O.; CHAPOUTOT, A.: An operational semantics for Simulink’s simulation engine. In Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems, LCTES ’12, pages 129– 138, New York, NY, USA, 2012. ACM. ISBN:978-1-4503-1212-7. doi:10.1145/2248418.2248437. [BCC98] BEREZIN, S.; CAMPOS, S.; CLARKE, E. M.: Compositional reasoning in model checking. In ROEVER, W.-P.; LANGMAACK, H.; PNUELI, A. (Eds.), Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 81– 102. Springer Berlin Heidelberg, 1998. ISBN:978-3-540-65493-3. doi:10.1007/3-540-49213-5_4. [BCC+03] BIERE, A.; CIMATTI, A.; CLARKE, E. M.; STRICHMAN, O.; ZHU, Y.: Bounded model checking. In ZELKOVWITZ, M. V. (Ed.), Advances in Computers, Volume 58, pages 117–148. Elsevier, 1st edition, 2003. ISBN:0-12-012158-1. [BCDW04] BRADBURY, J. S.; CORDY, J. R.; DINGEL, J.; WERMELINGER,M.: A survey of self-management in dynamic software architecture specifications. In Proceedings of the 1st ACM SIGSOFT workshop on Selfmanaged systems, WOSS ’04, pages 28–33, New York, NY, USA, 2004. ACM. ISBN:1-58113-989-6. doi:10.1145/1075405.1075411. [BCK98] BELLARE, M.; CANETTI, R.; KRAWCZYK, H.: A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract). In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC ’98, pages 419– 428, New York, NY, USA, May 1998. ACM. ISBN:0-89791-962-9. doi:10.1145/276698.276854. [BCL+06] BRUNETON, E.; COUPAYE,T.;LECLERCQ, M.; QUÉMA,V.;STEFANI, J.-B.: The FRACTAL component model and its support in Java. Software: Practice and Experience, 36(11-12):1257–1284, 2006. ISSN:1097-024X. doi:10.1002/spe.767. Literature Page 253 [BDL04] BEHRMANN, G.; DAVID, A.; LARSEN, K. G.: A tutorial on Uppaal. In BERNARDO, M.; CORRADINI, F. (Eds.), Formal Methods for the Design of Real-Time Systems, number 3185 in Lecture Notes in Computer Science, pages 200–236. Springer Berlin Heidelberg, September 2004. ISBN:978-3-540-23068-7. doi:10.1007/978-3-540-30080-9_7. [BDL06a] BEHRMANN, G.; DAVID, A.; LARSEN,K.G.:A Tutorial on UPPAAL 4.0. Department of Computer Science, Aalborg University, Denmark, November 2006. [BDL+06b] BEHRMANN, G.; DAVID, A.; LARSEN, K. G.; PETTERSSON,P.;YI, W.; HENDRIKS,M.:UPPAAL 4.0. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST 2006, pages 125–126, Los Alamitos, CA, USA, September 2006. IEEE Computer Society. ISBN:0-7695-2665-9. doi:10.1109/QEST.2006.59. [BDM+98] BOZGA, M.; DAWS, C.; MALER, O.; OLIVERO, A.; TRIPAKIS, S.; YOVINE, S.: Kronos: A model-checking tool for real-time systems. In RAVN, A.; RISCHEL, H. (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, pages 298–302. Springer Berlin Heidelberg, 1998. ISBN:978- 3-540-65003-4. doi:10.1007/bfb0055357. [BDNG06] BARESI, L.; DINITTO, E.; GHEZZI, C.: Toward open-world software: Issue and challenges. Computer, 39(10):36 –43, October 2006. ISSN:0018-9162. doi:10.1109/mc.2006.362. [Bey01] BEYER, D.: Efficient reachability analysis and refinement checking of timed automata using BDDs. In MARGARIA,T.;MELHAM,T.F. (Eds.), Correct Hardware Design and Verification Methods, volume 2144 of Lecture Notes in Computer Science, pages 86–91. Springer Berlin Heidelberg, 2001. ISBN:978-3-540-42541-0. doi:10.1007/3- 540-44798-9_6. [BFHP09] BORDE, E.; FEILER, P. H.; HAÏK, G.; PAUTET, L.: Model driven code generation for critical and adaptative embedded systems. SIGBED Review, 6:10:1–10:5, October 2009. ISSN:1551-3688. doi:10.1145/1851340.1851352. [BGH+07] BURMESTER, S.; GIESE, H.; HENKLER, S.; HIRSCH, M.; TICHY, M.; GAMBUZZA, A.; MÜNCH, E.; VÖCKING, H.: Tool support for developing advanced mechatronic systems: Integrating the Fujaba Real- Time Tool Suite with CAMeL-View. In Proceedings of the 29th International Conference on Software Engineering, ICSE 2007, pages 801–804. IEEE Computer Society, May 2007. ISBN:0-7695-2828-7. doi:10.1109/ICSE.2007.88. Page 254 [BGH+13] BUREŠ,T.;GEROSTATHOPOULOS, I.; HNˇ ETYNKA,P.;KEZNIKL, J.; KIT, M.; PLÁŠIL, F.: DEECo: an ensemble-based component system. In Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, CBSE ’13, pages 81–90, New York, NY, USA, June 2013. ACM. ISBN:978-1-4503-2122-8. doi:10.1145/2465449.2465462. [BGK+96] BENGTSSON, J.; GRIFFIOEN,D.W.O.;KRISTOFFERSEN, K. J.; LARSEN, K. G.; LARSSON,F.;PETTERSSON,P.;YI, W.: Verification of an audio protocol with bus collision using UPPAAL. In ALUR, R.; HENZINGER, T. A. (Eds.), Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 244–256. Springer Berlin Heidelberg, July 1996. ISBN:978-3-540-61474-6. doi:10.1007/3-540- 61474-5_73. [BGN+10] BECKER, B.; GIESE, H.; NEUMANN, S.; SCHENCK, M.; TREFFER, A.: Model-based extension of AUTOSAR for architectural online reconfiguration. In GHOSH, S. (Ed.), Models in Software Engineering, volume 6002 of Lecture Notes in Computer Science, pages 83–97. Springer Berlin / Heidelberg, 2010. ISBN:978-3-642-12260-6. doi:10.1007/978-3-642-12261-3_9. [BGO06] BURMESTER, S.; GIESE, H.; OBERSCHELP, O.: Hybrid UML components for the design of complex self-optimizing mechatronic systems. In BRAZ, J.; ARAÚJO, H.; VIEIRA, A.; ENCARNAÇÃO, B. (Eds.), Informatics in Control, Automation and Robotics I, pages 281–288. Springer Netherlands, March 2006. ISBN:978-1-4020-4136-5. doi:10.1007/1- 4020-4543-3_34. [BGP13] BOYER,F.;GRUBER, O.; POUS, D.: Robust reconfigurations of component assemblies. In Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, pages 13–22, Piscataway, NJ, USA, May 2013. IEEE Computer Society. ISBN:978-1-4673-3076-3. doi:10.1109/ICSE.2013.6606547. [BGS05] BURMESTER, S.; GIESE, H.; SCHÄFER, W.: Model-driven architecture for hard real-time systems: From platform independent models to code. In HARTMAN, A.; KREISCHE, D. (Eds.), Proceedings of the European Conference on Model Driven Architecture – Foundations and Applications (ECMDA-FA ’05), volume 3748 of Lecture Notes in Computer Science, pages 25–40. Springer, Berlin/Heidelberg, November 2005. ISBN:978-3-540-30026-7. doi:10.1007/11581741_4. [BGSH11] BRINK, C.; GREENYER, J.; SCHÄFER,W.;HAHN, M.: Simulation von hybridem Verhalten in CAMeL-View. In GAUSEMEIER, Literature Page 255 J.; RAMMIG, F.-J.; SCHÄFER,W.;TRÄCHTLER, A. (Eds.), Wissenschaftsforum Intelligente Technische Systeme 2011, volume 294 of HNI-Verlagsschriftenreihe. Heinz Nixdorf Institut, Universität Paderborn, May 2011. ISBN:978-3942647137. [BGST05] BURMESTER, S.; GIESE, H.; SEIBEL, A.; TICHY, M.: Worst-case execution time optimization of story patterns for hard real-time systems. In Proceedings of the 3rd International Fujaba Days 2005, pages 71– 78, September 2005. [BHG87] BERNSTEIN, P. A.; HADZILACOS,V.;GOODMAN,N.:Concurrency Control and Recovery in Database Systems. Addison Wesley, 1987. ISBN:0-201-10715-5. [BHR09] BENNOUR, B.; HENRIO, L.; RIVERA, M.: A reconfiguration framework for distributed components. In Proceedings of the 2009 ESEC/FSE workshop on Software integration and evolution @ runtime, SINTER ’09, pages 49–56, New York, NY, USA, 2009. ACM. ISBN:978-1- 60558-681-6. doi:10.1145/1596495.1596509. [BIPM06] Bureau International des Poids et MesuresThe International System of Units (SI), 8th edition, 2006. [BK08] BAIER, C.; KATOEN, J.-P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA, 2008. ISBN:978-0-262-02649-9. [BK11] BARTELS, B.; KLEINE, M.: A CSP-based framework for the specification, verification, and implementation of adaptive systems. In Proceedings of the 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS ’11, pages 158– 167, New York, NY, USA, 2011. ACM. ISBN:978-1-4503-0575-4. doi:10.1145/1988008.1988030. [BK13] BOJIC, I.; KUSEK, M.: Self-synchronization of nonidentical machines in machine-to-machine systems. In IEEE 7th International Conference on Self-Adaptive and Self-Organizing Systems, SASO’13, pages 265–266. IEEE Computer Society, September 2013. doi:10.1109/saso.2013.39. [BKPPT01] BOTTONI,P.;KOCH, M.; PARISI-PRESICCE,F.;TAENTZER,G.:A visualization of OCL using collaborations. In GOGOLLA, M.; KOBRYN, C. (Eds.), UML 2001 — The Unified Modeling Language. Modeling Languages, Concepts, and Tools, volume 2185 of Lecture Notes in Computer Science, pages 257–271. Springer Berlin / Heidelberg, October 2001. ISBN:978-3-540-42667-7. doi:10.1007/3-540-45441-1_20. Page 262 [Est] Esterel TechnologiesSCADE Suite - Product Homepage. URL: http://www.esterel-technologies.com/products/ scade-suite/ [cited March 14, 2015]. [ETA] ETAS GmbHASCET Software-Produkte. URL: http://www.etas. com/de/products/ascet_software_products.php [cited March 14, 2015]. [EW92] ENDLER, M.; WEI, J.: Programming generic dynamic reconfigurations for distributed applications. In International Workshop on Configurable Distributed Systems, pages 68–79. IEEE, March 1992. ISBN:0-85296- 544-3. [FCT08] FENG, L.; CHEN, D.; TÖRNGREN, M.: Self configuration of dependent tasks for dynamically reconfigurable automotive embedded systems. In 47th IEEE Conference on Decision and Control, CDC 2008, pages 3737–3742, December 2008. ISBN:978-1-4244-3123-6. doi:10.1109/cdc.2008.4739195. [FFH05] FISH, A.; FLOWER, J.; HOWSE, J.: The semantics of augmented constraint diagrams. Journal of Visual Languages & Computing, 16(6):541 – 573, December 2005. ISSN:1045-926X. doi:10.1016/j.jvlc.2005.03.001. [FHTW05] FISH, A.; HOWSE, J.; TAENTZER, G.; WINKELMANN, J.: Two visualizations of OCL: a comparison. Technical Report VMG.05.1, University of Brighton, 2005. [FLGD+11] FREHSE, G.; LEGUERNIC, C.; DONZÉ, A.; COTTON, S.; RAY, R.; LEBELTEL, O.; RIPADO, R.; GIRARD, A.; DANG,T.;MALER,O.: SpaceEx: Scalable verification of hybrid systems. In GOPALAKRISHNAN, G.; QADEER, S. (Eds.), Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 379–395. Springer Berlin / Heidelberg, 2011. ISBN:978-3-642-22109-5. doi:10.1007/978- 3-642-22110-1_30. [FMB+09] FÜRST, S.; MÖSSINGER, J.; BUNZEL, S.; WEBER,T.;KIRSCHKEBILLER,F.;HEITKÄMPER,P.;KINKELIN, G.; NISHIKAWA, K.; LANGE,K.: AUTOSAR-aworldwide standard is on the road. In Proceedings of the 14th International VDI Congress Electronic Systems for Vehicles 2009, 2009. [FNTZ00] FISCHER,T.;NIERE, J.; TORUNSKI, L.; ZÜNDORF, A.: Story diagrams: A new graph rewrite language based on the Unified Modeling Language and Java. In EHRIG, H.; ENGELS, G.; KREOWSKI, H.- J.; ROZENBERG, G. (Eds.), Selected papers from the 6th International Workshop on Theory and Application of Graph Transformations (TAGT Literature Page 263 ’98), November 16-20, 1998, Paderborn, Germany, volume 1764 of Lecture Notes in Computer Science, pages 296 – 309. Springer Berlin / Heidelberg, 2000. ISBN:3-540-67203-6. doi:10.1007/978-3-540- 46464-8_21. [Fre05] FREHSE, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In MORARI, M.; THIELE, L. (Eds.), Proceedings of the Hybrid Systems 8th International Workshop on Computation and Control (HSCC 2005), volume 3414 of Lecture Notes in Computer Science, pages 258–273. Springer Berlin Heidelberg, March 2005. ISBN:3-540- 25108-1. doi:10.1007/978-3-540-31954-2_17. [Fri04] FRITZSON,P.:Principles of Object-Oriented Modeling and Simulation with Modelica 2.1. John Wiley & Sons, 1st edition, April 2004. ISBN:978-0471471639. [GAOR07] GÜDEMANN, M.; ANGERER, A.; ORTMEIER,F.;REIF, W.: Modeling of self-adaptive systems with SCADE. In IEEE International Symposium on Circuits and Systems, ISCAS 2007, pages 2922 – 2925. IEEE Computer Society, May 2007. ISBN:1-4244-0920-9. doi:10.1109/iscas.2007.377861. [GB03] GIESE, H.; BURMESTER, S.: Real-time statechart semantics. Technical Report tr-ri-03-239, Software Engineering Group, University of Paderborn, Paderborn, Germany, June 2003. [GBD07] GEIGER, L.; BUCHMANN,T.;DOTOR, A.: EMF code generation with Fujaba. In Proceedings of the Fifth International Fujaba Days, October 2007. [GBSO04] GIESE, H.; BURMESTER, S.; SCHÄFER,W.;OBERSCHELP, O.: Modular design and verification of component-based mechatronic systems with online-reconfiguration. In Proceedings of the 12th ACM SIGSOFT Foundations of Software Engineering, FSE 2004, pages 179–188, New York, NY, USA, November 2004. ACM. ISBN:1-58113-855-5. doi:10.1145/1029894.1029920. [GCH+04] GARLAN, D.; CHENG, S.-W.; HUANG, A.-C.; SCHMERL, B.; STEENKISTE, P.: Rainbow: architecture-based self-adaptation with reusable infrastructure. Computer, 37(10):46–54, October 2004. ISSN:0018-9162. doi:10.1109/mc.2004.175. [GCW+02] GENSSLER,T.;CHRISTOPH, A.; WINTER, M.; NIERSTRASZ, O.; DUCASSE, S.; WUYTS, R.; ARÉVALO, G.; SCHÖNHAGE, B.; MÜLLER,P.;STICH, C.: Components for embedded software: The PECOS approach. In Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, Page 264 CASES ’02, pages 19–26, New York, NY, USA, 2002. ACM. ISBN:1- 58113-575-0. doi:10.1145/581630.581634. [GCZ08] GOLDSBY, H. J.; CHENG,B.H.C.;ZHANG, J.: AMOEBA-RT: Runtime verification of adaptive software. In GIESE, H. (Ed.), Models in Software Engineering, volume 5002 of Lecture Notes in Computer Science, pages 212–224. Springer Berlin Heidelberg, 2008. ISBN:978-3- 540-69069-6. doi:10.1007/978-3-540-69073-3_23. [Gei13] GEISMANN, J.: Codegenerierung für LEGO Mindstorms - Roboter. Bachelor’s thesis, University of Paderborn, January 2013. [Ger13] GERKING, C.: Transparent Uppaal-based verifcation of Mechatronic- UML models. Master’s thesis, University of Paderborn, May 2013. [GFDK09] GAUSEMEIER, J.; FRANK, U.; DONOTH, J.; KAHL, S.: Specification technique for the description of self-optimizing mechatronic systems. Research in Engineering Design, 20:201–223, 2009. ISSN:0934-9839. doi:10.1007/s00163-008-0058-x. [GHS09] GIESE, H.; HILDEBRANDT, S.; SEIBEL, A.: Improved flexibility and scalability by interpreting story diagrams. In MARGARIA,T.;PADBERG, J.; TAENTZER, G. (Eds.), Proceedings of the Eighth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2009), volume 18. Electronic Communications of the EASST, 2009. [Gie03] GIESE, H.: A formal calculus for the compositional pattern-based design of correct real-time systems. Technical Report tr-ri-03- 240, Lehrstuhl für Softwaretechnik, Universität Paderborn, Paderborn, Deutschland, July 2003. [GJSH12] GHAFARI, M.; JAMSHIDI,P.;SHAHBAZI, S.; HAGHIGHI, H.: An architectural approach to ensure globally consistent dynamic reconfiguration of component-based systems. In Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering, CBSE ’12, pages 177–182, New York, NY, USA, June 2012. ACM. ISBN:978- 1-4503-1345-2. doi:10.1145/2304736.2304765. [GKP08] GAUSEMEIER, J.; KAHL, S.; POOK, S.: From mechatronics to selfoptimizing systems. In Self-optimizing Mechatronic Systems: Design the Future, 7th International Heinz Nixdorf Symposium, volume 223. HNI Verlagsschriftenreihe, Paderborn, February 2008. [GMW00] GARLAN, D.; MONROE,R.T.;WILE, D.: Acme: architectural description of component-based systems. In LEAVENS,G.T.;SITARAMAN, M. (Eds.), Foundations of component-based systems, pages 47– Literature Page 265 67. Cambridge University Press, New York, NY, USA, March 2000. ISBN:0-521-77164-1. [GOS09] GUARINO, N.; OBERLE, D.; STAAB, S.: What is an ontology? In STAAB, S.; STUDER, R. (Eds.), Handbook on Ontologies, International Handbooks on Information Systems, pages 1–17. Springer Berlin Heidelberg, 2009. ISBN:978-3-540-70999-2. doi:10.1007/978-3-540- 92673-3_0. [Gos14] GOSCHIN, S.: Synthesis of extended hierarchical real-time behavior. Master’s thesis, University of Paderborn, February 2014. [GPVW96] GERTH, R.; PELED, D.; VARDI,M.Y.;WOLPER, P.: Simple on-the- fly automatic verification of linear temporal logic. In Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pages 3–18, London, UK, 1996. Chapman & Hall, Ltd. ISBN:0-412-71620-8. [Gra] Graphviz Open Source TeamGraphviz - Graph Visualization Software. URL: http://www.graphviz.org/ [cited March 14, 2015]. [Gre11] GREENYER,J.:Scenario-based Design of Mechatronic Systems. PhD thesis, University of Paderborn, October 2011. [Gro01] GROUP,O.M.:OMG Unified Modeling Language Specification 1.4, September 2001. Document formal/2001-09-67. URL: http://www. omg.org/spec/UML/1.4/. [Gro05] GROUP,O.M.:Unified Modeling Language (UML) 2.0 Superstructure Specification, July 2005. Document formal/2005-07-04. URL: http: //www.omg.org/spec/UML/2.0/. [Gro09] GRONBACK,R.C.:Eclipse Modeling Project – A Domain-Specific Language (DSL) Toolkit. The Eclipse Series. Addison-Wesley, 1st edition, March 2009. ISBN:978-0321534071. [Gro10] GROUP,O.M.:OMG Systems Modeling Language (OMG SysML), June 2010. Document formal/10-06-02. URL: http://www.sysml. org/specs/. [Gro11a] GROUP,O.M.:Common Object Request Broker Architecture (CORBA) Specification - Part 3: CORBA Component Model, November 2011. Document formal/2011-11-03. URL: http://www.omg.org/spec/ CORBA/3.2/. [Gro11b] GROUP,O.M.:Query/View/Transformation (QVT) 1.1, January 2011. Document formal/2011-01-01. URL: http://www.omg.org/spec/ QVT/1.1/. Page 266 [Gro11c] GROUP,O.M.:Unified Modeling Language (UML) 2.4.1 Superstructure Specification, August 2011. Document formal/2011-08-06. [Gro12] GROUP,O.M.:Object Constraint Language (OCL) 2.3.1, January 2012. Document formal/2012-01-01. URL: http://www.omg.org/ spec/OCL/2.3.1/. [Gro14] GROUP,O.M.:Model Driven Architecture (MDA) – MDA Guide rev. 2.0, June 2014. Document – ormsc/14-06-01. URL: http://www. omg.org/cgi-bin/doc?ormsc/14-06-01. [GRS09] GAUSEMEIER, J.; RAMMIG, F.-J.; SCHÄFER,W. (Eds.)Selbstoptimierende Systeme des Maschinenbaus – Definitionen, Anwendungen, Konzepte, volume 234. HNI-Verlagsschriftenreihe, Paderborn, 1st edition, January 2009. ISBN:978-3-939350-53-8. [GRS14] GAUSEMEIER, J.; RAMMIG, F.-J.; SCHÄFER, W. (Eds.)Design Methodology for Intelligent Technical Systems. Lecture Notes in Mechanical Engineering. Springer, 2014. ISBN:978-3-642-45434-9. [GS04] GARLAN, D.; SCHMERL, B.: Using architectural models at runtime: Research challenges. In OQUENDO,F.;WARBOYS, B. C.; MORRISON, R. (Eds.), Software Architecture, volume 3047 of Lecture Notes in Computer Science, pages 200–205. Springer Berlin Heidelberg, 2004. ISBN:978-3-540-22000-8. doi:10.1007/978-3-540-24769-2_15. [GS13] GIESE, H.; SCHÄFER, W.: Model-driven development of safe selfoptimizing mechatronic systems with MechatronicUML. In CÁMARA, J.; DE LEMOS, R.; GHEZZI, C.; LOPES, A. (Eds.), Assurances for Self-Adaptive Systems, volume 7740 of Lecture Notes in Computer Science, pages 152–186. Springer Berlin Heidelberg, January 2013. ISBN:978-3-642-36248-4. doi:10.1007/978-3-642-36249-1_6. [GSB+08] GOLDSBY, H. J.; SAWYER,P.;BENCOMO, N.; CHENG,B.H.C.; HUGHES, D.: Goal-based modeling of dynamically adaptive system requirements. In 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems, ECBS 2008., pages 36–45. IEEE Computer Society, March 2008. ISBN:0-7695- 3141-5. doi:10.1109/ecbs.2008.22. [GSG+09] GAUSEMEIER, J.; SCHÄFER,W.;GREENYER, J.; KAHL, S.; POOK, S.; RIEKE, J.: Management of cross-domain model consistency during the development of advanced mechatronic systems. In BERGENDAHL, M. N.; GRIMHEDEN, M.; LEIFER, L.; SKOGSTAD,P.;LINDEMANN, U. (Eds.), Proceedings of the 17th International Conference on Engineering Design, volume 6, Design Methods and Tools of ICED’09, pages 1–12. Design Society, August 2009. ISBN:978-1-904670-10-0. Literature Page 267 [GSR05] GEIGER, L.; SCHNEIDER, C.; RECKORD, C.: Template- and modelbased code generation for MDA-tools. In GIESE, H.; ZÜNDORF,A. (Eds.), Proceedings of the Third International Fujaba Days 2005, volume tr-ri-06-275 of Technical Report, pages 1–6. University of Paderborn, September 2005. [GTB+03] GIESE, H.; TICHY, M.; BURMESTER, S.; SCHÄFER,W.;FLAKE, S.: Towards the compositional verification of real-time UML designs. In Proceedings of the 9th European Software Engineering Conference Held Jointly with 11th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE’03, pages 38–47, New York, NY, USA, September 2003. ACM. ISBN:1-58113-743-5. doi:10.1145/940071.940078. [GTS14] GAUSEMEIER, J.; TRÄCHTLER, A.; SCHÄFER, W. (Eds.)Semantische Technologien im Entwurf mechatronischer Systeme: Effektiver Austausch von Lösungswissen in Branchenwertschöpfungsketten. Carl Hanser Verlag, München, June 2014. ISBN:978-3446436305. [GV14] GAUSEMEIER, J.; VASSHOLZ, M.: Design methodology for selfoptimizing systems. In GAUSEMEIER, J.; RAMMIG, F.-J.; SCHÄFER, W. (Eds.), Design Methodology for Intelligent Technical Systems, chapter 3.1, pages 66–69. Springer-Verlag, Heidelberg, Germany, January 2014. ISBN:978-3-642-45434-9. [Ham05] HAMON, G.: A denotational semantics for Stateflow. In Proceedings of the 5th ACM international conference on Embedded software, EMSOFT ’05, pages 164–172, New York, NY, USA, 2005. ACM. ISBN:1- 59593-091-4. doi:10.1145/1086228.1086260. [HB07] HNˇ ETYNKA,P.;BUREŠ, T.: Advanced features of hierarchical component models. In ZENDULKA, J. (Ed.), Proceedings of the 10th International Conference on Information System Implementation and Modeling, ISIM’07, pages 1–8. CEUR-WS.org Vol-252, April 2007. [HBRV10] HEGEDÜS, Á.; BERGMANN, G.; RATH, I.; VARRÓ, D.: Backannotation of simulation traces with change-driven model transformations. In 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM’10, pages 145–155. IEEE Computer Society, September 2010. ISBN:978-1-4244-8289-4. doi:10.1109/sefm.2010.28. [HC01] HEINEMAN,G.T.;COUNCILL, W. T. (Eds.)Component-based Software Engineering: Putting the Pieces Together. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2001. ISBN:0-201- 70485-4. Page 268 [HCH12] HANG,Y.;CARLSON, J.; HANSSON, H.: Towards mode switch handling in component-based multi-mode systems. In Proceedings of the 15th ACM SIGSOFT Symposium on Component Based Software Engineering, CBSE’12, pages 183–188, New York, NY, USA, June 2012. ACM. ISBN:978-1-4503-1345-2. doi:10.1145/2304736.2304766. [Hen96] HENZINGER, T. A.: The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS ’96, pages 278–292, Los Alamitos, CA, USA, July 1996. IEEE Computer Society. ISBN:0-8186-7463-6. doi:10.1109/lics.1996.561342. [Hen12] HENKLER,S.:Ein komponentenbasierter, modellgetriebener Softwareentwicklungsansatz für vernetzte, mechatronische Systeme. PhD thesis, University of Paderborn, Warburger Str. 100, Paderborn, Germany, June 2012. [HESV91] HSU, A.; ESKAFI,F.;SACHS, S.; VARAIYA, P.: Design of platoon maneuver protocols for IVHS. Technical Report UCB-ITS-PRR-91-6, UC Berkeley: California Partners for Advanced Transit and Highways (PATH), April 1991. URL: http://escholarship.org/uc/item/ 89c6p0cn. [HH13] HANG,Y.;HANSSON, H.: Handling multiple mode switch scenarios in component-based multi-mode systems. In Proceedings of the 20th Asia-Pacific Software Engineering Conference, volume 1 of APSEC’13, pages 404–413. IEEE Computer Society, December 2013. ISBN:978- 1-4799-2143-0. doi:10.1109/apsec.2013.61. [HHG08] HIRSCH, M.; HENKLER, S.; GIESE, H.: Modeling collaborations with dynamic structural adaptation in Mechatronic UML. In Proceedings of the 2008 international workshop on Software engineering for adaptive and self-managing systems, SEAMS ’08, pages 33–40, New York, NY, USA, May 2008. ACM. ISBN:978-1-60558-037-1. doi:10.1145/1370018.1370026. [HHMWT00] HENZINGER,T.;HOROWITZ, B.; MAJUMDAR, R.; WONG-TOI,H.: Beyond HyTech: Hybrid systems analysis using interval numerical methods. In LYNCH, N.; KROGH, B. (Eds.), Hybrid Systems: Computation and Control, volume 1790 of Lecture Notes in Computer Science, pages 130–144. Springer Berlin / Heidelberg, March 2000. ISBN:978- 3-540-67259-3. doi:10.1007/3-540-46430-1_14. [HHR09] HARHURIN, A.; HARTMANN, J.; RATIU, D.: Motivation and formal foundations of a comprehensive modeling theory for embedded systems. Technical Report TUM-I0924, Institut für Informatik, Technische Universität München, September 2009. Literature Page 269 [HHWT97] HENZINGER, T. A.; HO, P.-H.; WONG-TOI, H.: HYTECH: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer (STTT), 1(1-2):110–122, 1997. ISSN:1433-2779. doi:10.1007/s100090050008. [HIM98] HIRSCH, D.; INVERARDI,P.;MONTANARI, U.: Graph grammars and constraint solving for software architecture styles. In Proceedings of the third international workshop on Software architecture, ISAW ’98, pages 69–72, New York, NY, USA, 1998. ACM. ISBN:1-58113-081-3. doi:10.1145/288408.288426. [Hir08] HIRSCH,M.:Modell-basierte Verifikation von vernetzten mechatronischen Systemen. PhD thesis, University of Paderborn, Warburger Str. 100, Paderborn, Germany, September 2008. [HKMU06] HIRSCH, D.; KRAMER, J.; MAGEE, J.; UCHITEL, S.: Modes for software architectures. In GRUHN,V.;OQUENDO, F. (Eds.), Software Architecture, volume 4344 of Lecture Notes in Computer Science, pages 113–126. Springer Berlin Heidelberg, 2006. ISBN:978-3-540-69271-3. doi:10.1007/11966104_9. [HKPV98] HENZINGER, T. A.; KOPKE,P.W.;PURI, A.; VARAIYA,P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94 – 124, 1998. ISSN:0022-0000. doi:10.1006/jcss.1998.1581. [HM03] HAREL, D.; MARELLY,R.:Come, Let’s Play: Scenario-Based Programming Using LSC’s and the Play-Engine. Springer-Verlag New York, Secaucus, NJ, USA, 2003. ISBN:3540007873. [HM08a] HAREL, D.; MAOZ, S.: Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and System Modeling, 7(2):237– 252, May 2008. ISSN:1619-1366. doi:10.1007/s10270-007-0054-z. [HMTN+08] HÄNNINEN, K.; MÄKI-TURJA, J.; NOLIN, M.; LINDBERG, M.; LUNDBÄCK, J.; LUNDBÄCK, K.-L.: The Rubus component model for resource constrained real-time systems. In 3rd IEEE International Symposium on Industrial Embedded Systems, SIES 2008, pages 177– 183. IEEE Computer Society, June 2008. ISBN:978-1-4244-1994-4. doi:10.1109/SIES.2008.4577697. [HNSY94] HENZINGER, T. A.; NICOLLIN, X.; SIFAKIS, J.; YOVINE, S.: Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, June 1994. ISSN:0890-5401. doi:10.1006/inco.1994.1045. Page 270 [Hoa85] HOARE,C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, 1985. ISBN:978- 0131532717. [HOG04] HESTERMEYER,T.;OBERSCHELP, O.; GIESE, H.: Structured information processing for self-optimizing mechatronic systems. In ARAÚJO, H.; VIEIRA, A.; BRAZ, J.; ENCARNAÇÃO, B.; CARVALHO, M. (Eds.), Proceedings of 1st International Conference on Informatics in Control, Automation and Robotics, ICINCO 2004, pages 230–237. INSTICC Press, August 2004. [HP06] HNˇ ETYNKA,P.;PLÁŠIL, F.: Dynamic reconfiguration and access to services in hierarchical component models. In GORTON, I.; HEINEMAN, G.; CRNKOVI ´ C, I.; SCHMIDT, H.; STAFFORD, J.; SZYPERSKI, C.; WALLNAU, K. (Eds.), Component-Based Software Engineering, volume 4063 of Lecture Notes in Computer Science, pages 352– 359. Springer Berlin / Heidelberg, 2006. ISBN:978-3-540-35628-8. doi:10.1007/11783565_27. [HPB+10] HOŠEK,P.;POP,T.;BUREŠ,T.;HNˇ ETYNKA,P.;MALOHLAVA,M.: Comparison of component frameworks for real-time embedded systems. In GRUNSKE, L.; REUSSNER, R.; PLÁŠIL, F. (Eds.), Component Based Software Engineering, volume 6092 of Lecture Notes in Compute Science, pages 21–36. Springer, Berlin/Heidelberg, 2010. ISBN:978-3- 642-13237-7. doi:10.1007/978-3-642-13238-4_2. [HQCH13] HANG,Y.;QIN, H.; CARLSON, J.; HANSSON, H.: Mode switch handling for the ProCom component model. In Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering, CBSE ’13, pages 13–22, New York, NY, USA, June 2013. ACM. ISBN:978-1-4503-2122-8. doi:10.1145/2465449.2465451. [HR04] HUTH, M.; RYAN,M.:Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, UK, 2nd edition, 2004. ISBN:978-0-521-54310-1. [HR07] HAMON, G.; RUSHBY, J.: An operational semantics for Stateflow. International Journal on Software Tools for Technology Transfer (STTT), 9(5):447–456, July 2007. ISSN:1433-2779. doi:10.1007/s10009-007- 0049-7. [HTS+08a] HENKE, C.; TICHY, M.; SCHNEIDER,T.;BÖCKER, J.; SCHÄFER, W.: Organization and control of autonomous railway convoys. In Proceedings of the 9th International Symposium on Advanced Vehicle Control, AVEC’08, pages 318–323, October 2008. Literature Page 271 [HTS+08b] HENKE, C.; TICHY, M.; SCHNEIDER,T.;BÖCKER, J.; SCHÄFER, W.: System architecture and risk management for autonomous railway convoys. In Proceedings of the 2nd Annual IEEE International Systems Conference,, pages 1–8. IEEE Computer Society, April 2008. ISBN:978-1-4244-2149-7. doi:10.1109/SYSTEMS.2008.4518986. [HZ14] HÖLSCHER, C.; ZIMMER, D.: Intelligent drive module (iDM). In GAUSEMEIER, J.; RAMMIG, F.-J.; SCHÄFER, W. (Eds.), Design Methodology for Intelligent Technical Systems, chapter 2.1.2, pages 33– 36. Springer, Heidelberg, Germany, January 2014. [IBM06] IBM: An architectural blueprint for autonomic computing. Autonomic computing white paper, IBM, June 2006. [IEC96] IEC: Graphical symbols for diagrams. IEC 60617, 1996. [IEC10] IEC: Functional safety of electrical/electronic/programmable electronic safety-related systems. IEC 61508 Edition 2.0, April 2010. [IEE08] IEEE: IEEE standard for a precision clock synchronization protocol for networked measurement and control systems. IEEE Std 1588- 2008 (Revision of IEEE Std 1588-2002), pages c1–269, July 2008. doi:10.1109/ieeestd.2008.4579760. [IETF81] Internet Engineering Task Force (IETF)RFC793 - Transmission Control Protocol, September 1981. URL: http://tools.ietf.org/html/ rfc793. [ISO10] ISO: Systems and software engineering – vocabulary. ISO/IEC/IEEE 24765:2010(E), pages 1 –418, December 2010. doi:10.1109/ieeestd.2010.5733835. [ISO11a] ISO: Road vehicles – functional safety. ISO26262:2011, November 2011. [IUH11] ISHII, D.; UEDA, K.; HOSOBE, H.: An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. International Journal on Software Tools for Technology Transfer, 13(5):449–461, October 2011. ISSN:1433-2779. doi:10.1007/s10009-011-0193-y. [IW95] INVERARDI,P.;WOLF, A. L.: Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Transactions on Software Engineering, 21(4):373–386, April 1995. ISSN:0098-5589. doi:10.1109/32.385973. [IW14] IFTIKHAR, M. U.; WEYNS, D.: Assuring system goals under uncertainty with active formal models of self-adaptation. In Companion Proceedings of the 36th International Conference on Software Engineering, ICSE Companion 2014, pages 604–605, New Page 278 [NNSS07] NARTEN,T.;NORDMARK, E.; SIMPSON, W. A.; SOLIMAN,H.: RFC4861 - Neighbor Discovery for IP version 6 (IPv6). Network Working Group, September 2007. URL: http://tools.ietf.org/ html/rfc4861. [OHY11] OH, J.; HARMAN, M.; YOO, S.: Transition coverage testing for Simulink/Stateflow models using messy genetic algorithms. In Proceedings of the 13th Annual Conference on Genetic and Evolutionary Computation, GECCO ’11, pages 1851–1858, New York, NY, USA, 2011. ACM. ISBN:978-1-4503-0557-0. doi:10.1145/2001576.2001825. [OMT98] OREIZY,P.;MEDVIDOVI ´ C, N.; TAYLOR, R. N.: Architecturebased runtime software evolution. In Proceedings of the 20th international conference on Software engineering, ICSE ’98, pages 177– 186. IEEE Computer Society, April 1998. ISBN:0-8186-8368-6. doi:10.1109/ICSE.1998.671114. [OMT+08] OSMIC, S.; MÜNCH, E.; TRÄCHTLER, A.; HENKLER, S.; SCHÄFER, W.; GIESE, H.; HIRSCH, M.: Safe online-reconfiguration of selfoptimizing mechatronic systems. In GAUSEMEIER, J.; RAMMIG, F. J.; SCHÄFER, W. (Eds.), Selbstoptimierende mechatronische Systeme: Die Zukunft gestalten. 7. Internationales Heinz Nixdorf Symposium für industrielle Informationstechnik, pages 411–426, February 2008. [Ora13] ORACLE:JSR 345: Enterprise JavaBeansTM, Version 3.2, EJB Core Contracts and Requirements, April 2013. URL: http://download.oracle.com/otn-pub/jcp/ejb-3_ 2-fr-eval-spec/ejb-3_2-core-fr-spec.pdf [cited March 14, 2015]. [PBKS07] PRETSCHNER, A.; BROY, M.; KRÜGER, I. H.; STAUNER, T.: Software engineering for automotive systems: A roadmap. In 2007 Future of Software Engineering, FOSE ’07, pages 55–71, Washington, DC, USA, 2007. IEEE Computer Society. ISBN:0-7695-2829-5. doi:10.1109/fose.2007.22. [PDM+14] POHLMANN, U.; DZIWOK, S.; MEYER, M.; TICHY, M.; THIELE, S.: A Modelica coordination pattern library for cyber-physical systems. In Proceedings of the 7th International ICST Conference on Simulation Tools and Techniques, SIMUTools’14, pages 76–85, Brussels, Belgium, March 2014. ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering). ISBN:978- 1-63190-007-5. doi:10.4108/icst.simutools.2014.254640. [PDS+12] POHLMANN, U.; DZIWOK, S.; SUCK, J.; WOLF, B.; LOH, C. C.; TICHY, M.: A Modelica library for real-time coordination modeling. In Proceedings of the 9th International MODELICA Con- Literature Page 279 ference, pages 365–374. DLR - Robotics and Mechatronics Center, Modelica Association, Linköping University Electronic Press, Linköpings universitet, September 2012. ISBN:978-91-7519-826-2. doi:10.3384/ecp12076365. [Pea84] PEARL,J.:Heuristics: intelligent search strategies for computer problem solving. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1984. ISBN:0-201-05594-5. [PHMG14] POHLMANN, U.; HOLTMANN, J.; MEYER, M.; GERKING, C.: Generating Modelica models from software specifications for the simulation of cyber-physical systems. In Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications, SEAA ’14, pages 191–198. IEEE Computer Society, August 2014. doi:10.1109/SEAA.2014.18. [PKH+11] POP,T.;KEZNIKL, J.; HOŠEK,P.;MALOHLAVA, M.; BUREŠ, T.; HNˇ ETYNKA, P.: Introducing support for embedded and realtime devices into existing hierarchical component system: Lessons learned. In 9th International Conference on Software Engineering Research, Management and Applications, SERA’11, pages 3 –11. IEEE Computer Society, August 2011. ISBN:978-1-4577-1028-5. doi:10.1109/sera.2011.14. [PKP07] PAIZ, C.; KELTELHOIT, B.; PORRMANN, M.: A design framework for FPGA-based dynamically reconfigurable digital controllers. In IEEE International Symposium on Circuits and Systems, ISCAS 2007, pages 3708–3711. IEEE Computer Society, May 2007. ISBN:1-4244-0920-9. doi:10.1109/iscas.2007.378648. [PLM12] PANZICA LAMANNA, V.: Local dynamic update for component-based distributed systems. In Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering, CBSE ’12, pages 167–176, New York, NY, USA, 2012. ACM. ISBN:978-1-4503-1345-2. doi:10.1145/2304736.2304764. [Plu82] PLUMMER,D.C.:RFC826 - An Ethernet Address Resolution Protocol. Network Working Group, November 1982. URL: http://tools. ietf.org/html/rfc826. [Plu06] PLUMMER, A. R.: Model-in-the-loop testing. Proceedings of the Institution of Mechanical Engineers, Part I: Journal of Systems and Control Engineering, 220(3):183–199, May 2006. ISSN:0959-6518. doi:10.1243/09596518jsce207. [PMDB14] POHLMANN, U.; MEYER, M.; DANN, A.; BRINK, C.: Viewpoints and views in hardware platform modeling for safe deployment. In Page 280 Proceedings of the 2nd Workshop on View-Based, Aspect-Oriented and Orthographic Software Modelling, VAO ’14, pages 23:23–23:30, New York, NY, USA, July 2014. ACM. ISBN:978-1-4503-2900-2. doi:10.1145/2631675.2631682. [Pnu77] PNUELI, A.: The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46–57. IEEE Computer Society Press, October 1977. doi:10.1109/SFCS.1977.32. [Poh13] POHLMANN, U.: Safe deployment for reconfigurable cyber-physical systems. In Proceedings of the 18th International Doctoral Symposium on Components and Architecture, WCOP ’13, pages 31–36, New York, NY, USA, June 2013. ACM. ISBN:978-1-4503-2125-9. doi:10.1145/2465498.2465503. [Pos80] POSTEL,J.: User Datagram Protocol. Internet Engineering Task Force (IETF), August 1980. URL: http://tools.ietf.org/html/ rfc768. [PPO+12] POP,T.;PLÁŠIL,F.;OUTLY, M.; MALOHLAVA, M.; BUREŠ,T.: Property networks allowing oracle-based mode-change propagation in hierarchical components. In Proceedings of the 15th ACM SIGSOFT Symposium on Component Based Software Engineering, CBSE’12, pages 93–102, New York, NY, USA, June 2012. ACM. ISBN:978-1- 4503-1345-2. doi:10.1145/2304736.2304753. [Pri13] PRIESTERJAHN,C.:Analyzing Self-healing Operations in Mechatronic Systems. PhD thesis, University of Paderborn, Warburger Str. 100, Paderborn, Germany, August 2013. [PSR+12] POHLMANN, U.; SCHÄFER,W.;REDDEHASE, H.; RÖCKEMANN, J.; WAGNER, R.: Generating functional mockup units from software specifications. In Proceedings of the 9th International MODELICA Conference, pages 765–774. Linköping University Electronic Press, Linköpings universitet, September 2012. ISBN:978-91-7519-826-2. doi:10.3384/ecp12076765. [PST13] PRIESTERJAHN, C.; STEENKEN, D.; TICHY, M.: Timed hazard analysis of self-healing systems. In CÁMARA, J.; DE LEMOS, R.; GHEZZI, C.; LOPES, A. (Eds.), Assurances for Self-Adaptive Systems, volume 7740 of Lecture Notes in Computer Science, pages 112–151. Springer Berlin Heidelberg, January 2013. ISBN:978-3-642-36248-4. doi:10.1007/978-3-642-36249-1_5. [PTD+14] POHLMANN, U.; TRSEK, H.; DÜRKOP, L.; DZIWOK, S.; OESTERSÖTEBIER, F.: Application of an intelligent network architecture on Literature Page 281 a cooperative cyber-physical system: An experience report. In Proceedings of the 19th IEEE International Conference on Emerging Technology and Factory Automation, ETFA’14, pages 1–6. IEEE Computer Society, September 2014. doi:10.1109/ETFA.2014.7005358. [PTH+10] PRIESTERJAHN, C.; TICHY, M.; HENKLER, S.; HIRSCH, M.; SCHÄFER, W.: Fujaba4Eclipse Real-Time Tool Suite. In GIESE, H.; KARSAI, G.; LEE, E. A.; RUMPE, B.; SCHÄTZ, B. (Eds.), Model- Based Engineering of Embedded Real-Time Systems (MBEERTS), volume 6100 of Lecture Notes in Computer Science, chapter 12, pages 309–315. Springer Berlin Heidelberg, 2010. ISBN:978-3-642-16276- 3. doi:10.1007/978-3-642-16277-0_12. [PV14] PANUNZIO, M.; VARDANEGA, T.: A component-based process with separation of concerns for the development of embedded real-time software systems. Journal of Systems and Software, 96:105 – 121, October 2014. ISSN:0164-1212. doi:10.1016/j.jss.2014.05.076. [PWT+08] PROCHAZKA, M.; WARD, R.; TUMA,P.;HNˇ ETYNKA,P.;ADAMEK, J.: A component-oriented framework for spacecraft on-board software. In Proceedings of DASIA 2008, DAta Systems In Aerospace, Palma de Mallorca, European Space Agency Report Nr. SP-665, May 2008. ISBN:978-92-9221-229-2. [Qua] Quanser Inc.Quanser Real-Time Control Software (QUARC). URL: http://www.quarcservice.com/ReleaseNotes/files/ dynamic_reconfiguration.html [cited March 14, 2015]. [RC08] RAMIREZ, A. J.; CHENG, B. H. C.: Verifying and analyzing adaptive logic through UML state models. In 1st International Conference on Software Testing, Verification, and Validation, pages 529– 532. IEEE Computer Society, April 2008. ISBN:978-0-7695-3127-4. doi:10.1109/icst.2008.67. [RCC10] ROBINSON,T.;CHAN, E.; COELINGH, E.: Operating platoons on public motorways: An introduction to the SARTRE platooning programme. In 17th World Congress on Intelligent Transport Systems, October 2010. [Rei07] REINEKE, P.: Model checking von Story-Diagrammen mittels GROOVE. Bachelor’s thesis, University of Paderborn, July 2007. [Ren06] RENSINK, A.: Model checking quantified computation tree logic. In BAIER, C.; HERMANNS, H. (Eds.), CONCUR 2006 – Concurrency Theory, volume 4137 of Lecture Notes in Computer Science, pages 110–125. Springer Berlin Heidelberg, August 2006. ISBN:978-3-540- 37376-6. doi:10.1007/11817949_8. Page 282 [Ren07] RENSINK, A.: Isomorphism checking in GROOVE. In ZÜNDORF, A.; VARRÓ, D. (Eds.), Proceedings of the Third International Workshop on Graph Based Tools (GraBaTs 2006), volume 1 of Electronic Communications of the EASST. European Association of Software Science and Technology, September 2007. [Ren08] RENSINK, A.: Explicit state model checking for graph grammars. In DEGANO,P.;NICOLA, R.; MESEGUER, J. (Eds.), Concurrency, Graphs and Models, volume 5065 of Lecture Notes in Computer Science, pages 114–132. Springer Berlin Heidelberg, 2008. ISBN:978-3- 540-68676-7. doi:10.1007/978-3-540-68679-8_8. [RJC12] RAMIREZ, A. J.; JENSEN, A. C.; CHENG, B. H. C.: A taxonomy of uncertainty for dynamically adaptive systems. In Proceedings of the 2012 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems, SEAMS’12, pages 99 –108. IEEE Computer Society, June 2012. ISBN:978-1-4673-1788-7. doi:10.1109/seams.2012.6224396. [Roz97] ROZENBERG,G.:Handbook of graph grammars and computing by graph transformation: volume I. foundations. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1997. ISBN:9810228848. [RS08a] REEVES, S.; STREADER, D.: General refinement, part one: Interfaces, determinism and special refinement. Electronic Notes in Theoretical Computer Science, 214:277–307, June 2008. ISSN:1571-0661. doi:10.1016/j.entcs.2008.06.013. [RS08b] REEVES, S.; STREADER, D.: General refinement, part two: Flexible refinement. Electronic Notes in Theoretical Computer Science, 214:309–329, June 2008. ISSN:1571-0661. doi:10.1016/j.entcs.2008.06.014. [SBPM08] STEINBERG, D.; BUDINSKY,F.;PATERNOSTRO, M.; MERKS,E.: EMF: Eclipse Modeling Framework. The Eclipse Series. Addison- Wesley, 2nd edition, December 2008. ISBN:978-0321331885. [Sch95] SCHÜRR, A.: Specification of graph translators with triple graph grammars. In MAYR,E.W.;SCHMIDT, G.; TINHOFER, G. (Eds.), Graph- Theoretic Concepts in Computer Science, volume 903 of Lecture Notes in Computer Science, pages 151–163. Springer Berlin / Heidelberg, June 1995. ISBN:978-3-540-59071-2. doi:10.1007/3-540-59071-4_45. [Sch06] SCHMIDT, D. C.: Guest editor’s introduction: Model-driven engineering. Computer, 39(2):25–31, 2006. ISSN:0018-9162. doi:10.1109/mc.2006.58. Literature Page 283 [SGM02] SZYPERSKI, C.; GRUNTZ, D.; MURER,S.:Component Software - Beyond Object-Oriented Programming. Addison-Wesley, 2nd edition, 2002. ISBN:0-201-74572-0. [SH99] SRISURESH,P.;HOLDREGE,M.:RFC2663 - IP Network Address Translator (NAT) Terminology and Considerations. Network Working Group, August 1999. URL: http://tools.ietf.org/html/ rfc2663. [Sha02] SHAW, M.: "self-healing": softening precision to avoid brittleness: position paper for WOSS ’02: workshop on self-healing systems. In Proceedings of the first workshop on Self-healing systems, WOSS ’02, pages 111–114, New York, NY, USA, 2002. ACM. ISBN:1-58113-609- 9. doi:10.1145/582128.582152. [SHS12] STOCKMANN, L.; HOLLER, D.; SPENNEBERG, D.: Early simulation and testing of virtual ECUs for electric vehicles. In International Battery, Hybrid and Fuel Cell Electric Vehicle Symposium (EVS26), May 2012. [SK95] SLONNEGER, K.; KURTZ,B.L.:Formal Syntax and Semantics of Programming Languages - A Laboratory Based Approach. Addison- Wesley, 1995. ISBN:0-201-65697-3. [SK00] SILVA, B. I.; KROGH, B. H.: Formal verification of hybrid systems using CheckMate: A case study. In Proceedings of the 2000 American Control Conference, volume 3, pages 1679 –1683. IEEE Computer Society, June 2000. ISBN:0-7803-5519-9. doi:10.1109/acc.2000.879487. [SK06] STRUNK, E. A.; KNIGHT, J. C.: Dependability through assured reconfiguration in embedded system software. IEEE Transactions on Dependable and Secure Computing, 3(3):172 –187, July-Sept. 2006. ISSN:1545-5971. doi:10.1109/tdsc.2006.33. [SLT09] SIMONOT-LION,F.;TRINQUET, Y.: Vehicle functional domains and their requirements. In NAVET, N.; SIMONOT-LION, F. (Eds.), Automotive Embedded Systems Handbook, Industrial Information Technology Series, chapter 1. CRC Press, Boca Raton, FL, USA, 2009. ISBN:978- 0-8493-8026-6. [SP12] STÜRMER, I.; POHLHEIM, H.: Model quality assessment in practice: How to measure and assess the quality of software models during the embedded software development process. In Proceedings of the International Congress of Embedded Real Time Software and Systems, ERTS’12, February 2012. [Document text truncated for crawler view.]