Formal Methods Applied to Industrial Complex Systems E-Book

• Herausgeber: John Wiley & Sons
• Kategorie: Wissenschaft und neue Technologien
• Sprache: Englisch

Seitenzahl: 592

Veröffentlichungsjahr: 2014

Beschreibung

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

Leseprobe

Contents

Introduction

I.1. Context

I.2. Aims of this book

I.3. Bibliography

1 Formal Description and Modeling of Risks

1.1. Introduction

1.2. Standard process

1.3. Methodology

1.4. Case study

1.5. Implementation

1.6. Conclusion

1.7. Glossary

1.8. Bibliography

2 An Innovative Approach and an Adventure in Rail Safety

2.1. Introduction

2.2. Open Control of Train Interchangeable and Integrated System6

2.3. Computerized interlocking systems12

2.4. Conclusion

2.5. Glossary

2.6. Bibliography

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.3. Zone control equipment

3.4. Implementation of the solution

3.5. Technical solution and implementation

3.6. Results

3.7. Possible improvements

3.8. Conclusion

3.9. Glossary

3.10. Bibliography

4 Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof

4.1. Introduction

4.2. Case description

4.3. Modeling the whole system

4.4. Formal proof suite

4.5. Application

4.6. Results of our experience

4.7. Conclusion and prospects

4.8. Glossary

4.9. Bibliography

5 Formal Verification of Data for Parameterized Systems

5.1. Introduction

5.2. Data in the development cycle

5.3. Data verification

5.4. Example of implementation

5.5. SSIL4 process

5.6. Conclusion

5.7. Glossary

5.8. Bibliography

6 ERTMS Modeling Using EFS

6.1. The context

6.2. EFS description

6.3. Braking curves modeling

6.4. Conclusion

6.5. Further works

6.6. Bibliography

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.3. Generation of the configuration

7.4. Validating the model

7.5. Proof of the model

7.6. Report generation

7.7. Principal modeling choices

7.8. Conclusion

8 Applying Abstract Interpretation to Demonstrate Functional Safety

8.1. Introduction

8.2. Abstract interpretation

8.3. Non-functional correctness

8.4. Why testing is not enough

8.5. Verifying non-functional program properties by abstract Interpretation

8.6. The safety standards perspective

8.7. Providing confidence – tool qualification and more

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

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.4. The BCARe validation tool

9.5. Proof of the BCARe validation lemmas

9.6. Conclusion

9.7. Acknowledgments

9.8. Bibliography

10 Validation of Railway Security Automatisms Based on Petri Networks

10.1. Introduction

10.2. Issues involved

10.3. Railway safety: basic concepts

10.4. Formal validation method for critical computerized systems

10.5. Application to a real signal box

10.6. Conclusion

10.7. Glossary

10.8. Bibliography

11 Combination of Formal Methods for Creating a Critical Application

11.1. Introduction

11.2. Use of SCADE 6

11.3. Implementation of the B method

11.4. Conclusion

11.5. Appendices

11.6 Glossary

11.7. Bibliography

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.3. An early insight into the obtained proof

12.4. Feedback based on experience

Conclusion

C.1. Introduction

C.2. Formal methods and the standard CENELEC EN 50128

C.3. Modeling

C.4. Conclusion

C.5. Glossary

C.6. Bibliography

Glossary

List of Authors

Index

Dedicated to Mr Paul Caspi

First published 2014 in Great Britain and the United States by ISTE Ltd and John Wiley & Sons, Inc.

Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms and licenses issued by the CLA. Enquiries concerning reproduction outside these terms should be sent to the publishers at the undermentioned address:

ISTE Ltd27-37 St George’s RoadLondon SW19 4EUUK

www.iste.co.uk

John Wiley & Sons, Inc.111 River StreetHoboken, NJ 07030USA

www.wiley.com

© ISTE Ltd 2014

The rights of Jean-Louis Boulanger to be identified as the author of this work have been asserted by him in accordance with the Copyright, Designs and Patents Act 1988.

Library of Congress Control Number: 2014936487

British Library Cataloguing-in-Publication DataA CIP record for this book is available from the British LibraryISBN 978-1-84821-632-7

Introduction

Introduction written by Jean-LOUIS BOULANGER.

I.1. Context

Although formal program analysis techniques have a long history (including work by Hoare [HOA 69] and Dijkstra [DIJ 75]), formal methods were only established in the 1980s. These techniques are used to analyze the behavior of software applications written using a programming language. The correctness of a program (correct behavior, program completion, etc.) is then demonstrated using a program proof based on the calculation of the weakest precondition [DIJ 76].

The formal method (Z [SPI 89], VDM [JON 90] and the B method [ABR 96, ARA 97]) for industrial applications and their suitability for use in industrial contexts dates back to the late 1990s. Formal specifications use mathematical notations to give a precise description of system requirements.

NOTE 1.– Z – A Z specification is made up of schematic diagrams and of sets used to specify a computer system. A specification is a set of schematic diagrams.

NOTE 2.– The Vienna development method (VDM) is a formal method based on a denotational and operational vision (programs are seen as mathematical functions), unlike Z or the B method, which are based on axiomatic set theory.

One stumbling block is the possibility of implementation within the context of industrial applications (on a large scale, with cost and time constraints, etc.); this implementation requires tools to have attained a sufficient level of maturity and performance.

Note that for critical applications, at least two formal methods make use of recognized and widely available design environments covering part of the code specification process while implementing one or more verification processes: the B method [ABR 96], the LUSTRE language ([HAL 91, ARA 97]) and its graphic version SCADE1 [DOR 08]. The B method and the SCADE environment have been used successfully in industrial tools.

To give an example, Atelier B, marketed and sold by CLEARSY2, is a tool that covers the entire development cycle involved in the B method (specification, refining, code generation and proof). Note that Atelier B3 has been freely downloadable since version 4.0.

Formal methods are based on a variety of formal verification techniques such as proof, model checking [BAI 08] and/or simulation.

Formal methods are now becoming increasingly widely used, but are still relatively marginal when viewed in terms of the number of lines of code involved. To date, far more lines of ADA ([ANS 83]), C ([ISO 99]) and C++ code have been produced manually than through the use of a formal process.

For this reason, other formal techniques have been implemented in order to verify the behavior of software applications written in languages such as C and ADA. The main technique, abstract program interpretation, is used to evaluate all the behaviors of a software application by static analysis. In recent years, this type of technique has been applied to a number of tools, including POLYSPACE4, Caveat5, Absint6, FramaC7 and ASTREE8.

