The engineering of industrial systems, particularly in safety-critical domains such as railways, demands rigorous verification and validation processes to ensure system dependability. Formal methods have emerged as powerful tools to complement traditional software engineering practices. In the railway sector, which increasingly relies on complex, distributed, and cyber-physical control systems, formal methods have demonstrated particular value for many decades now. In this article, we provide a retrospective overview of the application of formal methods and tools in the railway domain, with emphasis on two prominent verification approaches and one frequently verified railway system: modeling and validation with the B method and tools and formal verification of interlocking systems by model checking. We explore their role in the design and development of key railway systems, highlighting both academic research and industrial success stories, as witnessed by international projects and initiatives. We conclude with an outlook on the potential of integrating AI and formal methods to enhance the efficiency of next-generation railway systems.

We present a distributed railway interlocking (IXL) method based on trains communicating with switch boxes deployed along the railway network for switching points and monitoring the occupancy states of track elements. The method does not require any centralised IXL components. A distributed architecture is proposed that carefully separates the overall business logic and automated train operation from the safety-critical automated train protection and distributed IXL logic. This architecture is also suitable for autonomous trains traversing the railway network. The safety of the IXL logic is formally proven, using the Isabelle/HOL proof assistant. Experiments confirm that this proof-based approach is superior to model checking approaches, since the model checking effort grows exponentially with the size of the railway network. In contrast to this, the mathematical safety proof is performed once and for all railway networks fulfilling a realistic well-formedness condition. For a concrete network, only the well-formedness of the network and its initial train placements has to be verified, whereas the safety of the dynamic behaviour is a consequence of the network-independent safety proof.

Abstract Formal methods for industrial critical systems are essential because they provide mathematically rigorous techniques to specify, design, and verify system behavior. This reduces the risk of failures in safety- and security-critical domains such as aerospace, automotive, and healthcare. This special issue of Software Tools for Technology Transfer contains four papers presenting recent advances in tools target the use of formal methods for critical systems in industry. The papers are revised and extended versions of selected conference papers from the 29th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2024).

Securing a safety-critical system is a challenging task, because safety requirements have to be considered alongside security controls. We report on our experience to develop a security architecture for railway signalling systems starting from the bare ...

Model checking techniques have often been applied to the verification of railway interlocking systems, responsible for guiding trains safely through a given railway network. However, these techniques fail to scale to the interlocking systems controlling large stations, composed of hundreds and even thousands of controlled entities, due to the state space explosion problem. Indeed, interlocking systems exhibit a certain degree of locality that allows some reasoning only on the mere set of entities that regard the train movements, but safe routing through a complex station layout requires a global reservation policy, which can require global state conditions to be taken into account. In this article, we present a compositional approach aimed at chopping the verification of a large interlocking system into that of smaller fragments, exploiting in each fragment a proper abstraction of the global information on routing state. A proof is given of the thesis that verifying the safety of the smaller fragments is sufficient to verify the safety of the whole network. Experiments using this compositional approach have shown important gains in performance of the verification, as well as in the size of affordable station layouts.

Abstract In this paper, we review software-based technologies already known to be, or expected to become essential for autonomous train control systems with grade of automation GoA 4 (unattended train operation) in existing open railway environments. It is discussed which types of technology can be developed and certified already today on the basis of existing railway standards. Other essential technologies, however, require modifications or extensions of existing standards, in order to provide a certification basis for introducing these technologies into non-experimental “real-world” rail operation. Regarding these, we check the novel pre-standard ANSI/UL 4600 with respect to suitability as a certification basis for safety-critical autonomous train control functions based on methods from artificial intelligence. As a thought experiment, we propose a novel autonomous train controller design and perform an evaluation according to ANSI/UL 4600. This results in the insight that autonomous freight trains and metro trains using this design could be evaluated and certified on the basis of ANSI/UL 4600 .

No abstract available.

Abstract This paper considers the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. It describes how this challenge can be tackled by stepwise development and model checking of state transition system models in a new extension of the RAISE Specification Language. Railway interlocking systems are reconfigurable systems which can be configured by supplying data describing the network to be controlled and other details. Therefore, such systems are natural candidates for being modelled by generic state transition systems, which abstract away from the concrete configuration at the time of modelling, and can later be instantiated with concrete data. For a real-world case study, a generic state transition system is developed in steps, starting with an abstract model of the essential system behaviour and incrementally adding details and restrictions. The stepwise development method allows different variants of the control protocol to be explored. The generic models are instantiated with concrete configuration data, after which desired properties, in particular safety properties, of the system models are verified using model checking.

Abstract In this paper, an efficient approach to data validation of distributed geographical interlocking systems (IXLs) is presented. In the distributed IXL paradigm, track elements are controlled by local computers communicating with other control components over local and wide area networks. The overall control logic is distributed over these track-side computers and remote server computers that may even reside in one or more cloud server farms. Redundancy is introduced to ensure fail-safe behaviour, fault-tolerance, and to increase the availability of the overall system. To cope with the configuration-related complexity of such distributed IXLs, the software is designed according to the digital twin paradigm: physical track elements are associated with software objects implementing supervision and control for the element. The objects communicate with each other and with high-level IXL control components in the cloud over logical channels realised by distributed communication mechanisms. The objective of this article is to explain how configuration rules for this type of IXLs can be specified by temporal logic formulae interpreted on Kripke Structure representations of the IXL configuration. Violations of configuration rules can be specified using formulae from a well-defined subset of LTL. By decomposing the complete configuration model into sub-models corresponding to routes through the model, the LTL model checking problem can be transformed into a CTL checking problem for which highly efficient algorithms exist. Specialised rule violation queries that are hard to express in LTL can be simplified and checked faster by performing sub-model transformations adding auxiliary variables to the states of the underlying Kripke Structures. Further performance enhancements are achieved by checking each sub-model concurrently. The approach presented here has been implemented in a model checking tool which is applied by Siemens Mobility for data validation of geographical IXLs.

The current trend of distributing computations over a network is here, as a novelty, applied to a safety critical system, namely a railway interlocking system. We show how the challenge of guaranteeing safety of the distributed application has been attacked by formally specifying and model checking the relevant distributed protocols. By doing that we obey the safety guidelines of the railway signalling domain, that require formal methods to support the certification of such products. We also show how formal modelling can help designing alternative distributed solutions, while maintaining adherence to safety constraints.

Abstract This paper describes a complete model-based development and verification approach for railway control systems. For each control system to be generated, the user makes a description of the application-specific parameters in a domain-specific language. This description is automatically transformed into an executable control system model expressed in SystemC. This model is then compiled into object code. Verification is performed using three main methods applied to different levels. (0) The domain-specific description is validated wrt. internal consistency by static analysis. (1) The crucial safety properties are verified for the SystemC model by means of bounded model checking. (2) The object code is verified to be I/O behaviourally equivalent to the SystemC model from which it was compiled.

Abstract This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering.

The authors introduce the concept for a distributed railway control system and present the specification and verification of the main algorithm used for safe distributed control. Our design and verification approach is based on the RAISE method, starting with highly abstract algebraic specifications which are transformed into directly implementable distributed control processes by applying a series of refinement and verification steps. Concrete safety requirements are derived from an abstract version that can be easily validated with respect to soundness and completeness. Complexity is further reduced by separating the system model into a domain model and a controller model. The domain model describes the physical system in absence of control and the controller model introduces the safety-related control mechanisms as a separate entity monitoring observables of the physical system to decide whether it is safe for a train to move or for a point to be switched.