Using formal verification to eliminate software errors

The use of software in safety critical railway applications is increasing. Techniques for developing and running such software are based on reducing the probability of an error in the software causing an unsafe system failure; e.g. that the system permits a train to proceed when it shouldn´t. At the same time these techniques cause problems of the opposite nature; that the systems fail to allow trains to proceed even when it is safe to proceed. Such failures, although not directly dangerous, lead to stress and delayed traffic, which in turn can cause safety to be compromised. This paper shows how the use of formal verification can solve this problem. This technique can be used to find and eliminate all errors in the software, before the system is put into service. Formal verification is one of the corner stones of Prover iLock, an off-the-shelf commercial tool suite used for developing railway signalling applications.