RATP, Paris

Dans le cadre de ce projet, Prover a collaboré avec la RATP pour créer une solution de vérification formelle répondant à la demande de la RATP en matière de vérification de la sécurité du logiciel des enclenchements. La RATP avait sélectionné un système d’enclenchement informatisé de Thales pour plusieurs lignes de métro et souhaitait vérifier la sécurité du logiciel de l’enclenchement en utilisant une preuve formelle, selon un processus conforme à la norme CENELEC EN 50128. La solution mise en place reposait sur:

• Des exigences de sécurité génériques et formelles, basées sur les propriétés de non-collision et de non-déraillement

• Un modèle d’environnement, modélisant le comportement des trains, et utilisé dans la vérification de la sécurité

• Un outil de vérification basé sur Prover Certifier, fournissant la preuve, formelle et indépendante, que le logiciel de l’enclenchement, et son image binaire compilée, répondent aux exigences de sécurité.

La solution a d’abord été évaluée, dans le cadre du projet PMI de la ligne 3bis en 2009, en parallèle de l’effort de test traditionnel. Depuis lors, la solution est entrée en production pour les systèmes d’enclenchements, par exemple : ligne 12 sud (2010), ligne 8 (2011), ligne 12 nord (2012) et ligne 1 (2013).