The effectiveness of these static program analysis techniques has been greatly improved with increases in the processing power of personal computers. Note that these techniques generally require the insertion of additional information, such as preconditions, invariants and/or postconditions, into the manual code.

SPARK Ada9 is an approach in which the ADA language [ANS 83] has been extended [BAR 03] to include these additional tools and a suite of tailored tools has been created.

I.2. Aims of this book

[BOW 95] and [ARA 97] provided the first feedback from industrial actors concerning the use of formal techniques, notably the B method [ABR 96], the LUSTRE language [HAL 91, ARA 97] and SAO+, the precursor of SCADE10 [DOR 08]. Other works, including [MON 00, MON 02] and [HAD 06], give an overview of formal methods from a more academic perspective.

Our aim in this book is to present real-world examples of the use of formal techniques in an industrial context.

For our purposes, the phrase “formal techniques” is taken to mean the different mathematically based approaches used to demonstrate that a software application respects a certain number of properties.

Note that the standard use of formal techniques consists of producing specification and/or design models, but that formal techniques are increasingly seen as tools for verification (static code analysis, to demonstrate that properties are respected, to demonstrate good management of floating points, etc.).

This book is the fourth volume in a series covering different aspects:

– Static Analysis of Software [BOU 11] concerns examples of the industrial implementation of formal techniques based on static analysis, such as abstract interpretation, and includes examples of the use of ASTREE, CAVEAT, CODEPEER, FramaC and POLSYPACE.

– Formal Methods: Industrial Use from Model to the Code [BOU 12b] presents different formal modeling techniques used in the field of rail transport, such as the B method, SCADE, Simulink DV, GaTel and Control Build and other techniques.

– Industrial Use of Formal Method, Formal Verification [BOU 12a] presents different tools used in formal verification: SPARK ADA, MaTeLo, AltaRica, Polyspace, Escher and B-event.

– This volume gives examples of the industrial implementation of the B method [ABR 96], SCADE and verification using Prover Verifier. Note that this volume (which presents examples of application using the B method) constitutes a useful addition to university textbooks such as [LAN 96], [WOR 96] and [SCH 01].

I wish to thank all the industrial actors who have freely given their time to contribute such interesting and informative chapters for this book.

I.3. Bibliography

[ABR 96] ABRIAL J.R., The B Book: Assigning Programs to Meanings, Cambridge University Press, Cambridge, August 1996.

[ANS 83] ANSI, Norme ANSI/MIL-STD-1815A-1983, Langage de programmation Ada, 1983.

[ARA 97] ARAGO, “Applications des méthodes formelles au logiciel”, Observatoire Français des Techniques Avancées (OFTA), vol. 20, Masson, June 1997.

[BAI 08] BAIER C., KATOEN J.-P., Principles of Model Checking, MIT Press, 2008.

[BAR 03] BARNES J., High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley, 2003.

[BOU 11] BOULANGER J.-L. (ed.), Static Analysis of Software, ISTE, London, & John Wiley & Sons, New York, 2011.

[BOU 12a] BOULANGER J.-L. (ed.), Industrial Use of Formal Method, Formal Verification, ISTE, London, & John Wiley & Sons, New York, 2012.

[BOU 12b] BOULANGER J.-L. (ed.), Formal Methods: Industrial Use from Model to the Code, ISTE, London, & John Wiley & Sons, New York, 2012.

[BOW 95] BOWEN J.P., HINCHEY M.G., Applications of Formal Methods, Prentice Hall, 1995.

[COU 00] COUSOT P., “Interprétation abstraite”, Technique et Science Informatique, vol. 19, nos. 1–3, pp. 155–164, January 2000.

[DIJ 75] DIJKSTRA E.W., “Guarded commands, nondeterminacy and formal derivation of programs”, Communications of the ACM, vol. 18 no. 8, pp. 453–457, August 1975.

[DIJ 76] DIJKSTRA E.W., A Discipline of Programming, Prentice Hall, 1976.

[DOR 08] DORMOY F.-X., “Scade 6 a model based solution for safety critical software development”, Embedded Real-Time Systems Conference, 2008.

[HAD 06] HADDAD S., KORDON F., PETRUCCI L., (eds.), Méthodes formelles pour les systèmes répartis et coopératifs, Hermes, 2006.

[HAL 91] HALBWACHS N., CASPI P., RAYMOND P., et al., “The synchronous dataflow programming language Lustre”, Proceedings of the IEEE, vol. 79, no. 9, pp. 1305–1320, September 1991.

[HOA 69] HOARE C.A.R., “An axiomatic basis for computer programming”, Communications of the ACM, vol. 12, no. 10, pp. 576–580, 583, 1969.

[ISO 99] ISO. ISO C standard 1999, Technical report, 1999. Available at http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf.

[JON 90] JONES C.B., Systematic Software Development Using VDM, 2nd ed., Prentice Hall International, 1990.

[LAN 96] LANO K., The B Language and Method: A Guide to Practical Formal Development, Springer Verlag London Ltd., 1996.

[MON 00] MONIN J.-F., Introduction aux méthodes formelles, Hermès, 2000.

[MON 02] MONIN J.-F., Understanding Formal Methods, HINCHEY M. (Trans. ed.), Springer Verlag, 2002.

[SCH 01] SCHNEIDER S., The B-Method: An Introduction, Palgrave, 2001.

[SPI 89] SPIVEY J.M., The Z Notation: A Reference Manual, Prentice Hall International, 1989.

[WOR 96] WORDSWORTH J., Software Engineering with B, Addison-Wesley, 1996.

1 The SCADE development environment is marketed by ESTEREL-Technologies – see http://www.esterel-technologies.com/.

2 For more information on CLEARSY and Atelier B, see http://www.clearsy.com/.

3 Atelier B and the associated information may be obtained at http://www.atelierb.eu/.

4 See http://www.mathworks.com/products/polyspace/ for further information concerning Polyspace.

5 See http://www-list.cea.fr/labos/fr/LSL/caveat/index.html for further information concerning Caveat.

6 See http://www.absint.com/ for further information concerning Absint.

7 Further details may be found at http://frama-c.com/.

8 See http://www.astree.ens.fr/ for further information concerning ASTREE.

9http://www.altran-praxis.com/spark.aspx offers additional information concerning SPARK Ada technology.

10 Note that SCADE started out as a development environment using the LUSTRE language, before becoming a language in its own right from version 6 onwards (the code generator for version 6 uses a SCADE model instead of LUSTRE code as input).

1Formal Description and Modeling of Risks

Chapter written by Jean-Louis BOULANGER.

1.1. Introduction

