Extension of Line 14 of the Paris Metro: over 25 years of reliability thanks to the B formal method

26 June 2024

Thanks to the B method, Meteor kept its promise” … “I’d never seen anything like it: the software was almost perfect the first time”. – Claude Hennebert, RATP, Delegate to the DGA, Lettre B No3, April 98

On the occasion of the recent extension of line 14 of the Paris metro, a fully automatic driverless line, CLEARSY is proud to point out that the automatic train control software, initially developed using the B formal method, continues to guarantee the safety and reliability of this critical system.

The continued success of PARIS Line 14, thanks to the B method, demonstrates that formal methods are not only effective but also sustainable for critical systems.

Atelier B is the tool developed and distributed by CLEARSY since 1993 to support the B method, develop proven critical software and demonstrate system safety through mathematical proof.

The Atelier B tool would not have been developed without the RATP, which wanted a breakthrough innovation for the development of the METEOR metro (L14) by Siemens Mobility France (formerly Matra Transport). CLEARSY industrialized ALSTOM’s original tool; the close collaboration between RATP, ALSTOM, SIEMENS, INRETS (now IFSTTAR) and CLEARSY made this level of excellence possible.