Cover -- Title Page -- Copyright Page -- Table of Contents -- Introduction -- Chapter 1. From Classic Languages to Formal Methods -- 1.1. Introduction -- 1.2. Classic development -- 1.2.1. Development process -- 1.2.2. Coding -- 1.2.3. Specification and architecture -- 1.2.4. Verification and validation (V&V) -- 1.2.5. Summary -- 1.3. Structured, semi-formal and/or formal methods -- 1.3.1. E/E/PE system -- 1.3.2. Rail sector -- 1.3.3. Taking into account techniques and formal methods -- 1.4. Formal methods -- 1.4.1. Principles -- 1.4.2. Examples of formal methods -- 1.5. Conclusion -- 1.6. Bibliography -- Chapter 2. Formal Method in the Railway Sector the First Complex Application: SAET-METEOR -- 2.1. Introduction -- 2.2. About SAET-METEOR -- 2.2.1. Decomposition of the SAET-METEOR -- 2.2.2. Anticollision functions -- 2.2.3. Restrictions -- 2.3. The supplier realization process -- 2.3.1. Historical context -- 2.3.2. The hardware aspect -- 2.3.3. The software aspect -- 2.3.4. Assessment of the processes -- 2.4. Process of verification and validation set up by RATP -- 2.4.1. Context -- 2.4.2. RATP methodology -- 2.4.3. Verification carried out by RATP -- 2.4.4. Validation -- 2.4.5. Assessment of RATP activity -- 2.5. Assessment of the global approach -- 2.6. Conclusion -- 2.7. Appendix -- 2.7.1. Object of the track -- 2.7.2. Block logic -- 2.8. Bibliography -- Chapter 3. The B Method and B Tools -- 3.1. Introduction -- 3.2. The B method -- 3.2.1. The concept of abstract machines -- 3.2.2. Machines with implementations -- 3.3. Verification and validation (V&V) -- 3.3.1. Internal verification -- 3.4. B tools -- 3.4.1. General principles -- 3.4.2. Code generation -- 3.4.3. Prover -- 3.4.4. Atelier B -- 3.5. Methodology -- 3.5.1. Layered development -- 3.5.2. Link between the project structure and the POs -- 3.5.3. Cycle of development of a B project.

3.6. Feedback -- 3.6.1. Some figures -- 3.6.2. Some users -- 3.7. Conclusion -- 3.8. Bibliography -- Chapter 4. Model-Based Design Using Simulink - Modeling, Code Generation, Verification, and Validation -- 4.1. Introduction -- 4.2. Embedded software development using Model-Based Design -- 4.3. Case study - an electronic throttle control system -- 4.3.1. System overview -- 4.3.2. Simulink® model -- 4.3.3. Automatic code generation -- 4.3.4. Code optimization -- 4.3.5. Fixed-point code -- 4.3.6. Including legacy code -- 4.3.7. Importing interface definitions -- 4.3.8. Importing algorithms -- 4.4. Verification and validation of models and generated code -- 4.4.1. Integrating verification and validation with Model-Based Design -- 4.4.2. Design verification -- 4.4.3. Reviews and static analyses at the model level -- 4.4.4. Module and integration testing at the model level -- 4.4.5. Code verification -- 4.4.6. Back-to-back comparison testing between model and code -- 4.4.7. Measures to prevent unintended functionality -- 4.5. Compliance with safety standards -- 4.6. Conclusion -- 4.7. Bibliography -- Chapter 5. Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool -- 5.1. Introduction -- 5.2. Formal proof or verification method -- 5.2.1. Model verification -- 5.2.2. Formal methods and proof of correction -- 5.2.3. Combining models and proof tools -- 5.3. Implementation of the SIMULINK DESIGN VERIFIER tool -- 5.3.1. Reminders of the MATLAB modeling and verification environment -- 5.3.2. Case study -- 5.3.3. Modeling -- 5.3.4. Modeling -- 5.4. Experience feedback and methodological aspects -- 5.4.1. Modeling rules and convergence control -- 5.4.2. Modular proof phase -- 5.4.3. Proof of global properties -- 5.4.4. Detection of counterexamples -- 5.5. Study case feedback and conclusions -- 5.5.1. SIMULINK model.