Formal methods are currently used to design software aspects of systems. The “internal model verification” aspect of these methods is based on the hypothesis that the model contains requirements that must be respected by the program. To obtain a useful set of requirements, we recommend establishing a connection between risk analysis, specifications and formal models. This approach allows us to define one or more formal models for use at a system level. As we will see, the proposed system model combines risks, software and hardware requirements and usage procedures.

This approach requires us to modify certain practices. Risk analysis generally takes place during the system development cycle and during the development of associated application software. The system design processes include a feasibility analysis stage, where designers define the characteristics of the environment and identify the associated risks. In this chapter, we will show that system risk analysis can be carried out using a formal model. This formal model can be used as a reference point, as a tool to support reflection and as a tool for analyzing the impact of changes. Our aim in this book is to provide an approach for the formalization and monitoring of risks, taking account of the requirements of system components (software and hardware). The proposed methodology is based on the use of the formal method known as the “B method” [ABR 96].

This methodology conforms to the requirements set out in the European Committee for Electrotechnical Standardization (CENELEC1) reference document for application to rail transport systems. This document consists of three standards: EN 50126 [CEN 99], EN 50129 [CEN 03] and EN 50128 [CEN 01, CEN 11]. These three standards recommend the implementation of a process based on the notion of requirements, with consideration given to operational safety throughout the whole system design cycle.

This chapter is divided into four sections. First, we will present the standard safety procedures used for rail transport systems. Then, we will establish a methodological context. Next, we will present a case study, analyzing the risk of collision between two trains. Finally, we will present a formal model and analysis. We will conclude by considering the methodology and its implementation.

1.2. Standard process

1.2.1. Risks, undesirable events and accidents

In the context of rail transport systems, we wish to avoid accidents. An accident (see definition 1.1) is a situation that may be associated with different types of damage (individual or collective).

DEFINITION 1.1.– (ACCIDENT – EN 50129).– An accident is an unexpected event or a sequence of events leading to death, injury, loss of a system or service, or damage to the environment.

With terrestrial transports, as indicated in [BAR 90], accidents may be categorized into different classes:

– System-initiated accidents: the users of the system are in a passive position and are victims of the damage, which can be attributed to failures on the part of the staff (maintenance, intervention, operation, etc.), to failures internal to the system or to anomalous circumstances in the environment.

– User-initiated accidents: this category refers to events surrounding one or several users (malaise, panic, suicide, etc.).

– Accidents initiated by a system–user interaction: as opposed to the previous category, in this case the user is active and interacts with the system. Incorrect use of the system lies at the root of this type of accident (e.g. non-compliance with the audio signal for door closure).

In aiming to avoid accidents, we must take account of the possibility of these accidents occurring when creating a system. The definition given above highlights the notion of an event, which may be refined by considering the notion of undesirable events (see definition 1.2).

DEFINITION 1.2.– (UNDESIRABLE EVENT).– An undesirable event is an event that must be avoided, or that must have a very weak probability of occurring.

We can distinguish between two types of damage: individual damage and collective damage.

A user-initiated accident is likely to provoke damage to individuals, whereas the remaining two categories can cause damage either to individuals or collectivities. Once the category is identified, the level of severity of the accident2 can be determined: insignificant (minor), marginal (significant), critical and catastrophic.

In [HAD 98], which applies exclusively to the context of rail transport, the authors proposed an accident typology connecting categories of accidents, potential accidents, damage types, severity levels, types of danger and dangerous elements. This typology allows us to establish links between dangerous elements, such as a lightning strike, and system accidents, such as a train collision.

The “accident” situation is definitive; the concept of potential accidents is therefore a useful one. The notion of a potential accident refers to a known situation which may lead us to an accident.

For rail transport systems, the list of potential accidents (see definition 1.3) includes derailment, passengers falling, collision, dragging or trapping individual victims, electrocution, fire, explosions, flooding, etc.

DEFINITION 1.3.– (POTENTIAL ACCIDENT).– A potential accident is an unexpected event or a series of events that may lead to an accident following the occurrence of an additional event which is not mastered by the system.

Figure 1.1.Example of classification of a potential accident

Figure 1.1 is taken from [HAB 95]. It shows an example of the classification of a potential accident, in this case a collision. The potential accident situation is linked to the notion of danger (see definition 1.4).

DEFINITION 1.4.– (DANGER – EN 50126).– A danger is a condition which may give rise to a potential accident.

A danger (see definition 1.4) is therefore a dangerous situation, the consequences of which may be damaging to human life (injury or death), to society (loss of production, financial loss, damage to image, etc.) or to the environment (damage to the natural and animal world, pollution, etc.). The terms “danger” and “threat” are used on the basis of whether the origin is random or voluntary (deterministic). The term “threat” is therefore used in the context of safety and/or security/confidentiality activities.

Dangers may be grouped into three categories: dangers created by the system or its equipment, dangers created by human activity (operator errors, maintenance errors, passenger actions, etc.) and dangers linked to unusual environmental circumstances (earthquakes, wind, fog, heat, humidity, etc.).

For a given system, dangerous situations are identified through systematic analysis, which consists of two complementary phases:

– an empirical phase, based on feedback (existing lists, accident analysis, etc.);

– a creative and/or predictive phase that may be based on brainstorming, forecasting studies, etc.

The notion of danger (dangerous situations) is directly linked to the notion of fault.

Figure 1.2 shows the pathway leading from an undesirable event to an accident. Note that the potential accident will only occur with the right operational context. For example, if a driver fails to follow a red light when moving onto a different line, the risk of an accident is much lower if this line is a small one with little traffic than if the train is joining a main line with high traffic levels. The passage from an undesirable event to a dangerous situation is linked to the technical context in a similar way.

Figure 1.3 shows the full sequence of events from a cause to a potential accident (see [BLA 08], for example, for further details). The notion of causes is used to bring in different types of faults which may affect the system, such as faults concerning one or more functions (a function may be associated with multiple parts of the internal equipment), equipment faults, human error or external factors (electromagnetic compatibility (EMC), etc.).

Figure 1.2.Chain of events leading to an accident

Figure 1.3.Chain of events leading to a potential accident

Figure 1.4 shows the combinatorics involved in a potential accident. Analysts must then identify representative scenarios (cause/undesirable event/dangerous situation/potential accident).

Figure 1.4.Combinatorics of events leading up to a potential accident

1.2.2. Usual process

In safety applications, safety demonstration [AUC 96] relies on two kinds of activities:

– Risk analysis is performed at the system specification level. Undesirable events are identified by safety engineers and the risk analysis checks that system specifications are robust enough to prevent these events from occurring. A system safety framework is used to describe the activities to be performed throughout the system lifecycle.

