Author(s)

S. Behnia, A. Mammar, J.-M. Mota, N. Breton, P. Caspi & P. Raymond

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 Metro’s line 3Bis. These high-level properties have first been refined to an intermediate level permitting their expression in terms of the control system’s inputs and outputs. The resulting properties have then been formalised in the Prover iLock Verifier engine’s 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. Keywords: formal verification, interlocking application, proof certification, environment modelling. 1 Introduction Interlocking systems are safety critical systems and thus require thorough validation before being set into operation. Usually, this validation is performed by means of testing and even though the experience of several decades shows that intensive testing is a very safe approach, it is also very expensive: the experience of RATP,

Keywords

formal verification, interlocking application, proof certification, environment modelling.