Formal verification of computerized interlocking systems at Jernbaneverket

During the development of computerized interlocking systems, conducted by Jernbaneverket (Norwegian National Rail) and ABB, Prover Technology was a partner providing formal verification services, using the powerful methods of Prover iLock Verifier.

A generic safety requirement specification for Norwegian interlocking systems was used. Prover Technology played a central role in the development of this specification, which is maintained in cooperation with Jernbaneverket and ABB.

The formal verification services utilized a two-step formal verification process for computerized interlocking systems:

• The functional specification is formally verified to ensure that it meets the safety requirements.

• The interlocking system software code is formally verified to ensure that it meets the specification.

Errors found by formal verification could be removed early in the process, saving significant development resources and improving quality. When all errors had been corrected, formal verification techniques were applied again to ensure the correctness of the software.

As part of these services, Prover Technology delivers software safety verification reports, which play a central role in the Technical Safety Report as part of the CENELEC Safety Cases for interlocking systems.