Following our post “Event-B to demonstrate metro safety in New York“, a presentation of
the final results of the project have been presented in Paris on June 26th.
ClearSy has developed a system formal verification for the CBTC of New York subway line 7 (Flushing), using the B method. The obtained formal system verification is an element for the safety assessment of this critical railway system.
New York City Transit (NYCT) has awarded THALES Toronto for the design and fitting of this CBTC (awarded in 2010, revenue service in 2016). This CBTC system is composed of an on-board computer fitted in renewed R142 cars and of filed and office equipment (zone controllers and central supervision). It interfaces to the existing interlocking system, adapted with specific modifications.
NYCT has decided to obtain a mathematical proof-based safety guaranty for the Flushing new CBTC. To achieve this system formal verification, ClearSy conducted a system level proof based on the B formal language and the Atelier B toolkit. The proven target properties are:
- Impossibility of collision between trains
- Impossibility of derailment over an unlocked switch
- Impossibility of over-speeding.
Now all the proof development is finished and all assumptions are pre-validated (by THALES and NYCT experts).
The goal of this meeting is to give the participants an insight of what has been done in this system level proved, what methods have been used, and what are the results and their practical usage.