CLEARSY validates the data that parameterize its railway interlocking system because of the infallibility of its approach based on formal methods.
One major company entrusted CLEARSY with the data validation for the control system of switch points, i.e. the interlocking system. The aim is SIL4 certification, the highest safety level of the CENELEC EN 50128 standard. The interlocking solution proposed by the company being generic, it requires configuration. Rigorous validation of the parameterization data is one of the aspects required by the certification.
“Validation based on formal methods proposes a new logic, based on mathematics, which has the advantage of removing all ambiguities regarding the interpretation of the data and the properties they must respect”, states Erwan Mottin who heads the data validation activity at CLEARSY. In other words, formal validation ensures that the parameter settings comply with the levels of operational safety required by the standard. To achieve these safety objectives, CLEARSY relies on the one hand on a certified IT tool – the CLEARSY Data Solver – and on the other hand on verification rules developed using formal methods.
Publisher of Atelier B since 2001, CLEARSY developed the 1st formal data validation tool in 2005 in response to an order from the RATP. Since then, ATOS, SNCF, Siemens, Alstom, and Thales have used its services. Within the framework of this new contract, CLEARSY will prepare the necessary tooling