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.).

List 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.

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.

Summary

A presentation of real examples of industrial uses for formal methods such as SCADE, the B-Method, ControlBuild, Matelo, etc.

Product details

• Authors: Jean-Louis Boulanger, JL Boulanger
• Assisted by: Jean-Loui Boulanger (Editor), Jean-Louis Boulanger (Editor)
• Publisher: Wiley & Sons
• Languages: English
• Product format: Hardback
• Released: 01.01.2014
• EAN: 9781848216327
• ISBN: 978-1-84821-632-7
• No. of pages: 480
• Dimensions: 150 mm x 250 mm x 15 mm
• Weight: 666 g
• Series: ISTE; ISTE
• Subject: Natural sciences, medicine, IT, technology > Technology > Electronics, electrical engineering, communications engineering