Pour analyser la sécurité du système de pilotage des lignes automatiques 3 et 5 du métro parisien ; CLEARSY a utilisé la méthode B événementielle. Comme précédemment pour le métro de New-York.
Octys est la solution de contrôle automatique du trafic ferroviaire déployée par la RATP sur les lignes 3 et 5 du métro parisien. Comme tout CBTC (Communication Based Train System), Octys doit garantir un niveau de sécurité maximum (SIL4). Il doit être capable notamment – quelques soient les événements (pannes, signalisation, alimentation…) se produisant sur les lignes – d’écarter tout risque de collision ou de déraillement. Prouver formellement par démonstration mathématique le caractère sécuritaire d’Octys : tel était l’objet du contrat signé entre CLEARSY et la RATP.
Pour la RATP, les différents éléments constitutifs d’Octys, et principalement le bord et le sol – doivent pouvoir être réalisés par des industriels différents. Conséquence : la sécurité du système global n’arrive pas de fait avec le produit fini. Car ce qui garantit la sécurité de l’assemblage entre les différents éléments du CBTC – le sol et le bord notamment – c’est la spécification inter-systèmes, spécification que CLEARSY a interrogée. Nous avons dû garantir par la preuve, que si les spécifications sont bien respectées par les sous-systèmes alors l’assemblage sol/bord est sécuritaire, explique Julien Molinero, ingénieur méthodes formelles chez CLEARSY. D’abord le système est décrit comme un ensemble d’éléments susceptibles d’évoluer selon un ensemble d’évènement spécifiés. Reste ensuite à exprimer en langage mathématique, le langage formel B, les propriétés désirées (non-collision, non-déraillement) et à prouver mathématiquement qu’à tout moment, les propriétés sont conservées. Dans le cas contraire il faut revoir sa copie en explicitant plus précisément les propriétés que doivent respecter les systèmes.
Si l’approche reste assez inédite, elle a prouvé son efficacité. CLEARSY a déjà démontré par le passé qu’elle était capable de prouver formellement la sécurité d’un système complexe : « Nous avons conduit un projet parfaitement similaire sur le métro de New York en prouvant formellement la sécurité du CBTC mis en place par la New York City Transit qui exploite le réseau new-yorkais » relève Julien Molinero. A ce jour, CLEARSY a permis de compléter certains aspects de la spécification et fourni un raisonnement clair et précis permettant de valider la sécurité de la solution Octys.