CLEARSY carries out the formal validation of data from SNCF Réseau's MISTRAL NG program

Following on from the MISTRAL programme (Modules Informatiques de Signalisation, de TRransmission et d'ALarmes) initiated in 1998, MISTRAL NG is the future centralized command and control system for rail traffic management. The generic IT tool is under development, and will be configured and deployed on site by ATOS, a company specialized in digital services. It will make it possible to group together the control of signalling installations (currently managed by 1,500 switching installations), and will offer SNCF Réseau traffic agents a more efficient tool to regulate traffic in centres supervised and coordinated by a national centre. The configuration of a deployed MISTRAL NG system contains thousands of signalling data (routes, signals, track circuits, switches, etc.), automation data (to automatically manage train traffic) and site topology. Contracted by ATOS, CLEARSY must automate, using formal methods, the verification of the configuration of the IT tool and support its client's teams in the use of the configuration verification software.
 

The NF EN 50128:2011 standard requires this parameter setting to be verified. To achieve these safety objectives, CLEARSY relies on a dedicated IT tool and on verification rules developed using formal methods. "Validation based on formal methods proposes a new logic, based on mathematics, which has the advantage of removing all ambiguities regarding the interpretation of data and the properties they must respect. It replaces the traditional testing methods, which are manual and therefore tedious and potentially incomplete", says Erwan Mottin, who manages the data validation activity at CLEARSY.

Publisher of Atelier B, CLEARSY has been using formal methods in software design - methods particularly adapted to industrial systems with high safety constraints - since 2001. In 2005, CLEARSY developed the first formal data validation tool in response to an order from RATP, aware that this method provides guarantees in terms of operational safety. In the wake of RATP, Alstom and Siemens are adopting the formal approach to its highest level of requirements for the validation of CBTC (Radio Communication Based Train Control) railway invariants. And since 2011, CLEARSY has been carrying out the formal validation of the data of CBTC U400, deployed by Alstom worldwide. In the MISTRAL NG project, SNCF Réseau has promoted the use of formal methods. The deployment of the MISTRAL NG production head is planned for 2021.

More informations : www.clearsy.com/en/