Cover -- Title Page -- Copyright -- Contents -- Introduction -- Chapter 1. Formal Description and Modeling of Risks -- 1.1. Introduction -- 1.2. Standard process -- 1.2.1. Risks, undesirable events and accidents -- 1.2.2. Usual process -- 1.2.3. Formal software processes for safety-critical systems -- 1.2.4. Formal methods for safety-critical systems -- 1.2.5. Safety kernel -- 1.3. Methodology -- 1.3.1. Presentation -- 1.3.2. Risk mastery process -- 1.4. Case study -- 1.4.1. Rail transport system -- 1.4.2. Presentation -- 1.4.3. Description of the environment -- 1.4.4. Definition of side-on collision -- 1.4.5. Risk analysis -- 1.5. Implementation -- 1.5.1. The B method -- 1.5.2. Implementation -- 1.5.3. Specification of the rail transport system and side-on collision -- 1.6. Conclusion -- 1.7. Glossary -- 1.8. Bibliography -- Chapter 2. An Innovative Approach and an Adventure in Rail Safety -- 2.1. Introduction -- 2.2. Open Control of Train Interchangeable and Integrated System -- 2.3. Computerized interlocking systems -- 2.4. Conclusion -- 2.5. Glossary -- 2.6. Bibliography -- Chapter 3. Use of Formal Proof for Cbtc (Octys) -- 3.1. Introduction -- 3.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC -- 3.2.1. Open Control of Train Interchangeable and Integrated System -- 3.2.2. Purpose of CBTC -- 3.2.3. CBTC architectures -- 3.3. Zone control equipment -- 3.3.1. Presentation -- 3.3.2. SCADE model -- 3.4. Implementation of the solution -- 3.5. Technical solution and implementation -- 3.5.1. Property definition -- 3.5.2. Two basic principles of property definition -- 3.5.3. Test topologies -- 3.5.4. Initial analyses -- 3.5.5. The property treatment process -- 3.5.6. Non-regression -- 3.6. Results -- 3.7. Possible improvements -- 3.8. Conclusion -- 3.9. Glossary -- 3.10. Bibliography.

Chapter 4. Safety Demonstration for A Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof -- 4.1. Introduction -- 4.1.1. Context -- 4.2. Case description -- 4.2.1. Operational architecture of the PMI system -- 4.2.2. CIM subsystem -- 4.2.3. CIM program verification with and without proof -- 4.2.4. Scope of verification -- 4.3. Modeling the whole system -- 4.3.1. Application model -- 4.3.2. Safety properties -- 4.3.3. Environment model -- 4.4. Formal proof suite -- 4.4.1. Modeling the system -- 4.4.2. Non-certified analysis chain -- 4.4.3. The certified analysis chain -- 4.4.4. Assessment of the proof suite -- 4.5. Application -- 4.6. Results of our experience -- 4.6.1. Environment modeling -- 4.6.2. Proof vs. testing -- 4.6.3. Limitations -- 4.7. Conclusion and prospects -- 4.8. Glossary -- 4.9. Bibliography -- Chapter 5. Formal Verification of Data for Parameterized Systems -- 5.1. Introduction -- 5.1.1. Systerel -- 5.1.2. Data verification -- 5.1.3. Parameterized systems -- 5.2. Data in the development cycle -- 5.2.1. Data and property identification -- 5.2.2. Modeling -- 5.2.3. Property validation -- 5.2.4. Data production -- 5.2.5. Property verification using data -- 5.2.6. Data integration -- 5.3. Data verification -- 5.3.1. Manual verification -- 5.3.2. Algorithmic verification -- 5.3.3. Formal verification -- 5.4. Example of implementation -- 5.4.1. Presentation -- 5.4.2. Property modeling -- 5.4.3. Data extraction -- 5.4.4. Tools -- 5.5. SSIL4 process -- 5.6. Conclusion -- 5.7. Glossary -- 5.8. Bibliography -- Chapter 6. Ertms Modeling Using Efs -- 6.1. The context -- 6.2. EFS description -- 6.2.1. Characteristics -- 6.2.2. Modeling process -- 6.2.3. Interpretation or code generation -- 6.3. Braking curves modeling -- 6.3.1. Computing braking curves.

