The PMI L1 project consists of creating a process to check the computer signalling implemented on line 1, 3 bis and 11 of the Paris metro.
- CLIENT : RATP, AQL
- DATE : From November 2007 to today
- LOCATION : Line 1, 3bis et 11, Paris Metro
This process is based on a formal approach, and necessitated the development of a proof workshop adapted to the Thalès RSS computerised signal boxes (PMI). This workshop has been constructed around the Prover iLock Verifier proof engine by Prover Technology and certified with CENELEC SIL4 software security.
Trials have been carried out on the PMI data from lines 11 and 3 bis of the Parisian metro. This workshop is currently used within the framework of the PMI L1 project for checking certain security properties on the PMI, which will soon be installed on line 1 of the Paris metro.
Our actions
CLEARSY has contributed to the SIL4 evaluation of the tooling making up the Prover iLock proof workshop – PMI. CLEARSY has also participated in the modelling and the proof of certain safety properties on the PMI of lines 11, 3 bis and 1.
Indeed, CLEARSY has participated in the verification of proof carried out by Thalès RSS on the PMI of line 1. We are continuing to assist the RATP in verifying the proof of Thalès RSS and for the proof of certain properties within the context of the PMI L1 project.-.
Link to this référence
