Why formal verification – The suitability of formal verification (part 2/3)

Hopefully you have read part 1 on this blog, where I tried to convince you that traditional methods will not get you very far when verifying safety requirements for railway interlockings.

This time my task is to convince you that formal verification will get you far. In fact, all the way.

So what is formal verification?

Well, we already know what verification means. The ‘formal’ part means ‘mathematical’. Thus, formal verification means that the verification problem is made into a mathematical problem. And since we enter the realm of mathematics, all the rigour and precision that comes with mathematics are available to us.

The typical activity in mathematics is to make statements and then prove that they are true. Sounds familiar? And the proof of a mathematical statement has to be so convincing, so airtight, that any person with the proper education should agree that the statement actually is true. Of course, in practice the last part can be hard to achieve. Some parts of mathematics are notoriously difficult to understand even with a proper education. But let’s consider a classic example from arithmetic. The statement I am thinking about is as follows:

1 + 2 + … + n = n(n+1)/2.

In my mind, the most elegant way to prove this goes as follows. Write down the sum on the lefthand side twice, one under the other.

1 + 2 + … + n
n + (n-1) + … + 1

Note that the order of the terms is reversed in the lower sum. Now here comes the trick: if we look at the columns in this expression, each column has the sum n+1. And there are n columns. Hence, the sum of all these numbers is n(n+1). What we have then is

2(1 + 2 + … + n) = n(n+1),

which means that

1 + 2 + … + n = n(n+1)/2.

Isn’t that a convincing argumentation?

With this example, I have tried to show you how a mathematical proof can be done and hopefully you agree that, when properly done, mathematical proofs are airtight. In fact, they are the only airtight form of proofs known. As we noted in part 1, the major snag with the verification problem is the huge size of the potential state space. Mathematics provides solutions to this as well, since all domains handled are huge, often infinite.

It turns out that I only got halfway through my aspiration to convince you about the suitability of formal verification. So please wait until the next post.