Formal verification applications to ensure safety of CBTC systems

A significant number of modern metro systems around the world use Communication-Based Train Control (CBTC) for safer and more efficient train operations. While the role of CBTC is straightforward, the systems themselves are quite complex.

Due to this complexity, coupled with high safety requirements imposed on CBTC systems, both suppliers and operators have taken to implementing formal verification methods to ensure that the deployed systems meet the highest safety standards. Here, we will walk through six of these methods. But first, let’s review the basics.

What is communication-based train control?

CBTC is a modern signaling system that keeps track of a train’s position by utilizing continuous communication between wayside and carborne equipment.

From a functional standpoint, CBTC is mainly composed of two subsystems: Automatic Train Control (ATC) and Automatic Train Supervision (ATS). The ATC guarantees the safe operation of trains, while the ATS provides an overview of the system for supervision and centralized operation. The ATC is composed of two components: Automatic Train Protection (ATP) and Automatic Train Operation (ATO). ATO is in charge of operating trains while ATP is in charge of the safety of this operation.

Generic and Specific Application Levels

The complexity of CBTC systems has led suppliers to offer generic CBTC solutions which can be deployed in different locations, only by changing the configuration data and parameters. Such solutions make it possible to optimize redundant activities so they can be done once and for all at a generic level, and reduce the required workload on the location-specific level. This is usually known as Generic Application (GA) and Specific Application (SA) level, with configuration data used to instantiate one from the other.

6 verification methods used to ensure CBTC systems meet high safety standards

To improve the correctness and safety of CBTC systems, a number of formal verification methods have been applied globally with success.

The major obstacle that has been observed in these applications is the state-space explosion due to the complexity of the studied CBTC systems. In recent years, however, this issue has been tackled in different ways and, in some applications, improved results have already been observed.

1. System Configuration Data validation

The instantiation of an SA from a GA is performed by essentially integrating the so-called configuration data relative to the specific location. In order to guarantee the safety of the resulting SA, one must ensure that the configuration data are correct. Formal methods utilizing properties formalization and exhaustive data checking have been of great help in this matter.

2. Software Configuration Data generation/validation

While System Configuration Data covers system-wide aspects, subsystem software usually requires a different presentation of this data. This software configuration data is usually derived from the system-level data with a safety-preserving process. For this matter, formal methods have also been successfully applied either to generate correct software data or to check the correctness of data previously generated with another process.

3. Verification of vital requirements on software at equipment or function level
(GA or SA)

Formal verification has also been applied to verify the correct implementation of vital requirements at the sub-system level using (the whole or parts of) the subsystem’s software as a target. Compared to classical testing approaches, formal verification helps to capture the requirements and gives wider coverage of the verified behavior. In many cases, safety-related bugs have been identified only using formal verification (in projects where both techniques were used). Requirement formalization has helped to clarify a significant number of ambiguous specifications as well.

4. Verification of safety requirements at system or equipment level
(against a formalization of the System/equipment)

At the system level, formal verification of safety properties have also been performed against a formalization of the studied system/subsystem (so-called digital twin). Functional requirements are used as a basis for the development of the formal model, with some abstractions of small details. Safety properties, usually derived from system safety studies, are then checked on the formal model. This helps identify high-level discrepancies in the system specifications that might not be seen at lower-level verification.

5. Formal development process

Formal methods have also been applied successfully for the entire development process of CBTC systems. A system-level formal specification is first developed and proven to be safe. This high-level specification is then refined to include more implementation details, with the proof that the refinement preserves the safety properties. Refinement is repeated until the resulting model is detailed enough and can be implemented by a software. Since all refinement steps are formally verified, the resulting model is correct-by-construction.

6. Equivalence proofs for generated code

In some applications, when the software is automatically generated from a formal model, formal verification has been used to check the correctness of the generated code. An equivalence proof is performed between both the formal model and a formalization of the generated software.

Would you like to know more? Let our experts show you how a formal approach can help your CBTC-project. Contact us for a meeting