Prover Technology

Interlocking Design Automation (IDeA) is a new concept that helps clients to overcome the challenges in meeting infrastructure manager expectations regarding the delivery of modern rail control interlocking systems, and the cost of change problem.

Formal methods to cut cost and increase safety on railway signalling systems

Railway signalling systems are surprisingly expensive to produce. Formal methods have emerged as a way to cut costs and increase safety at the same time.

Today, there are proof engines that can formally verify the safety requirements for a railway interlocking system in a few minutes using an average laptop computer. Time-consuming and incomplete safety testing can be replaced by mathematical proofs that, for a fraction of the previous cost, can provide 100% coverage. This approach requires high-quality specifications that must be formalised in a mathematically precise formal language, so that proof engines understand exactly what they are supposed to prove.

Formal verification is now strongly recommended by safety standards organisations such as CENELEC. Several leading railway infrastructure managers, such as Paris Metro, Swedish National Rail, Norwegian National Rail and New York City Transit, require formal verification as part of their safety assessments. The reason: formal verification increases safety and quality, and provides more efficient processes for otherwise costly and time-consuming safety testing.