This paper introduces a framework to ensure the semantic integrity of Control-Command and Signaling (CCS) design data, essential for reliable and efficient planning processes. Traditional XML Schema checks address syntax but fail to capture the complex logic required for CCS systems. To overcome this, we apply the Schematron standard to formally validate complex railway signaling rules. Our approach is to translate natural language constraints into semi-formal semantic rules that are implemented and tested. We extend Schematron with technology- and domain-specific features, such as data indexing and advanced error reporting. These innovations enable scalability for large datasets while producing clear, actionable reports for signaling engineers, safety assessors, and infrastructure managers. Applied to DB InfraGO’s PlanPro data format, our framework automates processes that improve data quality, reduce human error, and accelerate CCS planning. By supporting formal workflows, it strengthens safety assurance and regulatory compliance, addressing key challenges in the railway domain. Its integration into the “Werkzeugkoffer” toolkit demonstrates its practical value in tackling the complexities of modern railway control systems.
Autonomous Tram (AT) systems are an emerging application requiring mission critical services to ensure safe and continuous operation. Key functions such as positioning, track occupancy detection, and obstacle perception depend on uninterrupted communication and mobility support. Leveraging the capabilities of 5G networks is thus crucial to support these functions. In this paper, we investigate the applicability of 5G Ultra-Reliable Low Latency Communications (URLLC) services for AT use case, with a particular focus on mobility challenges. We begin by conducting a comprehensive 5G coverage analysis in a real urban deployment to identify limitations in handover (HO) performance, which may compromise service reliability and, consequently, the accuracy and timeliness of positioning and perception functions. To address this, we propose a 5G Dual Connectivity Handover (DC HO), offering seamless transitions compared to classical 4G-based HO solutions. The proposed HO mechanism is validated through extensive simulations, comparing key performance metrics such as latency and reliability against classical 4G HO approach. Results demonstrate that the 5G DC HO strategy meets the stringent requirements of URLLC, thus enabling reliable support for AT operations in dynamic environments and safeguarding the critical services of positioning, track management, and environment perception.
Machine learning (ML) offers promising capabilities for predicting rail infrastructure failure and enabling a shift from diagnostic to prognostic railway maintenance. However, the real-world adoption of high-performing ML models in safety-critical domains such as railway systems hinges on their trustworthiness, particularly their interpretability and transparency. This study, based on a case study in track geometry management, explores the trade-off between accuracy and interpretability in predicting track alignment failures by comparing six ML classifiers: Logistic Regression, Random Forest, Gradient Boosting, XGBoost, Support Vector Machine (SVM), and a Neural Network (NN). The models were trained on railway defect datasets using features such as operating speed, train traffic, total gross tonnage, and defect length. Performance was evaluated using recall as the primary metric, given the high cost of false negatives in rail safety contexts. Results showed that SVM and NN models achieved the highest recall (0.704 and 0.734, respectively), but at the cost of lower interpretability. To address this, post-hoc Explainable AI (XAI) techniques, including SHAP and LIME, were applied. These methods collectively enhance both local and global interpretability and support model transparency, stakeholder trust, and the bridging of the gap between predictive performance and decision-making needs. While XAI is increasingly applied in other sectors, its use in asset management and particularly railway predictive maintenance remains limited. This work fills that gap by demonstrating how XAI can foster more informed and confident adoption of ML models in rail infrastructure management. These explainability techniques help domain experts and end users understand why a model produced a specific result and what key factors influenced that decision, while also supporting data scientists and developers in refining model performance. For instance, feature refinement guided by SHAP improved SVM recall from 0.704 to 0.716.
Autonomous rail systems, including driverless trams, are gaining traction due to their potential to enhance efficiency, capacity, and operational cost-effectiveness. A central requirement for safe operation of autonomous tram vehicles is achieving ultra-reliable positioning accuracy, which traditionally relies on costly, infrastructure-heavy solutions like trackside beacons or GPS, alongside sensor fusion algorithms that often fail to meet the stringent requirements of Safety Integrity Level 4 (SIL4). These limitations create a significant barrier to the widespread adoption of autonomous light rail systems. This paper introduces the Consistency Check and Best performance Selection (CCBS) algorithm, a novel fully onboard solution that enhances data reliability for rail positioning and velocity estimation systems. Our method validates and combines outputs from multiple sensors, leveraging a sophisticated consistency check and a data performance selection mechanism to achieve a SIL4 level – even when individual data streams do not. This entirely onboard approach significantly improves positioning and velocity estimation accuracy and offers substantial cost and maintenance efficiencies by eliminating the need for trackside infrastructure.
Virtual Coupling of Train Sets (VCTS) offers a promising way to boost railway capacity and flexibility, but it demands reliable, high-performance and safe wireless communication between trains and control centres, as well as between train sets. Current centralized systems like Euroradio are not suited for VCTS’s decentralized architecture, making a dedicated safety layer essential. This paper presents a Coloured Petri Net (CPN)-based framework to assess the reliability of Train-to-Train (T2T) communication, focusing on 5G NR V2X. After introducing VCTS architecture and dependability analysis methods, we detail our CPN model and performance metrics. Simulations reveal that higher message loss rates (MLR) significantly reduce reliability, highlighting the need for robust error handling. In the absence of VCTS-specific requirements for the wireless communication performance, we use automotive benchmarks (3GPP V2X, 5G AA) for evaluation. Under low MLR, the system meets these performance criteria.
Many application domains resolve to the use of synthetic test data motivated by privacy concerns and safety reasons, but also, on the positive side, due to cost and quality considerations. Genetic Algorithms have long been studied for graph optimisation, however, to the best of our knowledge, not for scheme plan generation. We present a new approach that automatically constructs scheme plans from a set of tiles. This transforms the scheme plan generation problem into a combinatorial optimisation process. The manual design of scheme plans is laborious, costly, and in itself an error-prone process. Thus, there is a demand in the rail industry for synthetic scheme plans. All constructions are given. The runtimes achieved by our tool are presented.
This short industrial paper discusses the challenge of precisely defining the scope of formal verification in industrial applications, to avoid both unintentional omission of verification of requirements and duplication of verification. It draws on the experience of using our formal verification technology, called SafeCap, in a substantial number of live railway signalling projects in the UK , and the solutions we are now developing. SafeCap uses safety invariants (safety properties) to formally and fully automatically verify the safety of site-specific configurations of railway interlockings using a dedicated symbolic theorem prover. The scope of this formal verification is a subset of the totality of site-specific interlocking configuration verification, which itself is a subset of the totality of signalling system verification. In the course of our work, it has also become apparent that there is a need to develop and use in practice different (often overlapping) sets of properties. There are various reasons for this: different railways use different safety standards from which the properties are developed; the standards themselves evolve; their is a need for versioning and change management of the properties during the continuous improvement of our tool. To this end, the paper puts forward the idea of defining the verification scopes (called dialects) together with a mechanism of introducing a scope as a set of verification properties which are tagged with the unique scope name. The paper uses various industrial scenarios we are facing in deploying SafeCap to demonstrate how this mechanism works in our commercial deployment.
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.
This paper presents the ETCS Moving Block system developed within Europe’s Rail Joint Undertaking (ERJU) programme to address today’s railway capacity constraints by replacing classical operational rules to optimize throughput. The concept was validated through simulations and field trials and future work includes extended field tests, contributing to European interoperability standards.
Each planning phase of ETCS-compliant railway tracks at Deutsche Bahn (DB) prescribes a concluding review, now performed by manually inspecting printed diagrams and tables. This is time-consuming and bears the risk to overlook critical mistakes. We present a concept and a tool for fully automated formal verification of railway plannings against ETCS planning rules. The approach is based on a modular translation of track models, as well as planning rules, to the SMT-LIB language understood by Satisfiability Modulo Theories (SMT) solvers, which are used as a backend. Track models are assumed to be available in the standardized object-oriented PlanPro format and are automatically translated to SMT-LIB constraints. The planning rules themselves are given in natural language in rule books and cannot be translated automatically. Instead, we provide a translation schema that lets a planning engineer render planning rules almost one-to-one as first-order formulas. No specific knowledge of logic or SMT solver internals is required to perform this task, and it is sufficient to do it once and for all for each planning rule. Subsequent verification of a track model against a planning rule is fully automatic. Deviations are visually highlighted for manual inspection. To this end, we integrated rule verification with an existing track visualization tool into a GUI. Our approach was evaluated with real DB infrastructure data, showing that it is easy to use and sufficiently powerful to be integrated into existing planning workflows.
Formal methods and domain-specific languages (DSLs) are now integral to the development and assurance of railway signalling systems in compliance with CENELEC EN 50128 and EN 50129. This article presents a survey and a comparison of research works and industrial initiatives that intertwine graphical DSLs with formal verification techniques. The comparison covers modelling syntax, operational semantics, adherence to industrial standards such as RailML, EULYNX and ERTMS/ETCS, and the extent to which each solution supports verification and validation. Special attention is devoted to initiatives that rely on the B Method and its associated toolchain, notably ProB, because these initiatives demonstrate how mathematically proven artefacts can be presented to, and interactively animated by, signalling engineers through user-friendly diagrams. The study highlights the added value of visual front-ends for bridging the communication gap between domain experts and formal-methods specialists while preserving traceability from informal requirements to verified systems.
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 supported in the original method because flank protection requires a coordination of distant points. The extension comprises soundness results for this new context and a decomposition strategy able to divide a network into sub-networks of minimal size.
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.
Upgrading rail network infrastructure involves complex system design decisions that can be informed by suitably abstract 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.
To ensure secure and efficient transportation, railway vehicles require high levels of reliability, availability, maintainability, and safety (RAMS). These attributes are strongly influenced by the effectiveness of maintenance strategies. Due to rapid advancements in digitalization and automation, rolling stock maintenance strategies currently undergo a shift from traditional corrective and preventive methods to condition-based and predictive approaches. However, one of the main challenges in adopting condition-based maintenance (CBM) lies in the significant initial investment required. To reduce maintenance costs and maximize operational value, it is crucial to identify the subsystems, those are most prone to failure, as they can lead to unplanned downtime or safety-critical incidents. This paper analyzes maintenance logs and accident reports of passenger trains to identify recurrent failures and critical subsystems. The most failure-prone subsystems, which account for up to 80
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 logics and 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).
Empirical formal methods (FMs) aim to ground the development, evaluation, and deployment of formal techniques in software engineering through systematic observation, data collection, and analysis. In the context of safety-critical domains such as railways, the need to balance mathematical rigor with practical feasibility makes empirical approaches particularly relevant. In this keynote summary, I will outline the scope and significance of empirical FMs, and present a retrospective on my experience applying these approaches in railway system development and verification. Drawing on a series of industrial and collaborative projects, I will discuss how empirical software engineering techniques such as surveys, systematic literature reviews, case studies, judgment studies, and tool evaluations have been used to assess the applicability, usability, and impact of FMs in practice. I will conclude with a roadmap for strengthening the empirical evidence base for FMs in railways, identifying research gaps and practical strategies to improve their integration into industrial processes, toolchains, and certification workflows.
The rail system is a complex system of systems that is entering the era of total automation thanks to wireless sensors and advanced communication, localization and perception systems that transfer the control functions of the human driver to computers. Information must be shared between the various stakeholders in the system: Infrastructure manager, train manager, maintenance manager, timetable manager, customer manager, etc. Consequently, wireless communications are widely deployed for train operation and will carry mission critical information. The question of safety demonstration and then dependability analysis of a wireless link is an open topic. In general, a so called “safety layer” is designed to cope with the wireless communications impairments. In particular the Euroradio philosophy will be recalled as an example of safety layer for train-to-ground communication. This protocol is not suitable for decentralized communications such as train-to-train or device-to device communications and new systems should be developed. The presentation will give an overview of the current deployment of wireless communication systems in the rail domain (train-ground, intra-train, inter-train) for train operation and the on-going developments at European level. Challenges to be solved will be highlighted and possible methodologies for dependability analysis will be presented.
Relay-based Railway Interlocking Systems (RIS) control railway components like signals and turnouts safely but are still analysed manually through their relay diagrams, a process prone to errors. Previous works proposed formal methods and industrial tools for RIS analysis, but digitalizing and automatically transforming these diagrams into formal specifications remained challenging. This paper presents a proof of concept using an existing Multimodal Language Model to analyse relay diagrams and automatically generate formal specifications in propositional logic. Our method adopts a prompt-based methodology to guide the expected outcome (model in propositional logic) which is then applied to new diagrams. The results confirm that automatic formalization is feasible and accessible. This work opens promising perspectives for further improving correctness through dedicated prompt engineering or fine-tuning, advancing automation of the formal verification of relay-based railway systems.
Ensuring the resilience of computer-based railways is increasingly crucial to account for uncertainties and changes due to the growing complexity and criticality of these systems. Although their software relies on strict verification and validation processes following well-established best-practices and certification standards, anomalies can still occur at run-time due to residual faults, system and environmental modifications that were unknown at design-time, or other emergent cyber-threat scenarios. This paper explores run-time control-flow anomaly detection using process mining to enhance the resilience of ERTMS/ETCS L2 (European Rail Traffic Management System/European Train Control System Level 2). Process mining allows learning the actual control flow of the system from its execution traces, thus enabling run-time monitoring through online conformance checking. In addition, anomaly localization is performed through unsupervised machine learning to link relevant deviations to critical system components. We test our approach on a reference ERTMS/ETCS L2 scenario, namely the RBC/RBC Handover, to show its capability to detect and localize anomalies with high accuracy, efficiency, and explainability.