– Testing activities: dedicated system engineers specify a “safety oriented” testing strategy, and a specific team is responsible for the implementation of testing tasks.

Once the system-level specifications and basic implementation concepts are validated by risk analysts, development is organized as for any other project. The safety testing strategy is destructive; discontinuity occurs in the safety activity process, meaning that safety objectives cannot be easily traced. It is also difficult to test for completeness [BOU 97b] and to test system completion mechanisms.

Figure 1.5.Safety management

1.2.3. Formal software processes for safety-critical systems

Using the software lifecycle shown in Figure 1.6, formal methods allow us to integrate validation and verification activities into the design and development process. Refinement and proof activities contribute to design and development steps. Consequently, safety properties become traceable if they have been included in the formal model. The “missing link” in this type of approach is located between system and risk analysis and formal modeling. There is no traceability between safety objectives at the system level and properties which are proved during the software lifecycle. This means that there is no traceability between proven properties and the safety testing strategy.

Figure 1.6.Classic lifecycle

In system modeling, a distinction is traditionally made between safety and liveness properties. A safety property stipulates that specific “bad things” will not happen during execution, while liveness properties stipulate that certain “good things” will (eventually) happen.

Figure 1.7.Software formal process for safety critical system

1.2.4. Formal methods for safety-critical systems

“A system may be proved if and only if it has been designed to be proved”. In our opinion, formal methods (whether model checking methods or rewriting-based methods) are efficient for, and applicable to, large safety-critical systems if the system design makes the system provable [RUS 93]. The objective of this study is to define a system design process, including the demonstration that safety properties have been achieved. It is a constructive approach based on the safety kernel concept [RUS 89].

1.2.5. Safety kernel

In the field of safety, a safety kernel (see Figure 1.8) is a set of components, whose correction properties ensure that safety properties for the whole system are verified. In this section, we will demonstrate the applicability of this approach to safety-critical systems. Kernel-based architectures are characterized by a set of second-order properties: ∀ α ∈ op*, P(α). Such properties state that whatever operations or events (op*) occur from the kernel environment, the system’s properties will be verified.

This type of approach involves two main design features:

– The safety properties of the system must be formalized in terms of kernel functions and related correction properties.

– No assumption is made for the system components, which are not within the kernel.

Figure 1.8.Safety kernel

1.3. Methodology

1.3.1. Presentation

In the context of our work, we wish to define a risk mastery process, which allows us to design a safe system rather than demonstrating the safety of a system at the end of the development process. In [BOU 97a], we presented the issues surrounding development based on the notion of properties. In this section, we will show how risk analysis may be integrated into the system (or subsystem) design phase.

The abstract system model must show and take account of all properties derived from risks. This abstract model is the starting point of the design process. The description of objects then becomes increasingly precise, design choices are made and the abstract model is refined or broken down in order to define an implementation. Different steps are validated by demonstrating that properties have been respected and by verifying the conservation of behavior of intermediate models.

1.3.2. Risk mastery process

Following an initial, informal requirement specification stage, which aims to give an understanding of the formal specification (specification of general principles of the rail transport system, expression of risks to cover and preliminary risk analysis, informal listing of general safety principles), our proposed risk-elimination procedure consists of five distinct steps:

1) Formalization of the evaluation target (as specified in ITSEC3 [DEL 96] and [ITS 91, ITS 93]).

This involves the creation of a formal specification of the command system environment, the failure modes to consider and the safety objectives (formalization of risk coverage), with the aim of providing a precise, formal definition of the scope of the study.

2) Formal definition of the abstract command system and demonstration of risk coverage.

The abstract system is defined by the functions it fulfills and the properties of these functions that constitute safety principles. It should therefore be possible to demonstrate that these principles are sufficient to “fence in” the risk.

3) Projection of the abstract system onto subsystems and equipment. Introduction of the formal definition of the safety kernel of the command system.

This phase involves the specification of the system architecture, which is then used to refine the properties of the abstract command system as set out in step 2. Our definition of the notion of a safety kernel is set out in [RUS 89], as the set of material and software components which are required in order to cover risks and which, in terms of safety properties, are insensitive to normal or abnormal changes to the rest of the command system.

4) Demonstration of the properties of the safety kernel.

We must show that the safety properties of the kernel are invariant to all operations outside of the kernel (including the failure of elements outside the kernel, within the limits specified in point 1) and demonstrate that the properties of the kernel are sufficient to guarantee the properties of the abstract system.

5) Risk elimination.

In this step, we must show that the implementation of the kernel satisfies our safety properties. This activity involves a certain number of checks and requires us to provide a number of justifications over the course of the production cycle. Figure 1.8 shows possible errors for each stage in the development process along with the means of identifying anomalies.

The aim of this approach is to force system designers to clearly set out design principles which are essential for safety, to minimize the system subset which requires formal validation and, finally, to produce a traceable proof tree in which the “leaves” are closed by:

– validation of materials, either in terms of intrinsic safety or probabilities;

– analyzing the physical implementation (track plans, physical installation);

– properties of the usage principles of the system;

– proof or safety validation of programs.

In this context, we will limit our consideration to phases 1, 2 and 3.

Table 1.1.Connections between activities and risks

Activity

Error/risk

Coverage

Identification of root properties

Edge errorsIncomplete mission analysisPoor description of risks

Analysis of the requirement acquisition processFeedback analysisPreliminary risk analysis

Allocation of properties to subsystems and identification of the properties of interfaces between subsystems

Property incompletenessIncoherency between properties

Implementation of traceabilityProof of root properties

Development of subsystems and validation with regard to properties

Design faults made during the development process

Risk analysis of the development processProof of formal modelsTesting of non-formal components

Interfaces between formal/non-formal components

Incoherency between interfaces (e.g. interfacing between generic program and data)Incompleteness of services

SEEA

4

Constraint identificationConstraint testing

Generation of executable elements:– code generation– compilation– linkage

Code does not conform to the applicationPoor formal/non-formal integrationPoor integration between generic program and data

Risk analysis of the code generation process.Certification/qualification of toolsTest of correct operation

Executable elements

Analysis of installation procedures

Dynamic verification of the checksum of the executable element

1.4. Case study

This section corresponds to phase 1. We will define the perimeters of the study by establishing environmental characteristics and a list of risks.

1.4.1. Rail transport system

The whole ground transportation system in its environment is composed of the following subsystems:

– Rolling stock: this subsystem performs functions according to dynamics and kinematics, and according to commands set by the control/monitoring system.

