Formal Methods Applied to Industrial Complex Systems

A presentation of real examples of industrial uses for formal methods such as SCADE, the B-Method, ControlBuild, Matelo, etc. in various fields, such as railways, aeronautics, and the automotive industry, the purpose of this book is to present a summary of experience on the use of these “formal methods” (such as proof and model-checking) in industrial examples of complex systems. It is based on the experience of people who are currently involved in the creation and evaluation of safety critical system software. The involvement of people from within the industry allows us to avoid the usual problems of confidentiality which could arise and thus enables us to supply new useful information (photos, architecture plans, real examples, etc.).

Table of Contents:
INTRODUCTION xiii CHAPTER 1. FORMAL DESCRIPTION AND MODELING OF RISKS 1 Jean-Louis BOULANGER 1.1. Introduction1 1.2. Standard process 2 1.2.1. Risks, undesirable events and accidents 2 1.2.2. Usual process 7 1.2.3. Formal software processes for safety-critical systems 8 1.2.4. Formal methods for safety-critical systems 9 1.2.5. Safety kernel 9 1.3. Methodology 10 1.3.1. Presentation 10 1.3.2. Risk mastery process 10 1.4. Case study 13 1.4.1. Rail transport system. 13 1.4.2. Presentation 13 1.4.3. Description of the environment 14 1.4.4. Definition of side-on collision 16 1.4.5. Risk analysis17 1.5. Implementation 18 1.5.1. The B method 18 1.5.2. Implementation 19 1.5.3. Specification of the rail transport system and side-on collision 19 1.6. Conclusion 22 1.7. Glossary 23 1.8. Bibliography 23 CHAPTER 2. AN INNOVATIVE APPROACH AND AN ADVENTURE IN RAIL SAFETY 27 Sylvain FIORONI 2.1. Introduction 27 2.2. Open Control of Train Interchangeable and Integrated System 30 2.3. Computerized interlocking systems 32 2.4. Conclusion 34 2.5. Glossary 35 2.6. Bibliography 36 CHAPTER 3. USE OF FORMAL PROOF FOR CBTC (OCTYS) 37 Christophe TREMBLIN, Pierre LESOILLE and Omar REZZOUG 3.1. Introduction . 37 3.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC 38 3.2.1. Open Control of Train Interchangeable and Integrated System 38 3.2.2. Purpose of CBTC 39 3.2.3. CBTC architectures 40 3.3. Zone control equipment 42 3.3.1. Presentation 42 3.3.2. SCADE model 43 3.4. Implementation of the solution 46 3.5. Technical solution and implementation 49 3.5.1. Property definition 49 3.5.2. Two basic principles of property definition 50 3.5.3. Test topologies 52 3.5.4. Initial analyses 53 3.5.5. The property treatment process 57 3.5.6. Non-regression 63 3.6. Results 65 3.7. Possible improvements 66 3.8. Conclusion 67 3.9. Glossary 68 3.10. Bibliography 69 CHAPTER 4. SAFETY DEMONSTRATION FOR A RAIL SIGNALING APPLICATION IN NOMINAL AND DEGRADED MODES USING FORMAL PROOF 71 Jean-Marc MOTA, Evguenia DMITRIEVA, Amel MAMMAR, Paul CASPI, Salimeh BEHNIA, Nicolas BRETON and Pascal RAYMOND 4.1. Introduction 71 4.1.1. Context 73 4.2. Case description 74 4.2.1. Operational architecture of the PMI system 75 4.2.2. CIM subsystem 76 4.2.3. CIM program verification with and without proof 78 4.2.4. Scope of verification 80 4.3. Modeling the whole system 82 4.3.1. Application model 82 4.3.2. Safety properties 83 4.3.3. Environment model 86 4.4. Formal proof suite 97 4.4.1. Modeling the system 97 4.4.2. Non-certified analysis chain 98 4.4.3. The certified analysis chain 99 4.4.4. Assessment of the proof suite 100 4.5. Application 101 4.6. Results of our experience 105 4.6.1. Environment modeling 105 4.6.2. Proof vs. testing 107 4.6.3. Limitations 108 4.7. Conclusion and prospects 108 4.8. Glossary 110 4.9. Bibliography 111 CHAPTER 5. FORMAL VERIFICATION OF DATA FOR PARAMETERIZED SYSTEMS 115 Mathieu CLABAUT 5.1. Introduction 115 5.1.1. Systerel 115 5.1.2. Data verification 116 5.1.3. Parameterized systems 117 5.2. Data in the development cycle 118 5.2.1. Data and property identification 119 5.2.2. Modeling 119 5.2.3. Property validation 120 5.2.4. Data production 120 5.2.5. Property verification using data 120 5.2.6. Data integration 120 5.3. Data verification 122 5.3.1. Manual verification 122 5.3.2. Algorithmic verification 122 5.3.3. Formal verification 123 5.4. Example of implementation 130 5.4.1. Presentation 130 5.4.2. Property modeling 131 5.4.3. Data extraction 132 5.4.4. Tools 133 5.5. SSIL4 process 133 5.6. Conclusion 134 5.7. Glossary 134 5.8. Bibliography 134 CHAPTER 6. ERTMS MODELING USING EFS 137 Laurent FERIER, Svitlana LUKICHEVA and Stanislas PINTE 6.1. The context 137 6.2. EFS description 139 6.2.1. Characteristics 139 6.2.2. Modeling process 147 6.2.3. Interpretation or code generation 148 6.3. Braking curves modeling 149 6.3.1. Computing braking curves 149 6.3.2. Permitted speed and speed limitation curves 151 6.3.3. Deceleration factors 155 6.3.4. Deceleration curves 156 6.3.5. Target supervision limits 159 6.3.6. Symbolic computation 159 6.3.7. Braking curves verification 160 6.4. Conclusion 161 6.5. Further works 162 6.6. Bibliography 163 CHAPTER 7. THE USE OF A “MODEL-BASED DESIGN” APPROACH ON AN ERTMS LEVEL 2 GROUND SYSTEM 165 Stéphane CALLET, Saïd EL FASSI, Hervé FEDELER, Damien LEDOUX and Thierry NAVARRO 7.1. Introduction 166 7.2. Modeling an ERTMS Level 2 RBC 168 7.2.1. Overall architecture of the model 170 7.2.2. Functional separation 171 7.3. Generation of the configuration 175 7.3.1. Development of a track plan 175 7.3.2. Writing the configuration 176 7.3.3. Translation of the configurations to the MATLAB/Simulink format 177 7.4. Validating the model 177 7.4.1. Development of a language in which to write the scenarios 178 7.4.2. Writing the scenarios 178 7.4.3. Verification of the scenarios 179 7.4.4. Animation of the model 180 7.4.5. Addition of coherence properties for the scenarios 183 7.4.6. Coverage of the model 183 7.5. Proof of the model 184 7.5.1. Expressing the properties 184 7.5.2. Proof of the properties 186 7.6. Report generation 186 7.6.1. Documentation of the model 187 7.6.2. Automatic generation of the report 188 7.7. Principal modeling choices 189 7.8. Conclusion 190 CHAPTER 8. APPLYING ABSTRACT INTERPRETATION TO DEMONSTRATE FUNCTIONAL SAFETY 191 Daniel KÄSTNER 8.1. Introduction 191 8.2. Abstract interpretation 193 8.3. Non-functional correctness 194 8.3.1. Stack usage 194 8.3.2. Worst-case execution time 195 8.3.3. Run-time errors 196 8.4. Why testing is not enough 197 8.5. Verifying non-functional program properties by abstract Interpretation 199 8.5.1. WCET and stack usage analysis 200 8.5.2. Run-time error analysis 206 8.6. The safety standards perspective 210 8.6.1. DO-178B 210 8.6.2. DO-178C / DO-333 211 8.6.3. ISO-26262 214 8.6.4. IEC-61508 216 8.6.5. CENELEC EN-50128 217 8.6.6. Regulations for medical software 218 8.7. Providing confidence – tool qualification and more 219 8.7.1. Tool qualification 220 8.8. Integration in the development process 222 8.9. Practical experience 223 8.10. Summary 224 8.11. Appendix A: Non-functional verification objectives of DO-178C 225 8.12. Appendix B: Non-functional requirements of ISO-26262 225 8.13. Bibliography 229 CHAPTER 9. BCARE: AUTOMATIC RULE CHECKING FOR USE WITH SIEMENS 235 Karim BERKANI, Melanie JACQUEL and Eric LE LAY 9.1. Overview 235 9.2. Introduction 235 9.3. Description of the validation process for added rules 238 9.3.1. The proof activity 238 9.3.2. Rules 238 9.3.3. Rule validation 241 9.4. The BCARe validation tool 243 9.4.1. BCARe: an environment for rule validation 243 9.4.2. Check_blvar 244 9.4.3. Chaine_verif 253 9.5. Proof of the BCARe validation lemmas 260 9.5.1. Automatic proof using Ltac 261 9.5.2. Evaluation and tests 269 9.6. Conclusion 271 9.7. Acknowledgments 272 9.8. Bibliography 272 CHAPTER 10. VALIDATION OF RAILWAY SECURITY AUTOMATISMS BASED ON PETRI NETWORKS 275 Marc ANTONI 10.1. Introduction 275 10.1.1. Note to the reader 275 10.1.2. Summary 275 10.2. Issues involved 277 10.2.1. Introduction 277 10.2.2. An industry context: railways 278 10.2.3. Determinism versus probabilism for the safe management of critical computerized systems 279 10.2.4. A key element: formal validation 300 10.3. Railway safety: basic concepts 301 10.3.1. Control of safety properties and postulates 302 10.3.2. Aspects that should be considered for carrying out a formal validation 308 10.4. Formal validation method for critical computerized systems 313 10.4.1. The interlocking module for modern signal boxes 313 10.4.2. AEFD specification language 316 10.4.3. Method for proof by assertions 325 10.5. Application to a real signal box 337 10.5.1. Introduction 337 10.5.2. Presentation of the track plan and the signal box program 337 10.5.3. Safety properties and postulates 338 10.5.4. Exploration and formal validation of the application functional software of the signal box 339 10.6. Conclusion 340 10.6.1. From a general point of view 340 10.6.2. The use of the method 342 10.6.3. From a research point of view 344 10.6.4. From the railway industry perspective 344 10.6.5. The model and its implementation 346 10.7. Glossary 347 10.8. Bibliography 348 CHAPTER 11. COMBINATION OF FORMAL METHODS FOR CREATING A CRITICAL APPLICATION 353 Philippe COUPOUX 11.1. Introduction 353 11.1.1. A history of the use of formal method in AREVA TA 354 11.2. Use of SCADE 6 355 11.2.1. Reasons for the choice of SCADE 6 355 11.2.2. SCADE 6 in the context of the lifecycle of a software package 356 11.2.3. Organization and development rules of a SCADE 6 model 361 11.2.4. Usage summary SCADE 6 363 11.3. Implementation of the B method 367 11.3.1. The reasons for choosing the B method for the ZC application 367 11.3.2. Positioning the B method in the V cycle of the ZC software 368 11.3.3. B Method Usage Summary 372 11.4. Conclusion 375 11.5. Appendices 376 11.5.1. Appendix 1: SOFTWARE architecture on DRACK platform 376 11.5.2. Appendix 2: detailed description of the approach chosen for the B method 379 11.5.3. General design of the ZC security application 380 11.5.4. Detailed design ZC security application 383 11.5.5. Proof of the formal model 384 11.5.6. Coding of the ZC security application 386 11.5.7. Integration of the ZC security application 387 11.5.8. Tests of the ZC security application 388 11.6 Glossary 388 11.7. Bibliography 389 CHAPTER 12. MATHEMATICAL PROOFS FOR THE NEW YORK SUBWAY 391 Denis SABATIER 12.1. The CBTC of the New York subway Line 7 and the system proof 391 12.2. Formal proof of the system 392 12.2.1. Presentation 392 12.2.2. Benefits 393 12.2.3. Obtaining the first demonstration: organization and communication 397 12.2.4. A method based on exchange 398 12.3. An early insight into the obtained proof 400 12.3.1. The global proof 400 12.3.2. Proof that localization has been correctly achieved 403 12.3.3. Proof of correct braking 404 12.4. Feedback based on experience 406 CONCLUSION 409 GLOSSARY 449 LIST OF AUTHORS 455 INDEX 457

About the Author :
Jean-Louis Boulanger is currently an Independent Safety Assessor (ISA) in the railway domain focusing on software elements. He is a specialist in software engineering (requirement engineering, semi-formal and formal method, proof and model-checking). He also works as an expert for the French notified body CERTIFER in the field of certification of safety critical railway applications based on software (ERTMS, SCADA, automatic subway, etc.). His research interests include requirements, software verification and validation, traceability and RAMS with a special focus on SAFETY.