3 scenarios where formal verification caught errors missed by traditional rail control system tests

As most signal and verification engineers know, when developing and verifying software for rail control systems, testing can be very tricky. Especially when it comes to finding corner cases and scenarios outside of normal operations.

When conducting a test, you typically define a test case as well as the circumstances in which you are testing your software. The problem is, when you do it that way, you’re thinking as a human. This means that, sometimes, you forget things or fail to consider the possibility that certain scenarios could even happen.

Of course, if you’ve done your work correctly, the risk of errors slipping through and actually causing an accident is very small. Field testing and simulation methods offer a lot of benefits. However, when it comes to identifying those hard-to-pinpoint cases, there is nothing like formal verification. When you perform formal verification, every possible case is considered—helping you keep even the few, otherwise overlooked, errors from slipping through and prevent accidents from happening.

What is formal verification?

Formal verification is a technique for checking that systems fulfill selected properties with 100% certainty. For example, for a rail control system, it can be checked that signals cannot display green aspects unless certain switches are in correspondence.

While testing of big systems can never reach full coverage, due to the number of combinations that have to be tested, formal verification provides full certainty because it uses a mathematical argument without gaps.

Run all possible scenarios with model-checker analysis

One of the great advantages of formal verification is the completeness of the model-checker analysis. Contrary to testing, the model-checker checks all possible sequences of inputs on every part of the track. Modelling communications between subsystems and investigating delays in such communications can help spot scenarios that would otherwise be difficult to stumble upon using traditional testing methods.

Working closely with our customers over the years, we have seen a number of issues revealed during formal verification which were not found by testing. In these cases, the conditions where the bugs appeared were difficult to reproduce in test environments, and it was not natural to even look for these kinds of bugs.

Here are three examples of scenarios discovered using formal verification that traditional test cases failed to find.

Scenario 1: Communication delays between two sub-systems

One scenario that formal verification often catches, which is nearly impossible to find using traditional testing methods, is one that appears due to communication delays between two sub-systems.

The challenge in finding such scenarios comes from the fact that both the sequence and communication delay may need to be very specific to lead to such cases. However, by using formal methods to model the communication between the different sub-systems, it is possible to spot these kinds of scenarios.

For example, the communication from A to B must be fast, the communication from B to A slow, and a specific command is received while a message is being sent from B to A. With formal proof, once the communication is modeled (e.g., max communication delay, cycle of forgiveness if no message received), the model-checker will cover every possible state to find a non-safe scenario. Once such a counter-example is found and captured, it is possible to reproduce the scenario using a simulator.

Scenario 2: Delays caused by sequences involving several trains

Scenarios involving a specific sequence of several trains are also often overlooked by traditional testing methods. Sometimes you establish configurations according to the first train, but fail to take into account the trains that come after it. The consequence is big delays.

For instance, a first train is moving to a closed level crossing and a second train is causing a particular sequence that allows the said level crossing to be opened. Such a scenario may be possible due to the level crossing’s particular configuration.

Scenario 3: Complex sequences and contexts

Another type of overlooked scenario often discovered via formal verification is one with a deeper sequence of events, which requires a very particular context or sequence in order to take place. At first normal behavior happens that sets a certain value in a given memory. Then that memorized state reveals unsafe scenarios in a nominal case, which is induced by the particular context.

For instance, a certain route 1-3 can be formed without any issues, but if it is formed after the route 1-2 has been formed and destroyed, the route can be formed while a switch within its perimeter is being commanded.

In addition to that, there are also certain counter-examples that can be caused by quick state changes. These too can be tricky to uncover during testing. A switch position change for a single cycle can cause a signal to open while a conflicting one may take a bit more time to close, causing a risk of collision.

Questions?

We invite you to read about our line of formal verification products. And if you would like to discuss how these can be applied to your specific rail control project, please feel free to book a meeting with us.