– Control and communications: this is divided into two functional subsystems: one is devoted to operations control (train description, communication with operators, etc.) and the other one is automatic train pilot (ATP). ATP is divided into ground ATP and on-board ATP. Finally, the ground functions of ATP are distributed across the topology, while the on-board functions are replicated on trains.

– Vital signaling: this subsystem monitors trackside equipment such as points, train detectors, track circuits and wayside signals. It interacts with ATP for route setting: routes are defined at ATP level and are set by the signaling system.

– Civil engineering: this subsystem defines the physical implantation of trackside equipment, the topology (distances, slopes, etc.) etc. It interacts with ATP subsystems through parameters known as “topological parameters”.

1.4.2. Presentation

We will use an example to illustrate the proposed methodology, considering train collision problems. As we see in [CLE 01], trains represent a particularly safe mode of transport, and collision is the main type of accident which may arise. The movement of trains along a line must respect rules established in order to guarantee safe circulation. The risks associated with moving trains include collision, derailment and travel risks (access to dangerous zones, etc.).

The risk of collision may be classified into several types:

– collision from behind (with a rail transport vehicle);

– head-on collision (with a rail transport vehicle);

– side-on collision;

– collision with an object or another type of vehicle.

The analysis of different collision types is outside the scope of this book; in the following sections, we will focus on side-on collisions.

1.4.3. Description of the environment

A railway line (Figure 1.9) is made up of several tracks. Trains use tracks to move from one point to another. A track is made up of several track circuits (TCs). A track circuit is a physically defined portion of track, which detects the presence of trains by “shunting5”.

Figure 1.9.Example of topology

A basic track circuit (a branch) has the following characteristics:

– beginning and end;

– state (shunted, non-shunted);

– previous track circuit and next track circuit.

A single abscissa reference point is defined by deconstructing the line. Each position (track object or train) is characterized by a pair (track number and abscissa). Passages from one track to another are carried out using switches. As we see in Figure 1.10, a switch is a three-branch track circuit, made up of a fixed component and a mobile component (the point). A point has three logical states: uncontrolled (operational fault detected), a straight position or a divergent position.

Figure 1.10.Static and dynamic definitions of a switch

A switch can therefore be seen as a track circuit, and has the following characteristics:

– Track circuit characteristics:

- point abscissa, divergent abscissa and direct abscissa,

- track circuit following point, TC following direct, TC following divergent;

- state: shunted and non-shunted.

– Switch characteristics,

- type: right and left,

- state: direct, divergent and uncontrolled.

We may define a certain number of operators which aim to manipulate the characteristics of a point.

Figure 1.11.Side-on collision

1.4.4. Definition of side-on collision

The movement of trains on a switch creates a risk of side-on collision. This type of collision is due to the fact that a train moving on the switch may “catch” a stationary train in the point zone (see Figure 1.11). Figure 1.12 gives an example of a formalization of the side-on collision risk. This formalization takes account of time and the position of the two trains.

Figure 1.12.Property associated with side-on collision

This formalization is constructed using a number of position operators:

– The operator “pos_2_tc” gives us the support track circuit of a coordinate.

– The operator “tc_support” gives us the support track circuit of a train.

– “pos” gives us the abscissa of a coordinate.

– “a” is an operator giving the abscissa of a train.

Train spacing in manual drive mode is regulated by the implementation of lateral signaling. These signals have two characteristics:

– a position (track, abscissa);

– a state: permissive or restrictive.

Signals are associated with routes. Routes represent pathways that are accessible to trains, and are characterized by:

– start and end positions;

– an entry signal;

– a list of switches located on the pathway and their expected positions (divergent, direct);

– information characterizing the fact that the route is accessible, which corresponds to the state of lights and the position of points located on the pathway.

1.4.5. Risk analysis

We may analyze the risk of side-on collision using a fault tree analysis. Fault tree analysis is used to identify the causes of potential problems with a product, process or service. This analytical tool is generally used for reliability predictions or in analyzing design performance. Fault tree creation is a graphical methodology that enables systematic description of the impact of faults, which may occur during the lifetime of a system (see [IEC 90] for further details). This method takes account of both “material” faults (hardware) and human error. This technique gives us an overview of potential problems and their relationships, while requiring a detailed analysis permitting active intervention during the design phase. Figure 1.13 shows a reduced and simplified version of the fault tree associated with the risk of side-on collision.

Figure 1.13.Fault tree

Figure 1.13 shows two types of cases of side-on collision: either both trains are moving or one of the trains may be stationary. For cases where both trains are moving (Figure 1.14), we may identify physical faults (absence of signals, faulty display or physical non-detection of the train), a behavioral fault (the driver does not respect the signal) and a control/command system failure.

Figure 1.14.Fault tree for the case of two moving trains

Side-on collisions in cases where only one of the trains is moving (Figure 1.15) result from the fact that the stationary train is outside the safe position (the crossing point). This may occur if there has been a delay in responding to a signal, or if track objects are not in the correct positions.

Figure 1.15.Fault tree for the case of one moving and one stationary train

1.5. Implementation

In this section, we will present the broad outlines of the B model and the connections between risk analysis and the proof of the model, corresponding to phase 2 of our proposed process.

1.5.1. The B method

The B method was developed by J.-R. Abrial [ABR 96]. It is a model-oriented formal model, such as Z [SPI 89] and VDM [JON 90], and allows incremental development from specification to coding using the notion of refining [MOR 90], using a single formalism, the abstract machine language. Proof obligations are generated at each stage of the B development in order to guarantee the validity of the refined version and the consistency of the abstract machine.

On reaching the final refinement (implementation), the level of modeling is sufficiently concrete to allow the use of a compatible automatic code generator (C, ADA and others). The B (sub-) language available at the implantation level is known as B0. The syntax and semantic restrictions placed on B0 allow the direct construction of the translator. The B method is currently used in the context of rail transport to develop safety software applications (for example, [DEH 94], [BEH 93] and [WAE 95]). Abrial has also proposed an extension known as “Event-B” [ABR 00, ABR 01], intended for use in analyzing system aspects.

1.5.2. Implementation

The initial component of our model represents the system aspect, and needs to include the basic functions and properties associated with the risks which must be covered. Subsystems, then components and their properties, are introduced iteratively by refinement and decomposition until we obtain the level of description introduced by the textual specification. The model must be traceable in relation to the textual specification, as presented in section 1.3, in terms of both functions and associated properties.

1.5.3. Specification of the rail transport system and side-on collision

The component system_0 gives the initial behavior of the command control system of a rail transport system in the form of a safety property that must be demonstrated in order to cover the risks involved in this type of system. In this case study, the risk we wish to cover is the side-on collision risk, associated with switches, as shown by the property in Figure 1.13.

