B in Large-Scale Projects: The Canarsie Line CBTC Experience

Abstract

Eight years ago, Siemens Transportation Systems accomplished the first successful application of the B Method on an industrial project. The vital software of the METEOR automatic train control system, with very strong dependability and safety needs, was specified and coded in B. Beyond the technological challenge of using such a complex formal method in an industrial context, it is now clear for us that building software using B is not more expensive than using conventional methods. Better, due to our experience in using this method, we can assert that using B is cheaper when considering the whole development process (from specification to validation and sometimes certification). Since METEOR, Siemens Transportation Systems has generalized the use of B for building all vital software of its systems in particular its Communication Based Train Control Systems (CBTC) recently enacted on the New York City Canarsie Line. This short paper shares the Canarsie line experience in the B landscape.