5.5.2. Proofs achieved -- 5.5.3. Incremental verification approach -- 5.6. Contributions of the methodology compared with the EN50128 normative referential -- 5.7. Bibliography -- Chapter 6. SCADE: Implementation and Applications -- 6.1. Introduction -- 6.2. Issues of embedded safety-critical software -- 6.2.1. Characteristics of embedded safety-critical software -- 6.2.2. Architecture of an embedded safety-critical application -- 6.2.3. Criticality and normative requirements for embedded safety-critical applications -- 6.2.4. Complexity, cost and delays -- 6.3. Origins of SCADE -- 6.3.1. Introduction -- 6.3.2. Initial industrial approaches -- 6.3.3. "Real-time" extensions of current languages -- 6.3.4. Synchronous formal languages dedicated to "real-time" created in laboratories -- 6.3.5. Birth of SCADE -- 6.4. The SCADE data-flow language -- 6.4.1. Introduction -- 6.4.2. Synchronous language -- 6.4.3. "Data-flow" functional language -- 6.4.4. Scalar data types -- 6.4.5. Structured data types -- 6.4.6. Clocks, temporal operators, and causality -- 6.4.7. Selectors -- 6.4.8. Imperative structures -- 6.4.9. Rigor and functional safety -- 6.5. Conclusion: extensions of languages for controllers and iterative processing -- 6.5.1. Objectives -- 6.5.2. Control flow -- 6.5.3. Iterative processing -- 6.6. The SCADE system -- 6.6.1. Outline of the SCADE workbench -- 6.6.2. Model verification -- 6.6.3. Performance prediction -- 6.6.4. The qualified code generator -- 6.7. Application of SCADE in the aeronautical industry -- 6.7.1. History: Aérospatiale and Thales Avionique -- 6.7.2. Control/command type applications -- 6.7.3. Monitoring/alarm type applications -- 6.7.4. Navigation systems -- 6.8 Application of SCADE in the rail industry -- 6.8.1. First applications -- 6.8.2. Applications developed for the RATP and other French metros.

6.8.3. Generic PAI-NG applications -- 6.8.4. Example of automated door control -- 6.9. Application of SCADE in the nuclear and other industries -- 6.9.1. Applications in the nuclear industry -- 6.9.2. Deployment of SCADE in the civil nuclear industry -- 6.10. Conclusion -- 6.11. Bibliography -- Chapter 7. GATeL: A V&V Platform for SCADE Models -- 7.1. Introduction -- 7.2. SCADE language -- 7.3. GATeL prerequisites -- 7.3.1. GATeL kernel -- 7.3.2. Example -- 7.4. Assistance in the design of test selection strategies -- 7.4.1. Unfolding of SCADE operators -- 7.4.2. Functional scenarios -- 7.5. Performances -- 7.6. Conclusion -- 7.7. Bibliography -- Chapter 8. ControlBuild, a Development Framework for Control Engineering -- 8.1. Introduction -- 8.2. Development of the control system -- 8.2.1. ERTMS -- 8.2.2. Development process equipment -- 8.2.3. A component-based approach -- 8.2.4. Development methodology -- 8.3. Formalisms used -- 8.3.1. Assembly editor -- 8.3.2. IEC1131-3 languages for embedded control -- 8.3.3. Electrical schematics for conventional control -- 8.3.4. Electromechanical and physical environment -- 8.4. Safety arrangements -- 8.4.1. Metrics -- 8.4.2. Assertions -- 8.4.3. Automatic test procedure execution -- 8.4.4. Functional tests -- 8.4.5. Code coverage -- 8.4.6. SSIL2 code generation -- 8.4.7. Management of the project documentation -- 8.4.8. Traceability of requirements -- 8.5. Examples of railway use cases -- 8.5.1. Specification validation -- 8.5.2. TCMS development -- 8.5.3. Progressive integration bench - HiL -- 8.6. Conclusion -- 8.7. Bibliography -- Chapter 9. Conclusion -- 9.1. Introduction -- 9.2. Problems -- 9.3. Summary -- 9.3.1. Model verification -- 9.3.2. Properties and requirements -- 9.3.3. Implementation of formal methods -- 9.4. Implementing formal methods -- 9.4.1. Conventional process.

9.4.2. Process accounting for formal methods -- 9.4.3. Problems -- 9.5. Realization of a software application -- 9.6. Conclusion -- 9.7. Bibliography -- Glossary -- List of Authors -- Index.