The Successful Use of the B Method in Industrial Development of Critical Systems: Standards Compliance and Certification in CBTC
摘要
The B Method has become one of the most successful formal approaches for the development of safety-critical railway software. Initially received with skepticism due to perceived costs and complexity, its industrial relevance was firmly established through milestones such as the use of the B language for the verification of SACEM and the application of the full B Method in the METEOR metro project in Paris. More recently, its widespread adoption in Communication-Based Train Control (CBTC) systems has reinforced its role in the railway industry. Its success is closely linked to the method’s ability to support compliance with industrial standards, in particular EN 50128, by contributing to verification, validation, proof, testing, and maintenance activities. This paper examines the factors that have enabled the successful industrial application of the B Method, offering an experience-based account of how it is applied to meet certification requirements in CBTC development. While respecting industrial confidentiality, the discussion is illustrated with simplified examples that highlight key aspects of the methodology and its alignment with safety standards.