Formal Methods Applied to Industrial Complex Systems

Jean-Louis Boulanger

• Publisher: Wiley-ISTE
• Year: 2014
• Print ISBN: 9781848216327
• eBook ISBN: 9781119004776
• Edition: 1
• Topic: Computer Science
• Subtopic: Computer Engineering
• Index: Computer Science

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

1
Formal 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 (CENELEC¹) 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 accident² 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 tha...

Table of contents

• Cover
• Contents
• Title Page
• Copyright
• Introduction
• 1 Formal Description and Modeling of Risks
• 2 An Innovative Approach and an Adventure in Rail Safety
• 3 Use of Formal Proof for CBTC (OCTYS)
• 4 Safety Demonstration for a Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof
• 5 Formal Verification of Data for Parameterized Systems
• 6 ERTMS Modeling Using EFS
• 7 The Use of a “Model-Based Design” Approach on an ERTMS Level 2 Ground System
• 8 Applying Abstract Interpretation to Demonstrate Functional Safety
• 9 BCARE: Automatic Rule Checking for use with Siemens
• 10 Validation of Railway Security Automatisms Based on Petri Networks
• 11 Combination of Formal Methods for Creating a Critical Application
• 12 Mathematical Proofs for the New York Subway
• Conclusion
• Glossary
• List of Authors
• Index