The implantation of the system takes the form of three subsystems:

– trains and their physical behaviors (wheel/rail interaction), via the machine Physical_0;

– signal control, via the machine Vital_Signalling_System_0;

– the train autopilot system via the machine ATP _0 (TRACK, TRAIN).

The B model as a whole will not be presented in this chapter; instead, we will consider certain aspects of the formalization. Figure 1.16 shows a view of the associated structure of the B model.

Figure 1.16.Architecture of the B model

A physical track is made up of track circuits, points and signals. The signals are related to routes which describe the authorized pathways that trains may take. These four object types are introduced as a set. The links between objects are described through mathematical functions which are used to describe properties. The set is located in the component “Topology_0”.

The fact that three signal lights are associated with each point is shown by the following properties:

The set of track circuits may be seen as a graph, described by the variable “track_next”, which has the following properties:

maximum three connections.

minimum two connections.

The component “system_0” introduces essential properties of the system, notably properties associated with safety. The properties characterizing the physical behaviors of the system are also introduced at this point. The two properties below indicate that the track objects (points and track circuits) have intrinsic safety. The first property shows that points can only be controlled from one position. The second property shows that if a track circuit is free, then no train is present.

The property preventing side-on collision is included in the main machine “system_0” in the following form:

Figure 1.17. gives a simplified representation of the proof.

The B model introduces the physical properties needed to produce a proof, but these need to be validated using trade procedures (e.g. drivers must respect signals) and specific demonstrations (components such as signals and track circuits must possess intrinsic safety).

Figure 1.17.Structure of proof

1.6. Conclusion

In this chapter, we have shown how the implementation of safety analysis (using a fault tree or FMECA, for example) during system design allows us to increase trust levels. This approach is particularly recommended for “safety” applications.

The aim of the suggested approach is to compel system designers to specify the design principles (intrinsic safety, usage procedures, maintenance processes, etc.) required for system safety, to minimize the subset of the system requiring formal validation, and, finally, to produce a traceable proof procedure. The notion of safety kernels aims to limit the size of elements involved in safety and to highlight the faults that must be taken into account in the design process.

In this chapter, we have used the B method as a support language; other languages may be used, but it is essential to formalize and trace the principles used in order to facilitate the demonstration of system safety.

1.7. Glossary

ATC: automatic train control

ATP: automatic train protection

CENELEC: Comité Européen de Normalisation Electrotechnique (European Committee for Electrotechnical Standardization)

FMECA: failure modes, effects and criticality analysis

FTA: fault tree analysis

ITSEC: information technology security evaluation criteria

1.8. Bibliography

[ABR 96] ABRIAL J.-R., The B Book: Assigning Programs to Meanings, Cambridge University Press, August 1996.

[ABR 00] ABRIAL J.-R., Event driven circuit construction, MATISSE project, August 2000.

[ABR 01] ABRIAL J.-R. Event driven distributed program construction, MATISSE project, August 2001.

[AUC 96] AUCLAIR J.P., BARANOWSKI F., CASPI P., et al., “Principes d'organisation pour la réalisation de logiciels critiques”, AFCET, 1996.

[BAR 90] BARANOWSKI F., Définition des objectifs de sécurité dans les transports terrestres, Technical Report 133, INRETS-ESTAS, 1990.

[BEH 93] BEHM P., “Application d'une méthode formelle aux logiciels sécuritaires ferroviaires”, Ateliers Logiciel Temps Reel – 6èmes Journées Internationales du Génie Logiciel, Part 5.1, 17–19 November 1993.

[BLA 08] BLAS A., BOULANGER J.-L., “Comment améliorer les méthodes d’analyse de risques et l’allocation des THR, SIL et autres objectifs de sécurité”, LambdaMu 16, 16ème Congrès de Maîtrise des Risques et de Sûreté de Fonctionnement, Avignon, 6–10 October 2008.

[BOU 97a] BOULANGER J.-L., DELEBARRE V., NATKIN S., et al., “Deriving safety properties of critical software from the system risk analysis, application to ground transportation systems”, HASE’97, Maryland, MD, 11–12 August 1997.

[BOU 97b] BOULANGER J.-L., DELEBARRE V., NATKIN S., Validation des spécifications et génération de tests de sécurité s'appuyant sur un modèle formel d'un système de transport ferroviaire, CEDRIC Research Report No 97-17, December 1997.

[CEN 99] CENELEC, EN 50126., Railways application – the specification and demonstration of reliability, availability, maintainability and safety (RAMS), 1999.

[CEN 01] CENELEC, EN 50128., Railways application – communication, signaling and processing systems – software for railway control and protection systems, 2001.

[CEN 11] CENELEC, EN 50128., Railways application – communication, signaling and processing systems – software for railway control and protection systems, 2011.

[CEN 03] CENELEC, EN 50129., Railways application – safety related electronic systems for signaling, 2003.

[CLE 01] CLÉON L.-M., LECUSSAN R., “L’apport des études d’accidentologie”, Revue Générale des Chemins de fer, pp. 17–22, February 2001.

[DEH 94] DEHBONEI B., MEJIA F., “Formal development of software in railways safety critical systems”, in MURTHY B.T.K.S., MELLITT C., BREBBIA G., et al., (eds.), Railway Operations, COMPRAIL ’94, vol. 2, Computational Mechanics Publications, pp. 213–219, 1994.

[DEL 96] DELEBARRE V., NATKIN S., “Conception et évaluation de logiciels critiques: de la sécurité logique à la sécurité physique”, Congrès sur l’application des méthodes formelles, ENSIMAG, Grenoble, January 1996.

[HAB 95] HABIB H.-M., “La maitrise des risques dans le domaine des automatismes des systèmes de transport guidés: le problème de l’évaluation des analyses préliminaires de risques”, Revue Recherche Transports Sécurité, vol. 49, pp. 101–112, December 1995.

[HAD 98] HADJ-MABROUCK H., STUPARU A., BIED-CHARRETON D., “Exemple de typologie d’accidents dans le domaine des transports guides”, Revue Générale des Chemins de Fers, 1998.

[IEC 90] INTERNATIONAL ELECTROTECHNICAL COMMISSION (IEC), Fault tree analysis (FTA), International standard IEC 61025, International Electrotechnical Commission, Geneva, Switzerland, 1990.

[ITS 91] ITSEC, Information technology security evaluation criteria, Technical report, June 1991.

[ITS 93] ITSEM, Information Technology Security Evaluation Manual, CEC Publication, September 1993.

[JON 90] JONES C.B., Systematic Software Development Using VDM, 2nd ed., Prentice Hall International, 1990.

