The American company Battelle (Columbus, Ohio) chose CLEARSY to intervene in the interoperable automation project of New York Metro (Culver test track) in the continuity of the Flushing line.
Battelle is an Independent Safety Assessor (ISA) for the railway safety of Flushing and Culver projects. These projects aim to equip the lines with CBTC systems (Communication-Based Train Control), to safely improve underground traffic.
For the Flushing line CLEARSY completed the formal modeling of the system by using the B method, a method of construction, based on the B language, refinement, and mathematical proof.
Modeling was used to determine the safety conditions of the system and to obtain the necessary document detailing the checkpoints before authorizing system commissioning.
This methodology and this knowledge will be used in the Culver project for complete modeling of the safety conditions required in the generic specification of New York future CBTCs (Interoperability Interface Specification). These elements should allow the implementation of CBTC involving diverse suppliers, while ensuring safety. Let’s recall that the B method is used in the railway domain to create safety critical software for automatic train control.