CLEARSY entre dans le programme MISTRAL NG de SNCF Réseau. En effet, la société ATOS – en charge du développement et du déploiement du programme – a souhaité être accompagnée par CLEARSY pour la partie validation formelle des données qui paramètrent MISTRAL NG. MISTRAL NG est le futur outil de commande centralisée du réseau SNCF.
Dans la continuité du programme MISTRAL (Modules Informatiques de Signalisation, de TRransmission et d’ALarmes) initié en 1998, MISTRAL NG est le futur système de commande/contrôle centralisé de gestion de la circulation ferroviaire. L’outil informatique générique est en cours de développement, et sera paramétré et déployé sur sites par la société ATOS, spécialisée dans les services du numérique. Il permettra de regrouper la commande/contrôle des installations de signalisation (actuellement gérée par 1.500 postes d’aiguillage), et offrira aux agents circulation de SNCF Réseau un outil plus performant pour réguler les circulations dans des centres supervisés et coordonnés par un centre national. Le paramétrage d’un système MISTRAL NG déployé contient des milliers de données de signalisation (itinéraires, signaux, circuits de voie, aiguilles…), d’automatismes (pour gérer automatiquement la circulation des trains) et de topologie du site. Contractualisée par ATOS, CLEARSY doit automatiser, en utilisant les méthodes formelles, la vérification du paramétrage de l’outil informatique et accompagner les équipes de son client dans l’utilisation du logiciel de vérification du paramétrage.
La norme NF EN 50128:2011 impose la vérification de ce paramétrage. Pour atteindre ces objectifs de sécurité, CLEARSY s’appuie d’une part sur un outil informatique dédié et d’autre part, sur des règles de vérification développées en utilisant les méthodes formelles. « La validation basée sur les méthodes formelles propose une logique nouvelle, fondée sur les mathématiques, qui a pour avantage de lever toutes les ambiguïtés quant à l’interprétation des données et des propriétés qu’elles doivent respecter. Elle remplace avantageusement les méthodes traditionnelles de tests qui sont manuelles et donc fastidieuses et potentiellement incomplètes », précise Erwan Mottin qui dirige l’activité validation de données chez CLEARSY.
Editeur de l’Atelier B, CLEARSY utilise les méthodes formelles dans la conception de logiciels – méthodes particulièrement adaptées aux systèmes industriels à fortes contraintes de sûreté – depuis 2001. En 2005, CLEARSY a développé le 1er outil de validation formelle de données en réponse à une commande de la RATP, consciente de ce que cette méthode apporte de garanties en termes de sûreté de fonctionnement. Dans le sillage de la RATP, Alstom et Siemens adoptent l’approche formelle à son plus haut niveau d’exigences pour la validation des invariants ferroviaires de CBTC (Radio Communication Based Train Control). Et depuis 2011, c’est CLEARSY qui effectue la validation formelle des données du CBTC U400, déployé par Alstom dans le monde entier. Dans le projet MISTRAL NG, SNCF Réseau a impulsé l’utilisation des méthodes formelles. Le déploiement de la tête de série de MISTRAL NG est prévu en 2021.