Verification of Safety Requirements

There are two main kinds of accidents that are worth worrying about: collisions and derailments. An interlocking is safe if it prevents such accidents from happening. Of course, an interlocking cannot provide 100% prevention as long as human operators are taking an active part of the operation. But the interlocking can and will make such accidents much less likely to happen if properly constructed.

The interlocking is constructed in order to prohibit trains from entering a track at the same time (preventing collisions) and also give trains the proper speed restrictions (preventing derailments). Thus, the verification of the safety requirements is supposed to guarantee that neither of these things can happen.

Obviously, the safety requirements that need to be verified will be many and of varying character. For instance, it is crucial that all wiring between different hardware components are done according to specifications. Changing wires for switch detection is a certain recipe for disaster, for instance.

Considering the interlocking software, what kind of safety requirements needs to be verified in order to guarantee safety of the software? The general idea is that the interlocking constitutes a filter between the operator (human or computer) and the physical objects in the railyard such as signals switches and tracks.

The operator requests certain actions from the railyard hardware and the interlocking will only transmit those requests that are safe, e.g. not commanding conflicting signals to proceed, not moving switches in front of moving trains, etc. In general, safety requirements on the software should be viewed as relations between the inputs and the outputs to the software, either allowing or forbidding them.

As an example, the output for driving a switch motor should not be allowed to be high if the input from the track circuit over the switch is low, indicating that it is occupied. Also, the relations may take into consideration certain internal states such as locking.

Hence, safety requirements for the interlocking software should include enough such relations between inputs, outputs and internal states in order to guarantee that it will filter out all unsafe combinations of operational requests.

Ultimately the verification of the safety requirements should provide a convincing argument for that the software fulfills the relations between inputs, outputs and internal states that are mentioned in the safety requirements.

Formal verification is a method that is getting more and more acknowledgement in the railway industry as a method for verifying safety.

Formal Verification gets its main ideas and motivations from mathematics. This is very natural, since in mathematics it is common practice to investigate huge domains (often infinite) and prove properties about them. As far as argumentation goes, there is nothing more convincing than a mathematical proof: it is precise, unambiguous and covers 100% of the domain under investigation.

We at Prover have written a guide that describes the basic principles of Formal Verification and how it can be applied for safety verification for signaling systems.

You can download the guide here.