Processus de preuve formelle de la sécurité d’un système de signalisation

Le processus de réalisation d’une preuve formelle des raisonnements de sécurité pour un système de contrôle-commande de signalisation est constitué de deux étapes :

1. Phase 1 : Sur la base d’une analyse des spécifications du système, l’équipe construit une preuve mathématique démontrant que les principes de conception du système écartent systématiquement l’ensemble des risques identifiés. Toutes les hypothèses nécessaires à cette preuve sont clairement identifiées.
2. Phase 2 : L’équipe vérifie que chacune des hypothèses de la preuve a été prise en compte par les différents fournisseurs des sous-systèmes et par les procédures d’exploitation. Cette étape vise à garantir l’absence de problèmes de sécurité dans les spécifications des sous-systèmes et assure que le système final est exempt de problèmes de sécurité.

L’utilisation des mathématiques dans cette démarche renforce la confiance dans la sécurité du système. Les hypothèses caractérisant les propriétés attendues de chaque sous-système sont précisément formalisées, en explicitant rigoureusement les arguments techniques qui éliminent tous les risques identifiés (collision, déraillement, survitesse, etc.). Ces propriétés forment des exigences de sécurité pour la réalisation des sous-systèmes et des contraintes pour l’opérateur.

La collaboration étroite entre l’équipe formelle, la maîtrise d’ouvrage et les équipes d’ingénierie est essentielle tout au long du processus. Des échanges techniques réguliers permettent de construire une compréhension approfondie du système, et des ateliers de travail sont organisés pour partager raisonnements et les hypothèses. Cette collaboration garantit l’adéquation des hypothèses choisies.

En conclusion, la preuve formelle des raisonnements de sécurité permet d’augmenter considérablement la confiance dans la sécurité du système. La preuve repose sur un ensemble minimal d’hypothèses qu’il suffit de vérifier systématiquement pour écarter mathématiquement tout risque d’accident (collisions, survitesse, déraillement, etc.) Cette activité, réalisée en collaboration avec les parties prenantes, rend explicite et tangible les raisonnements de sécurité des équipes d’ingénierie système.

Ce processus, inventé par CLEARSY, est employé pour sécuriser les systèmes de signalisation sous la responsabilité des donneurs d’ordres RATP, SNCF et le métro de New York.