@inproceedings{14bb79bdd28e4a269d0515e081287f20,
title = "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.",
keywords = "Environment modelling, Formal verification, Interlocking application, Proof certification",
author = "S. Behnia and A. Mammar and Mota, \{J. M.\} and N. Breton and P. Caspi and P. Raymond",
year = "2008",
month = dec,
day = "1",
doi = "10.2495/CR080151",
language = "English",
isbn = "9781845641269",
series = "WIT Transactions on the Built Environment",
pages = "143--152",
booktitle = "Computer System Design and Operation in the Railway and Other Transit Systems - Computers in Railways XI",
note = "11th International Conference on Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2008 ; Conference date: 15-09-2008 Through 17-09-2008",
}