ABSTRACT
CONTENTS 7.1 Introduction 156 7.2 Cyber-Physical Systems 157 7.3 Background: Event-B 158 7.4 Formal Development of a Resilient CPS in Event-B 160
7.4.1 The Initial Model 160 7.4.2 The First Renement 163 7.4.3 The Second Renement 165 7.4.4 The Third Renement 167 7.4.5 The Fourth Renement 169
7.5 Example: Satellite Data Processing Unit 170 7.5.1 Description 170 7.5.2 Instantiation of Generic Models 171
7.6 Conclusions 172 References 174
Cyber-physical systems (CPS) are complex software intensive systems consisting ofassemblies of heterogenous components. To guarantee the resilience of CPS, that is, to ensure that systems can adapt to changing operating conditions, CPS architectures should integrate mechanisms enabling adaptation. In this chapter, we employ Event-B to formally derive the reconguration mechanisms that allow the systems to dynamically interconnect components to cope with failures. The proposed approach formalizes relationships among system functionality, component functional capabilities, and failures. It serves as a basis for developing a system health monitoring infrastructure and facilitates rigorous construction of resilient systems.
