Formal Methods Applied to Industrial Complex Systems

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.

• INTRODUCTION xiiiCHAPTER 1. FORMAL DESCRIPTION AND MODELING OF RISKS 1Jean-Louis BOULANGER1.1. Introduction11.2. Standard process 21.2.1. Risks, undesirable events and accidents 21.2.2. Usual process 71.2.3. Formal software processes for safety-critical systems 81.2.4. Formal methods for safety-critical systems 91.2.5. Safety kernel 91.3. Methodology 101.3.1. Presentation 101.3.2. Risk mastery process 101.4. Case study 131.4.1. Rail transport system. 131.4.2. Presentation 131.4.3. Description of the environment 141.4.4. Definition of side-on collision 161.4.5. Risk analysis171.5. Implementation 181.5.1. The B method 181.5.2. Implementation 191.5.3. Specification of the rail transport system and side-on collision 191.6. Conclusion 221.7. Glossary 231.8. Bibliography 23CHAPTER 2. AN INNOVATIVE APPROACH AND AN ADVENTURE IN RAIL SAFETY 27Sylvain FIORONI2.1. Introduction 272.2. Open Control of Train Interchangeable and Integrated System 302.3. Computerized interlocking systems 322.4. Conclusion 342.5. Glossary 352.6. Bibliography 36CHAPTER 3. USE OF FORMAL PROOF FOR CBTC (OCTYS) 37Christophe TREMBLIN, Pierre LESOILLE and Omar REZZOUG3.1. Introduction . 373.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC 383.2.1. Open Control of Train Interchangeable and Integrated System 383.2.2. Purpose of CBTC 393.2.3. CBTC architectures 403.3. Zone control equipment 423.3.1. Presentation 423.3.2. SCADE model 433.4. Implementation of the solution 463.5. Technical solution and implementation 493.5.1. Property definition 493.5.2. Two basic principles of property definition 503.5.3. Test topologies 523.5.4. Initial analyses 533.5.5. The property treatment process 573.5.6. Non-regression 633.6. Results 653.7. Possible improvements 663.8. Conclusion 673.9. Glossary 683.10. Bibliography 69CHAPTER 4. SAFETY DEMONSTRATION FOR A RAIL SIGNALING APPLICATION IN NOMINAL AND DEGRADED MODES USING FORMAL PROOF 71Jean-Marc MOTA, Evguenia DMITRIEVA, Amel MAMMAR, Paul CASPI, Salimeh BEHNIA, Nicolas BRETON and Pascal RAYMOND4.1. Introduction 714.1.1. Context 734.2. Case description 744.2.1. Operational architecture of the PMI system 754.2.2. CIM subsystem 764.2.3. CIM program verification with and without proof 784.2.4. Scope of verification 804.3. Modeling the whole system 824.3.1. Application model 824.3.2. Safety properties 834.3.3. Environment model 864.4. Formal proof suite 974.4.1. Modeling the system 974.4.2. Non-certified analysis chain 984.4.3. The certified analysis chain 994.4.4. Assessment of the proof suite 1004.5. Application 1014.6. Results of our experience 1054.6.1. Environment modeling 1054.6.2. Proof vs. testing 1074.6.3. Limitations 1084.7. Conclusion and prospects 1084.8. Glossary 1104.9. Bibliography 111CHAPTER 5. FORMAL VERIFICATION OF DATA FOR PARAMETERIZED SYSTEMS 115Mathieu CLABAUT5.1. Introduction 1155.1.1. Systerel 1155.1.2. Data verification 1165.1.3. Parameterized systems 1175.2. Data in the development cycle 1185.2.1. Data and property identification 1195.2.2. Modeling 1195.2.3. Property validation 1205.2.4. Data production 1205.2.5. Property verification using data 1205.2.6. Data integration 1205.3. Data verification 1225.3.1. Manual verification 1225.3.2. Algorithmic verification 1225.3.3. Formal verification 1235.4. Example of implementation 1305.4.1. Presentation 1305.4.2. Property modeling 1315.4.3. Data extraction 1325.4.4. Tools 1335.5. SSIL4 process 1335.6. Conclusion 1345.7. Glossary 1345.8. Bibliography 134CHAPTER 6. ERTMS MODELING USING EFS 137Laurent FERIER, Svitlana LUKICHEVA and Stanislas PINTE6.1. The context 1376.2. EFS description 1396.2.1. Characteristics 1396.2.2. Modeling process 1476.2.3. Interpretation or code generation 1486.3. Braking curves modeling 1496.3.1. Computing braking curves 1496.3.2. Permitted speed and speed limitation curves 1516.3.3. Deceleration factors 1556.3.4. Deceleration curves 1566.3.5. Target supervision limits 1596.3.6. Symbolic computation 1596.3.7. Braking curves verification 1606.4. Conclusion 1616.5. Further works 1626.6. Bibliography 163CHAPTER 7. THE USE OF A “MODEL-BASED DESIGN” APPROACH ON AN ERTMS LEVEL 2 GROUND SYSTEM 165Stéphane CALLET, Saïd EL FASSI, Hervé FEDELER, Damien LEDOUX and Thierry NAVARRO7.1. Introduction 1667.2. Modeling an ERTMS Level 2 RBC 1687.2.1. Overall architecture of the model 1707.2.2. Functional separation 1717.3. Generation of the configuration 1757.3.1. Development of a track plan 1757.3.2. Writing the configuration 1767.3.3. Translation of the configurations to the MATLAB/Simulink format 1777.4. Validating the model 1777.4.1. Development of a language in which to write the scenarios 1787.4.2. Writing the scenarios 1787.4.3. Verification of the scenarios 1797.4.4. Animation of the model 1807.4.5. Addition of coherence properties for the scenarios 1837.4.6. Coverage of the model 1837.5. Proof of the model 1847.5.1. Expressing the properties 1847.5.2. Proof of the properties 1867.6. Report generation 1867.6.1. Documentation of the model 1877.6.2. Automatic generation of the report 1887.7. Principal modeling choices 1897.8. Conclusion 190CHAPTER 8. APPLYING ABSTRACT INTERPRETATION TO DEMONSTRATE FUNCTIONAL SAFETY 191Daniel KÄSTNER8.1. Introduction 1918.2. Abstract interpretation 1938.3. Non-functional correctness 1948.3.1. Stack usage 1948.3.2. Worst-case execution time 1958.3.3. Run-time errors 1968.4. Why testing is not enough 1978.5. Verifying non-functional program properties by abstract Interpretation 1998.5.1. WCET and stack usage analysis 2008.5.2. Run-time error analysis 2068.6. The safety standards perspective 2108.6.1. DO-178B 2108.6.2. DO-178C / DO-333 2118.6.3. ISO-26262 2148.6.4. IEC-61508 2168.6.5. CENELEC EN-50128 2178.6.6. Regulations for medical software 2188.7. Providing confidence – tool qualification and more 2198.7.1. Tool qualification 2208.8. Integration in the development process 2228.9. Practical experience 2238.10. Summary 2248.11. Appendix A: Non-functional verification objectives of DO-178C 2258.12. Appendix B: Non-functional requirements of ISO-26262 2258.13. Bibliography 229CHAPTER 9. BCARE: AUTOMATIC RULE CHECKING FOR USE WITH SIEMENS 235Karim BERKANI, Melanie JACQUEL and Eric LE LAY9.1. Overview 2359.2. Introduction 2359.3. Description of the validation process for added rules 2389.3.1. The proof activity 2389.3.2. Rules 2389.3.3. Rule validation 2419.4. The BCARe validation tool 2439.4.1. BCARe: an environment for rule validation 2439.4.2. Check_blvar 2449.4.3. Chaine_verif 2539.5. Proof of the BCARe validation lemmas 2609.5.1. Automatic proof using Ltac 2619.5.2. Evaluation and tests 2699.6. Conclusion 2719.7. Acknowledgments 2729.8. Bibliography 272CHAPTER 10. VALIDATION OF RAILWAY SECURITY AUTOMATISMS BASED ON PETRI NETWORKS 275Marc ANTONI10.1. Introduction 27510.1.1. Note to the reader 27510.1.2. Summary 27510.2. Issues involved 27710.2.1. Introduction 27710.2.2. An industry context: railways 27810.2.3. Determinism versus probabilism for the safe management of critical computerized systems 27910.2.4. A key element: formal validation 30010.3. Railway safety: basic concepts 30110.3.1. Control of safety properties and postulates 30210.3.2. Aspects that should be considered for carrying out a formal validation 30810.4. Formal validation method for critical computerized systems 31310.4.1. The interlocking module for modern signal boxes 31310.4.2. AEFD specification language 31610.4.3. Method for proof by assertions 32510.5. Application to a real signal box 33710.5.1. Introduction 33710.5.2. Presentation of the track plan and the signal box program 33710.5.3. Safety properties and postulates 33810.5.4. Exploration and formal validation of the application functional software of the signal box 33910.6. Conclusion 34010.6.1. From a general point of view 34010.6.2. The use of the method 34210.6.3. From a research point of view 34410.6.4. From the railway industry perspective 34410.6.5. The model and its implementation 34610.7. Glossary 34710.8. Bibliography 348CHAPTER 11. COMBINATION OF FORMAL METHODS FOR CREATING A CRITICAL APPLICATION 353Philippe COUPOUX11.1. Introduction 35311.1.1. A history of the use of formal method in AREVA TA 35411.2. Use of SCADE 6 35511.2.1. Reasons for the choice of SCADE 6 35511.2.2. SCADE 6 in the context of the lifecycle of a software package 35611.2.3. Organization and development rules of a SCADE 6 model 36111.2.4. Usage summary SCADE 6 36311.3. Implementation of the B method 36711.3.1. The reasons for choosing the B method for the ZC application 36711.3.2. Positioning the B method in the V cycle of the ZC software 36811.3.3. B Method Usage Summary 37211.4. Conclusion 37511.5. Appendices 37611.5.1. Appendix 1: SOFTWARE architecture on DRACK platform 37611.5.2. Appendix 2: detailed description of the approach chosen for the B method 37911.5.3. General design of the ZC security application 38011.5.4. Detailed design ZC security application 38311.5.5. Proof of the formal model 38411.5.6. Coding of the ZC security application 38611.5.7. Integration of the ZC security application 38711.5.8. Tests of the ZC security application 38811.6 Glossary 38811.7. Bibliography 389CHAPTER 12. MATHEMATICAL PROOFS FOR THE NEW YORK SUBWAY 391Denis SABATIER12.1. The CBTC of the New York subway Line 7 and the system proof 39112.2. Formal proof of the system 39212.2.1. Presentation 39212.2.2. Benefits 39312.2.3. Obtaining the first demonstration: organization and communication 39712.2.4. A method based on exchange 39812.3. An early insight into the obtained proof 40012.3.1. The global proof 40012.3.2. Proof that localization has been correctly achieved 40312.3.3. Proof of correct braking 40412.4. Feedback based on experience 406CONCLUSION 409GLOSSARY 449LIST OF AUTHORS 455INDEX 457