Le projet PMI L1 consiste à créer un processus de vérification des enclenchements informatiques mis en œuvre sur la ligne 1, 3 bis et 11 du métro de Paris.
- CLIENT : RATP, AQL
- DATE DU PROJET : De Novembre 2007 à nos jours
- LIEU : Line 1, 3bis et 11, Métro de Paris
Ce processus, se base sur une approche formelle, et a nécessité le développement d’un atelier de preuve adapté pour les postes de manœuvre informatisés (PMI) de Thalès RSS. Cet atelier a été construit autour du moteur de preuve Prover iLock Verifier de Prover Technology et certifié au niveau de sécurité logicielle CENELEC SIL4.
Les essais ont été effectués sur les données des PMI des lignes 11 et 3 bis du métro parisien. Cet atelier est utilisé actuellement dans le cadre du projet PMI L1 pour la vérification de certaines propriétés de sécurité sur les PMI qui seront prochainement installés sur la ligne 1 du métro de Paris.
Nos actions
CLEARSY a contribué à l’évaluation SIL4 des outils composant l’atelier de preuve Prover iLock – PMI. CLEARSY a également participé à la modélisation et à la preuve de certaines propriétés de sécurité sur les PMI des lignes 11, 3bis et 1.
Par ailleurs, CLEARSY a participé à la vérification des preuves effectuées par Thalès RSS sur les PMI de la ligne 1. Nous continuons à assister la RATP pour la vérification des preuves de Thalès RSS et pour la preuve de certaines propriétés dans le cadre du projet PMI L1.
Liées à cet référence
