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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

The Successful Use of the B Method in Industrial Development of Critical Systems: Standards Compliance and Certification in CBTC

  • Dalay Almeida,
  • Thierry Lecomte

摘要

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.