Why formal verification – Verifying safety requirements on railway systems (part 1/3)

The subject I am going to write about this time is not an easy one. I will try to explain why formal verification is good. In particular, why it is a good practice to use formal verification when verifying safety requirements on railway systems.

The verification problem

In order to make a convincing argument, I need to start from the beginning. It all begins with a system and some safety requirements that the system is supposed to satisfy. Let’s assume that the system is an interlocking. Now, the general problem is to provide a convincing argument proving that the interlocking actually fulfills the safety requirements; this can be called the *verification problem*.

Let’s think a bit about the verification problem. What is it that needs to be done? What we have is interlocking software and some safety requirements. In order to make things clearer, let’s assume that the software consists of a number of boolean variables. Some of these variables are inputs, some outputs, and some (probably the most) are internal or intermediate variables. An assignment of values to the variables then represents a potential state of the interlocking. And the collection of all such assignments represents the potential state space. Potential states are related by the interlocking in the sense that one potential state can be reached from another by executing the interlocking for one or more cycles. Also, some of the potential states correspond to assignments that occur during start-up. These are called initial states. Then the reachable states are the part of the potential state space that can be reached from the initial states. Most likely, this is just a small part of the potential state space.

What is a safety requirement?

In the context of the potential state space, what is a safety requirement? Well, a safety requirement is an event that is not supposed to happen. In the end, a safety requirement is one or several assignments of variables that the interlocking should not be able to realise. Hence, a safety requirement is a part of the potential state space that the interlocking never should reach. So the verification problem boils down to showing in a convincing way that the parts of the potential state space that represents the safety requirements does not contain any states that are reachable by the interlocking.

That doesn’t seem so hard does it?

Well, actually it is.

And the main reason is that the potential state space is huge.

In fact, if we only consider boolean variables,
this space contains 2^{number of variables} potential states.

If the interlocking contains 100 boolean variables, then the potential state space has
1 267 650 600 228 229 401 496 703 205 376 ~ 10^30 members!

As a comparison, the number of trees on Earth is estimated to be 3*10^12. And that is just for 100 variables, which would represent a very small interlocking.

It should be clear by now that no manual method can completely solve the verification problem. Also testing fails. To obtain full coverage with testing, one has to try all possible combinations of values of the input variables and then simulate the system in order to verify that no safety requirements are violated. But even with just a small number of input variables this is not feasible. If the number of input variables is 100, then to complete the testing in 1 year would require 4*10^22 test cases to be completed in each second.

So what is a solution to the verification problem?

I think you can guess…