L’activité de preuve formelle système consiste à exprimer mathématiquement les propriétés globales par lesquelles la sécurité du système est garantie et à établir par preuve mathématique que ces propriétés sont assurées grâce aux propriétés locales des constituants du système.
Il suffit alors d’établir que les constituants garantissent leurs propriétés locales détaillées pour garantir la sécurité système grâce à l’assurance de cette preuve mathématique.
Le raisonnement de sécurité et sa preuve garantissent ainsi les systèmes ferroviaires. Une première, l’outil Atelier B de CLEARSY vient d’être certifié T2 suivant la norme Cenelec EN50129 pour effectuer cette preuve au niveau SIL4.
Cette démarche maintenant outillée avec l’Atelier B T2 EN50129 a été appliquée pour les CBTC du métro de New York (MTA) et de Paris (RATP), ainsi que pour le renouveau de la ligne Marseille Vintimille (SNCF, système ERTMS).