ABSTRACT. Model checking techniques applied to the verification of railway interlocking systems may fail to scale. Compositional methods have been proposed to reduce the size of networks to be model checked. In this paper we extend the scope of a previously defined compositional method to systems employing flank protection, not allowed in the original method due to the fact that flank protection requires a coordination of distant points. The extension comprises soundness and completeness results for this new context and a decomposition strategy able to divide a network into subnetworks of minimal size.

ABSTRACT. Upgrading rail network infrastructure involves complex system design decisions that can be informed by robust models. Ideally, the modelling techniques support formal analysis, e.g., of safety, security, resilience, and performance, the models are extensible, and they are accessible to both railway engineers and policy makers.

We propose using bigraphs---a diagrammatic formal model with user-defined entities and rewrite rules---as a visual and intuitive approach to extensible railway system modelling. An example is presented: electrification rollout and the adoption of battery-powered trains that includes the impact of (probabilistic) power blackouts and supports system-level optimisation, e.g., selecting which track segments to electrify, without resorting to constraint programming languages. Formal analysis via model checking is used throughout.

This work represents a shift in the use of formal methods in railway engineering: from verifying isolated components such as signalling, to supporting formal, system-level design and decision-making.

ABSTRACT. Ensuring the correctness of control logic in railway systems is essential for safety and reliability. In this paper, we present an industrial case study on the formal verification of a software component responsible for managing signal color aspects in a railway interlocking system. We work within AIDA, a model-based design environment where generic control logics are specified in a controlled natural language, and which then drives the automatic generation of SysML models and executable code. In the first phase, we followed an approach based on the use of the Dafny prover, analyzing the model automatically generated from AIDA. This model includes both the Dafny counterpart of the control logic, as well as its annotations. When Dafny failed to prove the expected properties, manual inspection highlighted the existence of some corner cases, that led to the discovery of actual bugs. After revising the logic, Dafny still failed to prove the overall correctness. Hence, we replaced manual inspection with the model checking of a carefully reduced model, obtained by localization reduction and focusing on the most relevant classes and havoc-ing the behavior of the others. The model was derived from the summarizations of the methods in Dafny, and could be fully analyzed with the nuXmv model checker. The subsequent automated analysis was able to detect additional violations, and to pinpoint them in the form of easy-to-understand counterexample traces (instead of returning a failed to prove answer).

ABSTRACT. 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.