[MOR 90] MORGAN C., Deriving Programs from Specifications, Prentice Hall International, 1990.

[RUS 89] RUSHBY J., “Kernel for safety”, Safe and Secure Computing Systems, Blackwell Scientific Publications, London, 1989.

[RUS 93] RUSHBY J., Formal methods and the certification of critical systems, SRI Research report, November 1993.

[SPI 89] SPIVEY J.M., The Z Notation: A Reference Manual, Prentice Hall International, 1989.

[WAE 95] WAESELYNCK H., BOULANGER J.-L., “The role of testing in the B formal development process”, ISSRE 95, Toulouse, October 1995.

1 See http://www.cenelec.eu/Cenelec/Homepage.htm.

2 We have chosen to focus on the rail transport domain [CEN 99]; however, we have indicated alternative terms in brackets whenever they are used in other sectors.

3 ITSEC: information technology security evaluation criteria. More information is available at www.itsec.org.

4 SEEA: software error effect analysis. The SEEA is a software analysis methodology based on failure modes, effects and criticality analysis (FMECA), where we examine the effect of an error on each entry in a piece of code. This approach is widely used in the domain of rail transport for critical software applications.

5 The track circuit has a power supply. When two wheels of the same axle of a train are in the zone delimited by the track circuit, a short circuit occurs, and the train is said to be shunting the track circuit. The main function of the track circuit is to detect shunting.

2An Innovative Approach and an Adventure in Rail Safety

Chapter written by Sylvain FIORONI.

2.1. Introduction

In the context of a project with high stakes for success and limited room for maneuver, the decision to use formal proof to demonstrate the safety of critical software may seem daring. This choice was made possible by the presence of teams with a strong belief in this technique at each stage of the development process and their intuition, drive and will to succeed were essential to the success of the project.

When compared with testing methods, formal proof requires skill sets which are harder to find; the tools involved use highly precise algorithms, and the method as a whole is more difficult to master. When used well, however, this approach produces significant gains, both in economic terms and with regards to the safety assurances given by the results.

Formal proof limits the number of iterations in software development, as programs are consolidated early in the development cycle. Furthermore, it results in higher trust levels than those obtained by testing when demonstrating system safety, through exhaustive exploration of the satisfaction of safety requirements by system behaviors.

In the 1980s, the RATP (Régie Autonome des Transports Parisiens, Autonomous Operator of Parisian Transports) was involved in launching critical systems including the first control-command programs for rail transport across its network, and needed to ensure that the safety levels of the developed systems were at least equivalent to those of existing systems, based on the physical principles of “intrinsic safety1”. In this context, careful consideration was given to formal proof, and the potential of this technique quickly became apparent. The “classic” software development process (structured method, testing, verification and analysis) produces high-quality programs, but trust levels in safety terms (based essentially on a percentage of coverage) remain questionable when compared with intrinsic safety methods, which allow us to demonstrate that given safety levels have been attained.

Formal proof therefore had much to offer, and the safety level of a program would no longer be based on the classic software development process alone. The RATP decided to use this method to evaluate the safety levels of the critical programs of the SACEM2 [OFT 97] by retro-engineering. The lack of viable tools on an industrial scale meant that the RATP was obliged to implement studies of formal evaluation techniques for safety programs. This approach proved fruitful, highlighting around 20 faults which had not been picked up during testing, and led to the creation of the techniques used in the formal B method [ABR 96] (developed by Jean-Raymond Abrial, who was involved in the study process).

RATP management were convinced of the interest presented by the approach, and the B method was used in the 1990s to develop the critical programs used in SAET-METEOR3 [CHA 96, MAT 98] for the fully-automatic line 14 of the Paris metro. This decision led to the creation of a partnership and the provision of resources for the industrialization of formal proof tools for the B method [ABR 96].

The combination of the B method for software design, producing programs which are intrinsically safe by construction, and an ASA+4 modeling of the specification with property verification [BOU 06] based on model-checking [BAI 08] to consolidate the textual specification [BOU 00] led to the detection of a number of faults. The combination of the two approaches was a great success, and, since their implementation in 1998, the programs in question have never needed to be modified for safety reasons.

In addition to the assurance proof provides in relation to safety requirements, these first applications of formal techniques clearly show that the formalization of a system and of requirements plays a significant role in consolidating system functionality and in safety demonstration, as the approach requires rigorous identification of a context and the elimination of indeterminism and uncertainties.

The RATP has continued to use critical systems, including rail transport control-command programs, with safety software designed using tool-based formal methods (the B method, Petri networks, etc.). Furthermore, the RATP also uses formal modeling for the verification of system aspects (Event-B, AADL, etc.). The use of formal techniques concerns all automatisms used by the RATP with high and very high levels of safety integrity5 to varying extents [GLE 09]. Recent innovations made by the organization in the context of major modernization work on the Paris metro, which will be presented later in this chapter, have employed a posteriori proof techniques applied to finished programs. This has been made possible by increases in processor computing power and the introduction of design tools using formal languages, such as SCADE®.

From a project management perspective, the utility of these contributions is determined by their capacity to add value. A satisfactory response must be provided to each constraint – cost, delay, technical constraints and regulatory conditions – to reduce overall project risks. In order for an approach to be acceptable, particularly in regulatory terms, we must be able to guarantee the veracity of results established by these tools.

2.2. Open Control of Train Interchangeable and Integrated System6

The Open Control of Train Interchangeable and Integrated System (OCTYS) project presented significant risks, as the proof technology involved had never been used in an industrial context and no feedback from equivalent projects was available. Moreover, the approach needed to be qualified in order to integrate proof results in the regulatory approach for system approval.

Three groups were involved in successfully integrating proof into demonstrations of the safety of the Sol OCTYS Line 3 program: Ansaldo STS7, Prover Technology8 and the RATP9.

In this context, the RATP continued to promote advanced methods for the development of safety software (a policy which began in the 1990s with the choice of the formal B model), with the conviction that formal models provide the highest system safety levels while also reducing costs.

Ansaldo STS’s presentation of their software validation approach based on the use of proof with Prover Technology’s ProverVerifier™ tool in 2007 rapidly solved the issue of qualifying the results of proof produced by tools. This qualification, essential for safety demonstrations to be considered acceptable from a regulatory perspective, posed certain technical problems; more importantly, it required significant financial backing, and this requirement hindered the production of proofs. After extensive reflection, the RATP agreed to cover these technical and financial aspects, convinced that their investment would bring worthwhile results, and provided Ansaldo STS with a complement to the existing proof engine, allowing the demonstration report produced by this existing engine to be certified.

