ABSTRACT. 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 proposes 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 tool chain, 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.

ABSTRACT. 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 the rapid advancements in digitalization and automation, the maintenance strategies for rolling stock 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 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% of failures, are presented. Furthermore, the paper presents a comprehensive overview of the state-of-the-art CBM technologies used in railway vehicles, including both onboard systems and wayside monitoring solutions. These findings support the development of more targeted and cost-efficient maintenance practices in the railway sector.

ABSTRACT. Technological advances in modern Train Control Systems (TCSs) hold substantial promise for revolutionizing railway transportation de- pendability in terms of safety, availability, and operational capacity. This transformation is primarily driven by cutting-edge distancing policies such as Moving Block (MB) signaling and Virtual Coupling (VC), which are powered by sophisticated train localization technologies including satellite-based positioning systems. At the same time, these technological advances raise notable concerns about the effects that uncertainty in critical TCS parameters (such as train position and speed) may have on dependability-related attributes. Recently, various approaches have been proposed to characterize such effects through quantitative measures, leveraging formal stochastic modeling and evaluation of the TCS behavior. This study presents a comprehensive Systematic Literature Review investigating quantitative methodologies for assessing TCS dependability under uncertain conditions. Through careful selection and analysis of 42 peer-reviewed publications spanning 2011-2023, we provide both empirical insights and a structured taxonomic framework that illuminates the current landscape of research initiatives and practical implementations in quantitative dependability assessment for modern train control systems.

ABSTRACT. We use a railway-related case study to illustrate the differences that can be encountered while modelling 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 analyse instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.

ABSTRACT. The VCTS (Virtual coupling of Train Set) concept is considered as a game changer to increase capacity and flexibility of the railway system. The im-plementation of this concept, while maintaining the same safety level for train operation, requires exchanges of information between train and control center and between the train sets during the process. The wireless technolo-gy that will be deployed to support VTCS should answer stringent require-ments in terms of availability and performance. A safety layer at the applica-tion level should be developed. Euroradio covers train-to-ground communi-cations with a centralized system, and at this stage is not suitable for VTCS. This work presents a Coloured Petri Net (CPN)-based modelling and sim-ulation framework for evaluating the dependability of Train-to-Train (T2T) wireless communication in the context of virtual coupling of trains, consid-ering 5G NR V2X system. First, the VCTS and its overall architecture are in-troduced. After presentation of dependability analysis related methodologies, we detail the proposed modeling of T2T communication with CPN and the metrics considered. Simulation results show that under low Message Loss Rate conditions, the system performs well and meets the performance needs of 3GPP V2X standards. However, as MLR increases, system reliability and safety degrade significantly, highlighting the need for strong error handling and service quality mechanisms. Since there are currently no specific wire-less communication requirements defined for VCTS, our work considers au-tomotive standards, specifically 3GPP V2X and 5G Automotive Association requirements as a practical reference.

ABSTRACT. The railway domain is regulated by rigorous safety standards to ensure that specific safety goals are met. Often, safety-critical systems rely on custom hardware-software components that are built from scratch to achieve specific functional and non-functional requirements. Instead, the (partial) usage of Commercial Off-The-Shelf (COTS) components is very attractive as it potentially allows reducing cost and time to market. Unfortunately, COTS components do not individually offer enough guarantees in terms of safety and security to be used in critical systems as they are. In such a context, RFI (Rete Ferroviaria Italiana), a major player in Europe for railway infrastructure management, aims at equipping track-side workers with COTS devices to remotely and safely interact with the existing interlocking system, drastically improving the performance of maintenance operations. This paper describes the first effort to update existing (embedded) railway systems to a more recent cyber-physical system paradigm. Our Remote Worker Dashboard (RWD) pairs the existing safe interlocking machinery alongside COTS mobile components, making cyber and physical components cooperate to provide the user with responsive, safe, and secure service. Specifically, the RWD is a SIL4 cyber-physical system to support maintenance of actuators and railways in which COTS mobile devices are safely used by track-side workers. The concept, development, implementation, verification, and validation activities to build the RWD were carried out in compliance with the applicable CENELEC standards required by certification bodies to declare compliance with specific guidelines.

ABSTRACT. Ensuring the resilience of computer-based railways is increasingly crucial to account for uncertainties and changes due to the growing complexity and criticality of those 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.

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

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

ABSTRACT. We illustrate an approach to efficiently derive optimal signal schedules for multimodal intersections among vehicle flows and right-of-way tram lines, minimizing the maximum expected percentage of queued vehicles of each flow. We model trams by Stochastic Time Petri Nets (STPNs), capturing periodic tram departures and bounded delays and travel times with general (i.e., non-Exponential) distribution, and we model vehicles by finite-capacity vacation queues, with general vacation times determined by the intersection availability. For each vehicle flow, we study the expected queue size, deriving both its transient behavior and its steady-state distribution at multiples of the hyperperiod (resulting from nominal tram arrival times and vehicle traffic signals). By doing so, we study the behavior of each vehicle flow over arbitrary-duration intervals by performing transient analysis for the hyperperiod duration, starting from the steady-state distribution of the expected queue size. Experimental results on case studies of real complexity with time-varying parameters show the approach effectiveness at identifying optimal traffic signal schedules, notably exploring in few minutes hundreds of schedules requiring tens of hours in Simulation of Urban MObility (SUMO).

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

ABSTRACT. Abstract. 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 opera- tion of autonomous tram vehicles is achieving ultra-reliable positioning accuracy, which traditionally relies on costly, infrastructure-heavy solu- tions 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 posi- tioning and velocity estimation systems. Our method validates and com- bines outputs from multiple sensors, leveraging a sophisticated consis- tency 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 esti- mation accuracy and offers substantial cost and maintenance efficiencies by eliminating the need for trackside infrastructure.