ABSTRACT
CONTENTS 4.1 Introduction 76 4.2 State of the Art 77 4.3 Event-B: A Correct-by-Construction Method 77 4.4 Studied Systems 78
4.4.1 Specication of Studied Systems 79 4.4.2 Renement of Studied Systems 79
4.5 System Substitution 81 4.5.1 A Stepwise Methodology 81 4.5.2 An Event-B Model for System Substitution 82
4.5.2.1 Step 1. Dene a System Specication 82 4.5.2.2 Step 2. Characterize Candidate Substitute Systems 82 4.5.2.3 Step 3. Introduce System Modes 83 4.5.2.4 Step 4. Dene System Substitution as a Composition
Operator 85 4.5.3 Substitution as a Composition Operator 86 4.5.4 The Obtained Composed System with Substitution 86
4.6 Proof Obligations for the System Substitution Operator 87 4.6.1 Invariant Preservation Proof Obligation 88 4.6.2 Variant Denition Proof Obligation 88 4.6.3 About Restored States 89
4.7 A Case Study 89 4.7.1 Step 1. Specication 90 4.7.2 Step 2. Candidate Systems 91
4.7.2.1 The First Substitute System 92 4.7.2.2 The Second Substitute System: Two Suppliers 92
4.7.3 Step 3. Introducing System Modes 94 4.7.4 Step 4. Dene System Substitution 94
4.7.4.1 The Fail Event 94 4.7.4.2 The Repair Event 95
4.8 Substitution Characteristics 96 4.8.1 Cold and Warm Start 96 4.8.2 Identical, Included, or Disjoint Sets of State Variables 96 4.8.3 Equivalence, Upgrade, and Degradation 96 4.8.4 Static or Dynamic Set of Substitutes 97
4.9 Conclusion 97 Appendix 98 References 101
4.1 INTRODUCTION One of the key properties studied in Cyber-Physical Systems (CPS) [1] is the capability of a system to react to changes (e.g., failures, quality of service change, context evolution, maintenance, resilience, etc.). The development of such systems needs to handle explicitly, and at design time, the reactions to changes occurring at runtime. One of the solutions consists in dening another system that substitutes the original one. This substitute system may be a new system or an improvement of the original one.
