Cut on-site testing time by up to 50% using formal verification

In the space between system development and deployment, there are a number of inconvenient and costly delays that can occur in a typical rail control project. Many of which can be attributed to the necessary phase of on-site testing.

Perhaps most challenging are so-called brownfield projects, where a system upgrade must be implemented on a line that is already in operation. Carrying out on-site testing under this circumstance impacts traffic operations and requires a ton of procedures, people, and administrative steps. In some cases, the on-site tests are even risky from a safety perspective.

Thankfully, there is a solution suppliers and infrastructure managers can implement to keep testing-related deployment delays to a minimum. Formal verification ensures that more potential failures are identified earlier in the system development process and, as a result, significantly reduces the amount of time required for on-site testing.

Keep reading to learn more about formal verification, and how it can help reduce on-site testing time by up to 50%.

What is formal verification?

Formal methods have been used in production for rail control for over twenty years. At Prover, our way of applying formal methods is through a set of automation tools and processes called Signaling Design Automation (SDA), which we use to enable the development of specifications, digital twins, and actual systems. The basic idea is that SDA instantiates the generic principles for a particular configuration and produces the system’s design and software code. SDA also performs safety verification to produce safety evidence and automated testing to create a test report— this is where Formal Verification comes in.

Formal verification is a technique for checking that systems fulfill selected properties with 100% certainty. It is part of our SDA process, where formal methods are applied at three levels:

Formal specification: Formalizes system requirements by expressing them in a formal language with a precise and unambiguously defined syntax and semantics.

Formal development: Utilizes formal methods as an integrated part of a tool-supported system development process– this is where you write your system using formal methods.

> Formal verification: Utilizes a software tool to prove properties of a formal specification, or that a formal model (aka digital twin) of a system implementation satisfies its specification.

While it is most advantageous to use all levels of the SDA process, it is not necessary. Formal Verification can be applied to any system post-development to ensure a more complete verification.

Formal verification helps you build a safer system

In 2015, a TGV train derailed in France while safety tests were being performed in preparation for opening the high-speed line for commercial service. As the train accelerated beyond speed limits, the system failed to react effectively and activate speed control. The accident cost 11 lives and injured 42 others in what would become known as the most fatal derailment in the history of the TGV. This example is a reminder of how dangerous on-site testing can be.

The truth is that traditional testing methods for big systems can never reach full coverage, and certain scenarios cannot be reproduced easily in the field. However, by using Formal verification with a formal model of the system, all scenarios—both possible and the seemingly impossible—can be exhaustively explored, thereby reducing the need for dangerous tests to be run in real life. Due to the vast number of combinations tested, Formal Verification provides full certainty. It uses a mathematical argument without gaps.

For examples of how Formal verification has been used to detect critical safety issues that would have otherwise been overlooked, we recommend reading “3 scenarios where formal verification caught errors missed by traditional rail control system tests.”

Formal verification drastically reduces on-site testing time

Formal verification not only helps improve the safety and quality of systems, but it addresses the prevailing need among system suppliers and infrastructure managers to reduce testing and commissioning time. Through our experience supporting numerous rail control projects over the years, we’ve seen an average time reduction ranging from 30 to 50%.

Such a drastic reduction can be attributed to formal verification’s ability to identify safety or functional issues through its larger coverage. Because a lot of tests are covered with Formal Verification, bugs and issues are discovered much earlier in the life cycle– already before going into the field for testing. In the big picture of the project timeline, the gap between system development and actual deployment becomes a lot smaller.

If you would like to learn more about formal verification and how it can help you build safer and more quality systems with minimal on-site testing, we invite you to read about our line of formal verification products. Ready to discuss how formal verification can be applied to your specific rail control project? Feel free to book a meeting with us.