In order to analyse the safety of control system for the automatic lines 3 and 5 of Paris subway, CLEARSY has proceeded through event B method. The same method was employed previously for New-York subway.
Octys is a solution for automatic control of the railway traffic deployed by RATP on lines 3 and 5 of Paris subway. Like any CBTC (Communication Based Train System), Octys must guarantee a maximum-safety level (SIL4). Among others, it might be able to avoid any collision or derailment risks whatever may occur on subway lines (failures, signalisation, power supply, etc..). The subject-matter of the contract signed between CLEARSY and RATP was to prove formally the safety aspect of Octys through mathematical demonstration.
For RATP, the fabrication of different Octys components should be achievable by different manufacturers, especially when it goes about such components as on-board and trackside. The consequence is that the global system safety doesn’t result from finished products. Because the guarantee of the assembly safety of different CBTC components, notably on-board and trackside, is a cross-systems specification examined by CLEARSY. Formal methods engineer at CLEARSY Julien Molinero explains: “We had to guarantee by proof, that when the specifications are met in a proper way by the subsystems then on-board/trackside assembly is safe”. First, the system is described as a group of all elements that could evolve according to all specified events. Then it is necessary to communicate in mathematical language (formal B language) the required properties (non-collision, non-derailment) and to prove mathematically that the properties are conserved at any time. Otherwise, it is necessary to review the work by introducing more in detail the properties that the systems must respect.
If the approach method remains innovative it means that its efficiency has been proved. CLEARSY has already demonstrated in the past that its ability to prove formally a complex system safety. Julien Molinero mentions: « We have already carried out a similar project on New-York subway and managed to prove beyond doubt the CBTC safety implemented by the New York City Transit responsible for public transportation in New York.” To date, CLEARSY mission for RATP allowed to complete some specification aspects and to provide clear and precise argumentation approving the safety of Octys solution.