Formal Safety Verification for Bane NOR, Norway

In projects for Bane NOR’s Nordlandsbanen line, the Ganddal freight terminal and the double track Sandnes-Stavanger, Prover provided turnkey services for safety verification of interlocking software. The interlocking systems were supplied by ABB, and Prover performed projects on behalf of both Bane NOR and its supplier ABB. Prover played a central role in development of the generic safety requirement specification for Norwegian interlocking systems. This specification was maintained in cooperation with Bane NOR and ABB, and was used in a number of projects that applied a two-step process for safety verification of interlocking software using Prover iLock Verifier:

• The interlocking design is formally verified to satisfy the safety requirements.
• The interlocking software is formally verified to ensure that it implements the interlocking design.

By using this process, errors found by formal verification could be removed earlier in the process, saving development resources and improving quality. When all errors had been corrected, formal verification techniques were applied again to ensure the correctness of the final interlocking software for revenue service.