L’utilisation de la preuve formelle système pour garantir le nouveau CBTC de la ligne 7 (Flushing) de New York a été présentée à l’occasion d’une conférence qui s’est tenue le mercredi 26 juin 2013 à Paris. L’objectif de cette présentation est d’offrir aux auditeurs une vision de ce qui a été fait dans cette preuve formelle système, de quelles méthodes ont été employées, et de quels sont les résultats et leur usage en pratique.
CLEARSY a procédé à la vérification au niveau système du CBTC de la ligne 7 (Flushing) du métro de New York, en utilisant la méthode B. La preuve formelle obtenue est intégrée au dossier de sécurité de ce système ferroviaire critique.
New York City Transit (NYCT) a confié à THALES Toronto la conception, le développement et l’installation de ce CBTC (depuis 2010, mise en service en 2016). Le système est composé de calculateurs embarqués dans une version modifiée du matériel roulant R142, ainsi que de calculateurs sol (contrôleurs de zone, supervision centrale). Il s’interface sur l’interlocking existant, lequel a subi des adaptations spécifiques.
NYCT a voulu obtenir une garantie basée sur des preuves mathématiques pour le nouveau CBTC de Flushing. Dans ce but, CLEARSY a procédé à une preuve formelle au niveau système avec le langage formel B et l’outil Atelier B. Les propriétés systèmes cibles ainsi démontrées sont les suivantes :
- Impossibilité de collision entre trains ;
- Impossibilité de déraillement sur une aiguille mal positionnée ;
- Impossibilité de sur-vitesse.
A présent, la preuve de ces propriétés a été établie et les hypothèses utilisées ont été pré-validées avec les experts de THALES et de NYCT.