Along with the validation activities carried out by Ansaldo STS for OCTYS, the RATP asked Prover Technology to develop tools associated with the proof engine to guarantee that the SCADE® model would not be altered when translated into the language of the proof engine and to verify the generated proof; they then qualified the whole chain, known as the “Prover Certifier™”.

In order to reach a safety level compatible with rail transport requirements (SSIL10 level 4, as set out in the CENELEC EN 50128 [CEN 01, CEN 11] standard), the solution uses two representations of a system as input, the SCADE®11 model and the source code generated using the SCADE® model (in C or Ada), and formally establishes the equivalence of these two representations. This process also allows us to check for errors in the source code generation process. The engine attempts to establish proof that the safety requirements have been satisfied using one of these representations. Based on the outcome of the proof, the tool produces either a counter-example (failure) or a plot of the proof (success). This plot, known as the “proof certificate”, is made up of a pre-defined set of inference and rewriting rules, to be verified by a tool known as a “proof certifier”.

The RATP also took charge of the adaptations and additions required to transpose the proof activity carried out by Ansaldo STS for the certified chain. The formal proof of equivalence between the SCADE® model and the target code was a particularly sensitive point requiring attention.

Once the question of certification had been resolved, new initiatives were launched as part of an agreement between Ansaldo STS and the RATP to remove the project risks associated with failure to attain a suitable level of safety requirement coverage using proof by the time of implementation. This was done using a mixed methodology with proof of full functionality and tests of other functions, and by incremental scheduling using markers, based on the time needed to move from validating the unproven functions of the proof to a test-based approach.

The final remaining issue concerned the capacity of proof tools to process a program representing the real configuration of a line within an acceptable execution period. Tests carried out in 2008 by Ansaldo STS and Prover Technology on the Sol OCTYS Line 3 program using the full line topology resulted in an explosion in the amount of memory required by the proof engine. Ansaldo STS put forward a solution to this problem in 2007, which was adopted to allow OCTYS to be brought into service in 2009: proof was carried out for “test” configurations which had been shown, by Ansaldo STS, to cover all of the real configurations of line 3. In the course of 2010, a study carried out by Prover Technology in partnership with Ansaldo STS and the RATP succeeded in removing these technical difficulties, and it is now possible to carry out proof at the whole-line level.

The validation of the requirements of the Sol OCTYS Line 3 program represents a successful example of the use of formal proof. The enterprise was a daring one, but, due to the deep-seated convictions of those involved, it was successfully completed, with early consideration of all of the risks involved in the activity and progressive removal of the difficulties which were encountered. The gains generated by this process exceeded initial expectations (the bulk of the safety requirements were proved, with reduced costs and easy implementation of modified versions of the software, etc.). The “Prover Certifier™” certified solution has been accepted by the relevant regulatory bodies.

This experience resulted in the creation of an industrially-viable technological approach focusing on the proof of safety requirements for a program modeled using SCADE®. This approach has breathed new life into the use of formal proof, at a time when SCADE® is widely used in industrial contexts.

2.3. Computerized interlocking systems12

The computerized interlocking systems (PMI) operation at the RATP was the driving force behind the use of advanced model-checking techniques during the validation phase to establish safety demonstrations for existing critical programs.

The specificity of PMI13 is that it provides generic equipment for real-time interpretation of interlocking graphs, which display the operations of the interlocking system. The graphs are developed within a proprietary design suite using a two-step process. The first stage involves implementation of the behavior of the elementary functions of the system in the form of a set of generic graphs. The second stage consists of parameterizing these graphs to produce a site configuration. The design suite then instantiates the graphs in the form of a database loaded into the equipment.

The configuration of a PMI was previously validated through testing using a platform made up of a piece of target equipment in a simulated environment. Aiming to optimize verification and validation costs, the RATP wished to replace safety testing activities with proofs of interlocking graphs, instantiated for the configuration of the systems under consideration. To this end, the organization commissioned a PMI proof suite, known as Prover iLock PMI. The long-term goal of this project was to generate automatic safety validation of systems, whatever the configuration used.

Development of the Prover iLock PMI proof suite was based on a PREDIT14 research project known as PROOFER, bringing together the RATP, THALES RSS, responsible for the supply and development of PMIs, Prover Technology, who developed the proof suite, and VERIMAG, who validated the mathematical principles used in the proof. The chosen pathway involved constructing a “conservative” abstraction of the execution of instantiated interlocking graphs, which was then used for proof.

The research project involved a feasibility study, which confirmed the efficiency and safety of the proof validation method proposed by Prover Technology. Industrialization of the proof suite began in September 2006 and ended in November 2008 with its qualification by the RATP. The suite includes the proof itself and a certification mode, producing a safety level of SSIL4 as set out in the CENELEC EN 50128 standards [CEN 01].

The graph design suite may be used to model the generic rules of safety properties which must be respected by the interlocking graphs in the form of state automata, and instantiate these rules for the configuration of the system to validate.

From 2008 to 2011, this method was successfully applied in demonstrating the safety of 11 PMI systems across three metro lines, producing the expected benefits: reduced costs when compared to test-based methods, semi-automatic proof of new configurations by reusing the generic rule database, identification of unsafe situations which would have been difficult to identify through testing, etc.

Figure 2.1.Proof suite

2.4. Conclusion

Formal proof has attracted the interest of the rail transport community with the first rail safety control-command programs. The successful use of formal proof in large-scale projects has, on several occasions, confirmed its status as an efficient and economically viable basis for safety in automated systems.

The OCTYS and PMI projects discussed in this chapter highlight the superiority of proof compared to test-based methods in demonstrating safety, particularly in identifying unsafe situations, and through its capacity to verify high level requirements, which are difficult, if not impossible, to verify through testing15.

The decision to use formal proof is a daring one. In order to succeed, it requires a tailored project response, taking account of all of the technical difficulties and risks involved in the relevant activity from the earliest stages of the project. The challenge presented by this approach, alongside the conviction and collaborative working practices required from those involved, leads to the development of close working relationships. Those involved in projects of this type are generally more than satisfied with their choice.

With the resources currently available, a wide variety of developments are possible, for example use of the B method or proof during the validation of software designed using a formal language such as SCADE®. The generalization of formal proof in the development of critical systems may not be far off.

2.5. Glossary

CENELEC16: Comité Européen de Normalisation ELECtrotechnique, European Committee for Electrotechnical Standardization

OCTYS: Open Control of Train Interchangeable and Integrated System

PMI: Poste de Manœuvre Informatisé, Computerized Interlocking Systems

RATP17: