Paris, June 26th: System level formal proofs for the CBTC of the New York Flushing line

This meeting has taken place…

Many thanks to all the people who could come!

The slides are now available here:

Conference slides: BFlushing26_en

When:        Wednesday June 26th, 14h to 17h

Location:    Paris, Club Confair – 54 rue Laffitte

Presentation in English, slides in English and French

  • System level formal proof: what is it, target properties and assumptions
  • The main target properties in our case, ensuring no collision and no derailment
  • Global description of the top level proof, assumptions about the interlocking
  • Global description of the position / speed determination proof
  • Global description of the safe braking proof
  • Methods and organization with the designers
  • Costs and duration
  • Deliverables and their usage
  • Conclusion / discussion

Appetizers and drinks served at 17h.

Please visit our web page: NYCT formal proof page.


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.


Comments are closed.