6.3.2. Permitted speed and speed limitation curves -- 6.3.3. Deceleration factors -- 6.3.4. Deceleration curves -- 6.3.5. Target supervision limits -- 6.3.6. Symbolic computation -- 6.3.7. Braking curves verification -- 6.4. Conclusion -- 6.5. Further works -- 6.6. Bibliography -- Chapter 7. The Use of A "Model-Based Design" Approach on an Ertms Level 2 Ground System -- 7.1. Introduction -- 7.2. Modeling an ERTMS Level 2 RBC -- 7.2.1. Overall architecture of the model -- 7.2.2. Functional separation -- 7.3. Generation of the configuration -- 7.3.1. Development of a track plan -- 7.3.2. Writing the configuration -- 7.3.3. Translation of the configurations to the MATLAB/Simulink format -- 7.4. Validating the model -- 7.4.1. Development of a language in which to write the scenarios -- 7.4.2. Writing the scenarios -- 7.4.3. Verification of the scenarios -- 7.4.4. Animation of the model -- 7.4.5. Addition of coherence properties for the scenarios -- 7.4.6. Coverage of the model -- 7.5. Proof of the model -- 7.5.1. Expressing the properties -- 7.5.2. Proof of the properties -- 7.6. Report generation -- 7.6.1. Documentation of the model -- 7.6.2. Automatic generation of the report -- 7.7. Principal modeling choices -- 7.8. Conclusion -- Chapter 8. Applying Abstract Interpretation To Demonstrate Functional Safety -- 8.1. Introduction -- 8.2. Abstract interpretation -- 8.3. Non-functional correctness -- 8.3.1. Stack usage -- 8.3.2. Worst-case execution time -- 8.3.3. Run-time errors -- 8.4. Why testing is not enough -- 8.5. Verifying non-functional program properties by abstract Interpretation -- 8.5.1. WCET and stack usage analysis -- 8.5.2. Run-time error analysis -- 8.6. The safety standards perspective -- 8.6.1. DO-178B -- 8.6.2. DO-178C / DO-333 -- 8.6.3. ISO-26262 -- 8.6.4. IEC-61508 -- 8.6.5. CENELEC EN-50128.

8.6.6. Regulations for medical software -- 8.7. Providing confidence - tool qualification and more -- 8.7.1. Tool qualification -- 8.8. Integration in the development process -- 8.9. Practical experience -- 8.10. Summary -- 8.11. Appendix A: Non-functional verification objectives of DO-178C -- 8.12. Appendix B: Non-functional requirements of ISO-26262 -- 8.13. Bibliography -- Chapter 9. Bcare: Automatic Rule Checking For Use With Siemens -- 9.1. Overview -- 9.2. Introduction -- 9.3. Description of the validation process for added rules -- 9.3.1. The proof activity -- 9.3.2. Rules -- 9.3.3. Rule validation -- 9.4. The BCARe validation tool -- 9.4.1. BCARe: an environment for rule validation -- 9.4.2. Check_blvar -- 9.4.3. Chaine_verif -- 9.5. Proof of the BCARe validation lemmas -- 9.5.1. Automatic proof using Ltac -- 9.5.2. Evaluation and tests -- 9.6. Conclusion -- 9.7. Acknowledgments -- 9.8. Bibliography -- Chapter 10. Validation of Railway Security Automatisms Based on Petri Networks -- 10.1. Introduction -- 10.1.1. Note to the reader -- 10.1.2. Summary -- 10.2. Issues involved -- 10.2.1. Introduction -- 10.2.2. An industry context: railways -- 10.2.3. Determinism versus probabilism for the safe management of critical computerized systems -- 10.2.4. A key element: formal validation -- 10.3. Railway safety: basic concepts -- 10.3.1. Control of safety properties and postulates -- 10.3.2. Aspects that should be considered for carrying out a formal validation -- 10.4. Formal validation method for critical computerized systems -- 10.4.1. The interlocking module for modern signal boxes -- 10.4.2. AEFD specification language -- 10.4.3. Method for proof by assertions -- 10.5. Application to a real signal box -- 10.5.1. Introduction.

10.5.2. Presentation of the track plan and the signal box program -- 10.5.3. Safety properties and postulates -- 10.5.4. Exploration and formal validation of the application functional software of the signal box -- 10.6. Conclusion -- 10.6.1. From a general point of view -- 10.6.2. The use of the method -- 10.6.3. From a research point of view -- 10.6.4. From the railway industry perspective -- 10.6.5. The model and its implementation -- 10.7. Glossary -- 10.8. Bibliography -- Chapter 11. Combination of Formal Methods for Creating A Critical Application -- 11.1. Introduction -- 11.1.1. A history of the use of formal method in AREVA TA -- 11.2. Use of SCADE 6 -- 11.2.1. Reasons for the choice of SCADE 6 -- 11.2.2. SCADE 6 in the context of the lifecycle of a software package -- 11.2.3. Organization and development rules of a SCADE 6 model -- 11.2.4. Usage summary SCADE 6 -- 11.3. Implementation of the B method -- 11.3.1. The reasons for choosing the B method for the ZC application -- 11.3.2. Positioning the B method in the V cycle of the ZC software -- 11.3.3. B Method Usage Summary -- 11.4. Conclusion -- 11.5. Appendices -- 11.5.1. Appendix 1: SOFTWARE architecture on DRACK platform -- 11.5.2. Appendix 2: detailed description of the approach chosen for the B method -- 11.5.3. General design of the ZC security application -- 11.5.4. Detailed design ZC security application -- 11.5.5. Proof of the formal model -- 11.5.6. Coding of the ZC security application -- 11.5.7. Integration of the ZC security application -- 11.5.8. Tests of the ZC security application -- 11.6 Glossary -- 11.7. Bibliography -- Chapter 12. Mathematical Proofs for The New York Subway -- 12.1. The CBTC of the New York subway Line 7 and the system proof -- 12.2. Formal proof of the system -- 12.2.1. Presentation -- 12.2.2. Benefits.

12.2.3. Obtaining the first demonstration: organization and communication.