ABSTRACT

CONTENTS 6.1 Introduction 132 6.2 Goals and Architecture of Resilient CPS 133

6.2.1 Goal-Oriented Development and Reconguration 133 6.2.2 Generic Requirements for Goal-Oriented Resilient Systems 134 6.2.3 General Approach of Developing Distributed Systems in Event-B 135

6.3 Modeling and Renement in Event-B 135 6.3.1 Event-B Renement 136 6.3.2 Modularization 137

6.4 Deriving Resilient Architecture 138 6.4.1 Functional Decomposition by Renement 138 6.4.2 Second Renement 139

6.4.2.1 Introducing System Components 139 6.4.2.2 Modeling Dependencies between System Elements 140 6.4.2.3 Modeling Task Execution 142 6.4.2.4 Toward Modeling System Reconguration 143

6.4.3 Representing Manager’s Local Knowledge 144 6.4.3.1 Local Knowledge about Attached Workers and Responsible

Tasks 145 6.4.4 Explicit Model of Component Failures 146

6.5 Modeling of Communication 146 6.5.1 Communication between Managers 146 6.5.2 Communication between Managers and Workers 148

6.6 Toward Model Decomposition 148

6.7 Related Work and Conclusions 149 6.7.1 Related Work 149 6.7.2 Conclusions 151

References 152

Development of resilient cyber-physical systems (CPS), that is, the systemsthat can deliver trustworthy services despite changes, is a complex engineering task. Resilience can be considered as either a system’s ability to achieve its goals despite negative changes, such as failures of components, or as a system’s capability to achieve its desired goals more eciently, for instance by increasing component utilization. In this work, we present a formal goal-oriented approach to developing resilient CPS in Event-B. We dene the main abstractions required for reasoning about system goals and introduce the speci- cation patterns explicitly dening architectural reconguration mechanisms allowing the system to achieve resilience. We demonstrate how formal goal-oriented development in Event-B facilitates the structuring of component interdependencies and derivation of the overall distributed architecture of CPS.