Formal Methods Applied to Industrial Complex Systems

Herausgegeben von Boulanger, Jean-Louis

• Gebundenes Buch

Produktbeschreibung

A presentation of real examples of industrial uses for formalmethods such as SCADE, the B-Method, ControlBuild, Matelo, etc. invarious fields, such as railways, aeronautics, and the automotiveindustry, the purpose of this book is to present a summary ofexperience on the use of these "formal methods" (suchas proof and model-checking) in industrial examples of complexsystems.
It is based on the experience of people who are currently involvedin the creation and evaluation of safety critical system software.The involvement of people from within the industry allows us toavoid the usual problems of confidentiality which could arise andthus enables us to supply new useful information (photos,architecture plans, real examples, etc.).

Produktdetails

• Verlag: Wiley & Sons
• 1. Auflage
• Seitenzahl: 480
• Erscheinungstermin: 29. September 2014
• Englisch
• Abmessung: 234mm x 157mm x 30mm
• Gewicht: 666g
• ISBN-13: 9781848216327
• ISBN-10: 1848216327
• Artikelnr.: 40046223

Autorenporträt

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.

Inhaltsangabe

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.1.
Introduction 115 5.1.1. Systerel 115 5.1.2. Data verification 116 5.1.3.
Parameterized systems 117 5.2. Data in the development cycle 118 5.2.1.
Data and property identification 119 5.2.2. Modeling 119 5.2.3. Property
validation 120 5.2.4. Data production 120 5.2.5. Property verification
using data 120 5.2.6. Data integration 120 5.3. Data verification 122
5.3.1. Manual verification 122 5.3.2. Algorithmic verification 122 5.3.3.
Formal verification 123 5.4. Example of implementation 130 5.4.1.
Presentation 130 5.4.2. Property modeling 131 5.4.3. Data extraction 132
5.4.4. Tools 133 5.5. SSIL4 process 133 5.6. Conclusion 134 5.7. Glossary
134 5.8. Bibliography 134 CHAPTER 6. ERTMS MODELING USING EFS 137 Laurent
FERIER, Svitlana LUKICHEVA and Stanislas PINTE 6.1. The context 137 6.2.
EFS description 139 6.2.1. Characteristics 139 6.2.2. Modeling process 147
6.2.3. Interpretation or code generation 148 6.3. Braking curves modeling
149 6.3.1. Computing braking curves 149 6.3.2. Permitted speed and speed
limitation curves 151 6.3.3. Deceleration factors 155 6.3.4. Deceleration
curves 156 6.3.5. Target supervision limits 159 6.3.6. Symbolic computation
159 6.3.7. Braking curves verification 160 6.4. Conclusion 161 6.5. Further
works 162 6.6. Bibliography 163 CHAPTER 7. THE USE OF A "MODEL-BASED
DESIGN" APPROACH ON AN ERTMS LEVEL 2 GROUND SYSTEM 165 Stéphane CALLET,
Saïd EL FASSI, Hervé FEDELER, Damien LEDOUX and Thierry NAVARRO 7.1.
Introduction 166 7.2. Modeling an ERTMS Level 2 RBC 168 7.2.1. Overall
architecture of the model 170 7.2.2. Functional separation 171 7.3.
Generation of the configuration 175 7.3.1. Development of a track plan 175
7.3.2. Writing the configuration 176 7.3.3. Translation of the
configurations to the MATLAB/Simulink format 177 7.4. Validating the model
177 7.4.1. Development of a language in which to write the scenarios 178
7.4.2. Writing the scenarios 178 7.4.3. Verification of the scenarios 179
7.4.4. Animation of the model 180 7.4.5. Addition of coherence properties
for the scenarios 183 7.4.6. Coverage of the model 183 7.5. Proof of the
model 184 7.5.1. Expressing the properties 184 7.5.2. Proof of the
properties 186 7.6. Report generation 186 7.6.1. Documentation of the model
187 7.6.2. Automatic generation of the report 188 7.7. Principal modeling
choices 189 7.8. Conclusion 190 CHAPTER 8. APPLYING ABSTRACT INTERPRETATION
TO DEMONSTRATE FUNCTIONAL SAFETY 191 Daniel KÄSTNER 8.1. Introduction 191
8.2. Abstract interpretation 193 8.3. Non-functional correctness 194 8.3.1.
Stack usage 194 8.3.2. Worst-case execution time 195 8.3.3. Run-time errors
196 8.4. Why testing is not enough 197 8.5. Verifying non-functional
program properties by abstract Interpretation 199 8.5.1. WCET and stack
usage analysis 200 8.5.2. Run-time error analysis 206 8.6. The safety
standards perspective 210 8.6.1. DO-178B 210 8.6.2. DO-178C / DO-333 211
8.6.3. ISO-26262 214 8.6.4. IEC-61508 216 8.6.5. CENELEC EN-50128 217
8.6.6. Regulations for medical software 218 8.7. Providing confidence -
tool qualification and more 219 8.7.1. Tool qualification 220 8.8.
Integration in the development process 222 8.9. Practical experience 223
8.10. Summary 224 8.11. Appendix A: Non-functional verification objectives
of DO-178C 225 8.12. Appendix B: Non-functional requirements of ISO-26262
225 8.13. Bibliography 229 CHAPTER 9. BCARE: AUTOMATIC RULE CHECKING FOR
USE WITH SIEMENS 235 Karim BERKANI, Melanie JACQUEL and Eric LE LAY 9.1.
Overview 235 9.2. Introduction 235 9.3. Description of the validation
process for added rules 238 9.3.1. The proof activity 238 9.3.2. Rules 238
9.3.3. Rule validation 241 9.4. The BCARe validation tool 243 9.4.1. BCARe:
an environment for rule validation 243 9.4.2. Check_blvar 244 9.4.3.
Chaine_verif 253 9.5. Proof of the BCARe validation lemmas 260 9.5.1.
Automatic proof using Ltac 261 9.5.2. Evaluation and tests 269 9.6.
Conclusion 271 9.7. Acknowledgments 272 9.8. Bibliography 272 CHAPTER 10.
VALIDATION OF RAILWAY SECURITY AUTOMATISMS BASED ON PETRI NETWORKS 275 Marc
ANTONI 10.1. Introduction 275 10.1.1. Note to the reader 275 10.1.2.
Summary 275 10.2. Issues involved 277 10.2.1. Introduction 277 10.2.2. An
industry context: railways 278 10.2.3. Determinism versus probabilism for
the safe management of critical computerized systems 279 10.2.4. A key
element: formal validation 300 10.3. Railway safety: basic concepts 301
10.3.1. Control of safety properties and postulates 302 10.3.2. Aspects
that should be considered for carrying out a formal validation 308 10.4.
Formal validation method for critical computerized systems 313 10.4.1. The
interlocking module for modern signal boxes 313 10.4.2. AEFD specification
language 316 10.4.3. Method for proof by assertions 325 10.5. Application
to a real signal box 337 10.5.1. Introduction 337 10.5.2. Presentation of
the track plan and the signal box program 337 10.5.3. Safety properties and
postulates 338 10.5.4. Exploration and formal validation of the application
functional software of the signal box 339 10.6. Conclusion 340 10.6.1. From
a general point of view 340 10.6.2. The use of the method 342 10.6.3. From
a research point of view 344 10.6.4. From the railway industry perspective
344 10.6.5. The model and its implementation 346 10.7. Glossary 347 10.8.
Bibliography 348 CHAPTER 11. COMBINATION OF FORMAL METHODS FOR CREATING A
CRITICAL APPLICATION 353 Philippe COUPOUX 11.1. Introduction 353 11.1.1. A
history of the use of formal method in AREVA TA 354 11.2. Use of SCADE 6
355 11.2.1. Reasons for the choice of SCADE 6 355 11.2.2. SCADE 6 in the
context of the lifecycle of a software package 356 11.2.3. Organization and
development rules of a SCADE 6 model 361 11.2.4. Usage summary SCADE 6 363
11.3. Implementation of the B method 367 11.3.1. The reasons for choosing
the B method for the ZC application 367 11.3.2. Positioning the B method in
the V cycle of the ZC software 368 11.3.3. B Method Usage Summary 372 11.4.
Conclusion 375 11.5. Appendices 376 11.5.1. Appendix 1: SOFTWARE
architecture on DRACK platform 376 11.5.2. Appendix 2: detailed description
of the approach chosen for the B method 379 11.5.3. General design of the
ZC security application 380 11.5.4. Detailed design ZC security application
383 11.5.5. Proof of the formal model 384 11.5.6. Coding of the ZC security
application 386 11.5.7. Integration of the ZC security application 387
11.5.8. Tests of the ZC security application 388 11.6 Glossary 388 11.7.
Bibliography 389 CHAPTER 12. MATHEMATICAL PROOFS FOR THE NEW YORK SUBWAY
391 Denis SABATIER 12.1. The CBTC of the New York subway Line 7 and the
system proof 391 12.2. Formal proof of the system 392 12.2.1. Presentation
392 12.2.2. Benefits 393 12.2.3. Obtaining the first demonstration:
organization and communication 397 12.2.4. A method based on exchange 398
12.3. An early insight into the obtained proof 400 12.3.1. The global proof
400 12.3.2. Proof that localization has been correctly achieved 403 12.3.3.
Proof of correct braking 404 12.4. Feedback based on experience 406
CONCLUSION 409 GLOSSARY 449 LIST OF AUTHORS 455 INDEX 457