System level proofs for the CBTC of the New York Flushing line has been presented on June 26th 2013 in Paris. The aim of this presentation 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.
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).