Use of Certified Industrial Tools for Formal Analysis and Monitoring of Communications-Based Train Control Systems
摘要
The B method has long been employed in the development of Communications-Based Train Control (CBTC) systems, providing strong traceability from requirements and system design to implementation, as well as mathematical guarantees that the system meets its safety requirements. However, integration and system testing are typically performed using a distinct environment, which weakens the traceability between requirements and test scripts compared to the traceability with the code. Additionally, once deployed, CBTC systems could benefit from continuous functional monitoring to further enhance safety, not only by verifying compliance with formal specifications, but also by identifying possible issues arising from human actions or material failures. In previous work, we proposed a methodology for analyzing and monitoring relay-based Railway Interlocking Systems using the certified tools of the CLEARSY Safety Platform (CSSP). In this paper, we extend that methodology to support computer-based railway systems, with a particular focus on CBTC. Our approach introduces a formally defined runtime monitor that can be integrated into the testing, and operational phases of the system lifecycle. This monitor acts as a safety layer that reinforces test campaigns and continues to check key system properties after deployment. Although our method was applied to a real industrial case that cannot be fully disclosed, we present a representative case study to demonstrate its feasibility and benefits in realistic scenarios.