Industrialising a proof-based verification approach of computerised interlocking systems

Abstract

This paper describes the formal verification of an interlocking system.We have formally proved the non-derailing and non-collision safety properties for an existing interlocking system operating on Paris Metros line 3Bis. These high-level properties have first been refined to an intermediate level permitting their expression in terms of the control systems inputs and outputs. The resulting properties have then been formalised in the Prover iLock Verifier engines internal language. The Prover iLock Verifier engine is a COTS commercialised by Prover Technology. For this project some specific features have been added to the engine to provide certified proofs that can be used, instead of testing, in the SIL-4 qualification process of interlocking systems.