Railway services

PMI L1


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.

Process for formally checking the computer signalling implemented on line 1, 3 bis and 11 of the Paris metro


Client


> CLIENT : RATP, AQL
> DATE : From November 2007 to today
> LOCATION : Line 1, Paris Metro

Project context


> 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.

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.-.