Although formal analysis programming techniques may be quite old, the introduction of formal methods only dates from the 1980s. These techniques enable us to analyze the behavior of a software application, described in a programming language. It took until the end of the 1990s before formal methods or the B method could be implemented in industrial applications or be usable in an industrial setting. Current literature only gives students and researchers very general overviews of formal methods. The purpose of this book is to present feedback from experience on the use of formal methods (such as proof and model-checking) in industrial examples within the transportation domain. This book 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.). Topics covered by the chapters of this book include SAET-METEOR, the B method and B tools, model-based design using Simulink, the Simulink design verifier proof tool, the implementation and applications of SCADE (Safety Critical Application Development Environment), GATeL: A V&V Platform for SCADE models and ControlBuild. Contents 1. From Classic Languages to Formal Methods, Jean-Louis Boulanger. 2. Formal Method in the Railway Sector the First Complex Application: SAET-METEOR, Jean-Louis Boulanger. 3. The B Method and B Tools, Jean-Louis Boulanger. 4. Model-Based Design Using Simulink Modeling, Code Generation, Verification, and Validation, Mirko Conrad and Pieter J. Mosterman. 5. Proving Global Properties with the Aid of the SIMULINK DESIGN VERIFIER Proof Tool, V ronique Delebarre and Jean-Fr d ric Etienne. 6. SCADE: Implementation and Applications, Jean-Louis Camus. 7. GATeL: A V&V Platform for SCADE Models, Bruno Marre, Benjamin Bianc, Patricia Mouy and Christophe Junke. 8. ControlBuild, a Development Framework for Control Engineering, Franck Corbier. 9. Conclusion, Jean-Louis Boulanger.

Although formal analysis programming techniques may be quiteold, the introduction of formal methods only dates from the 1980s.These techniques enable us to analyze the behavior of a softwareapplication, described in a programming language. It took until theend of the 1990s before formal methods or the B method could beimplemented in industrial applications or be usable in anindustrial setting.Current literature only gives students and researchers very generaloverviews of formal methods. The purpose of this book is to presentfeedback from experience on the use of "formal methods"(such as proof and model-checking) in industrial examples withinthe transportation domain.This book is based on the experience of people who are currentlyinvolved in the creation and evaluation of safety critical systemsoftware. The involvement of people from within the industry allowsus to avoid the usual problems of confidentiality which could ariseand thus enables us to supply new useful information (photosarchitecture plans, real examples, etc.).Topics covered by the chapters of this book include SAET-METEORthe B method and B tools, model-based design using Simulink, theSimulink design verifier proof tool, the implementation andapplications of SCADE (Safety Critical Application DevelopmentEnvironment), GATeL: A V&V Platform for SCADE models andControlBuild.Contents1. From Classic Languages to Formal Methods, Jean-LouisBoulanger.2. Formal Method in the Railway Sector & #8232;the First ComplexApplication: SAET-METEOR, Jean-Louis Boulanger.3. The B Method and B Tools, Jean-Louis Boulanger.4. Model-Based Design Using Simulink - Modeling, CodeGeneration, Verification, and Validation, Mirko Conrad and PieterJ. Mosterman.5. Proving Global Properties with the Aid of the SIMULINK DESIGNVERIFIER Proof Tool, Véronique Delebarre andJean-Frédéric Etienne.6. SCADE: Implementation and Applications, Jean-Louis Camus.7. GATeL: A V&V Platform for SCADE Models, Bruno MarreBenjamin Bianc, Patricia Mouy and Christophe Junke.8. ControlBuild, a Development Framework & #8232;for ControlEngineering, Franck Corbier.9. Conclusion, Jean-Louis Boulanger.

Chapter 1. From Classic Languages to Formal Methods1Jean-Louis BOULANGER1.1. Introduction 11.2. Classic development 21.3. Structured, semi-formal and/or formal methods 331.4. Formal methods 391.5. Conclusion 451.6. Bibliography 49Chapter 2. Formal Method in the Railway Sector the FirstComplex Application: SAET-METEOR 55Jean-Louis BOULANGER2.1. Introduction 552.2. About SAET-METEOR 562.3. The supplier realization process 622.4. Process of verification and validation set up by RATP782.5. Assessment of the global approach 1142.6. Conclusion 1152.7. Appendix 1162.8. Bibliography 122Chapter 3. The B Method and B Tools 127Jean-Louis BOULANGER3.1. Introduction 1273.2. The B method 1283.3. Verification and validation (V&V) 1373.4. B tools 1413.5. Methodology 1463.6. Feedback 1503.7. Conclusion 1553.8. Bibliography 155Chapter 4. Model-Based Design Using Simulink -Modeling, Code Generation, Verification, and Validation159Mirko CONRAD and Pieter J. MOSTERMAN4.1. Introduction 1594.2. Embedded software development using Model-Based Design1624.3. Case study - an electronic throttle control system1644.4. Verification and validation of models and generated code1734.5. Compliance with safety standards 1774.6. Conclusion 1784.7. Bibliography 178Chapter 5. Proving Global Properties with the Aid of theSIMULINK DESIGN VERIFIER Proof Tool 183Véronique DELEBARRE and Jean-FrédéricETIENNE5.1. Introduction 1835.2. Formal proof or verification method 1845.3. Implementation of the SIMULINK DESIGN VERIFIER tool 1935.4. Experience feedback and methodological aspects 2115.5. Study case feedback and conclusions 2185.6. Contributions of the methodology compared with the EN50128normative referential 2205.7. Bibliography 222Chapter 6. SCADE: Implementation and Applications225Jean-Louis CAMUS6.1. Introduction 2256.2. Issues of embedded safety-critical software 2256.3. Origins of SCADE 2286.4. The SCADE data-flow language 2316.5. Conclusion: extensions of languages for controllers anditerative processing 2406.6. The SCADE system 2466.7. Application of SCADE in the aeronautical industry 2566.8 Application of SCADE in the rail industry 2616.9. Application of SCADE in the nuclear and other industries2656.10. Conclusion 2696.11. Bibliography 270Chapter 7. GATeL: A V&V Platform for SCADE Models273Bruno MARRE, Benjamin BIANC, Patricia MOUY and ChristopheJUNKE7.1. Introduction 2737.2. SCADE language 2757.3. GATeL prerequisites 2767.4. Assistance in the design of test selection strategies2797.5. Performances 2837.6. Conclusion 2847.7. Bibliography 285Chapter 8. ControlBuild, a Development Framework for ControlEngineering 287Franck CORBIER8.1. Introduction 2878.2. Development of the control system 2898.3. Formalisms used 3008.4. Safety arrangements 3118.5. Examples of railway use cases 3188.6. Conclusion 3238.7. Bibliography 323Chapter 9. Conclusion 325Jean-Louis BOULANGER9.1. Introduction 3259.2. Problems 3269.3. Summary 3279.4. Implementing formal methods 3329.5. Realization of a software application 3379.6. Conclusion 3399.7. Bibliography 340Glossary 345List of Authors 351Index 353