Formal verification of computerized interlocking systems at RATP

RATP (Régie Autonome des Transports Parisiens) replaced several of its existing relay-based interlocking systems with computerized interlocking systems supplied by Thales (called 'PMI systems' by RATP).

Prover Technology´s Prover Certifier product was used for formal safety verification of the non-derailing and non-collision safety properties that the PMI systems must satisfy. The formal verification solution for PMI includes:

• Formalization of the execution semantics of PMI systems.

• Automatic modeling of Specific Applications of PMI systems.

• Automatic instantiation of generic safety requirements for Specific Applications of PMI systems.

• The Prover Certifier product for formal verification.

The Prover Certifier for PMI has been CENELEC SIL 4-qualified by RATP, and the solution can be used as the main safety verification activity for the system´s logic, i.e. replacing the majority of the expensive and time-consuming testing effort usually devoted to this task. To allow this replacement, Prover Certifier must be guaranteed to never incorrectly report a property as proved. This is safe-guarded against using diversified modeling of the PMI system logic, and independent proof generation and proof checking mechanisms in the Prover Certifier software, documented and assessed by an independent body.

The first application of the verification solution for PMI was applied at RATP in 2009.