Railway signalling applications are strictly related to safety critical software. Railway systems have two great particularities: they are guided transportation systems for which the itineraries depend on the configuration of turnouts at a given time, and their braking performances are law compared with those of other land transportation modes. These two attributes constitute the origin of railway signalling principles which rely on two elementary functions consisting in itineraries and speed control.
The control of itineraries is materialized by the interlocking, which is totally independent of train speed. However, this speed influences directly the ability of signalling to continuously keep safe distances between trains.
Of course, theses signalling functions (including interlocking) couldn’t escape the computerization led by technological progress, with a significant ambition to replace relay based technologies by computer logic and integrate all functions into one global software system. Today, many signalling projects (i.e ERTMS/ETCS and CBTC projects) use safety critical software.
Yet, how can we make sure that the software will always keep safety requirements?
The software specification and formal design
The software specification aims to define a clear and rigorous description of what the software has to do, using various non-formal or formal notations such as the natural language, UML statecharts, Petri nets or B language… Whatever the notation used during this phase, the specification comprises all the information about the software data, its properties, environment and processing.
The formal design of the software following the specification phase consists in expressing the content of the specification using a formal-language based techniques and tool, such as the B method, High Level Language (HLL), SCADE… The goal of such a formal development is to provide mathematical proof of the compliance between the software and its specification as well as the insurance that the software will never compromise the safety of the system (error-free source code).
The vital coded processor
The formal design ensures that the software implementation is compliant with its specification. However, it is also necessary to make sure that the execution of the software is consistent regarding the source code.
Accordingly, most of safety critical signalling computerized systems, which deal with data acquisition and exchange (e.g. input/output modules, equipment interfaces…), rely on a structure controlled by a coded monoprocessor, also known as the Vital Coded Processor (VCP).
The basic principle of the Vital Coded Processor consists of a probabilistic approach using redundancy in data, space and time to detect operation errors, operand errors, dating and sequencing errors (e.g. usage of outdated operands). The data processed by the VPC is coded such as every variable (X) of the program is composed of the pair (Xf, Xc), where Xf is the value part and Xc is the control part of the variable. The program instructions are designed to deal with variables in this encoded form for both the input and the output data.
All in all, incorporating software in safety critical signalling functions amounts to ensuring its correctness and safe execution. One of the corporate most common and efficient ways to do so is the use of formal development techniques added to the Vital Coded Processor.
