RATP, Paris

Automated Sign-off Safety Verification compliant with CENELEC EN 50128

Purpose

Establish automated sign-off safety verification based on mathematical proof, in a process compliant with CENELEC EN 50128.

Infrastructure Manager

RATP (Paris Metro)

Signaling system

Computerized interlocking systems based on the PMI platform by Thales

In this project Prover Technology collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized interlocking by Thales for several metro lines, and wanted to establish the safety of the interlocking software using formal proof, in a process compliant with CENELEC EN 50128. The solution established was based on:

Generic, formal safety requirements, based on non-collision and non-derailment properties

An environment model for train behavior, taken into account in the safety verification

A sign-off safety verification tool based on Prover Certifier, providing independent formal proof that the interlocking software, including its compiled, binary image, meets the safety requirements.

The solution was first evaluated in parallel with a traditional testing effort within the PMI line 3bis project in 2009. Since then, the solution has entered production use for interlocking systems on e.g. Line 12 South (2010), Line 8 (2011), Line 12 North (2012) and line 1 (2013).