Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

The impact that cyber issues might have on the safety and resilience of railway systems has been studied for more than five years by industry specialists and government agencies. This paper presents some of the work done by Adelard in this area, ranging from an analysis of potential vulnerabilities in the ERTMS specifications through to a high-level cyber security risk assessment of a national ERTMS implementation and detailed analysis of particular ERTMS systems on behalf of the GB rail industry. The focus of the paper is on our overall methodology for security-informed safety and hazard analysis. Lessons learned will be presented but of course our detailed results remain proprietary or sensitive and cannot be published.

Since several years, ClearSy has driven large projects about using formal proofs at system level in the railway domain. The fundamental goal in these projects is to extract the rigorous reasoning establishing that the considered system ensures its requested properties, and to assert that this reasoning is correct and fully expressed. In this paper, we give feedback about the methodology used in all these projects, about the differences made by whether the concerned system is currently under design or already existing and about the benefits obtained. The formal proofs are performed using Event-B, with the Atelier-B toolkit.

Recent progress in bounded model checking and inductive reasoning has shown that the fully automated verification of route-based interlocking system designs of realistic “real-world” complexity is possible and ready for industrial application. In this paper, we present a new model-based testing strategy for interlocking system controllers that exploits the fact that the design has already been verified, so that it can be used as a reference model for test case and test oracle generation. Our special interest lies in the field of complete testing strategies that are able to uncover every implementation error, provided that the implementation behaviour is captured in a pre-specified fault domain. Despite their guaranteed test strength, these strategies have two well-known disadvantages: (1) applied in a naive way, they often result in an infeasible amount of test cases, and (2) the hypothesis that the real implementation behaviour is captured by a member of the fault domain can rarely be justified in a convincing way. We describe a new combination of compositional reasoning and input equivalence class generation techniques that removes problem (1). For coping with disadvantage (2), we suggest a combination of equivalence class and random testing that - while not being able to guarantee complete fault coverage for implementations outside the fault domain - results in a test strength that is significantly higher than heuristic test approaches for interlocking system controllers. Estimates are presented that show how application of this novel strategy reduces the effort for HW/SW integration testing, while simultaneously increasing the fault coverage in comparison to more conventional testing approaches.

This paper presents a formal analysis of the train to trackside communication protocols used in the European Railway Traffic Management System (ERTMS) standard, and in particular the EuroRadio protocol. This protocol is used to secure important commands sent between train and trackside, such as movement authority and emergency stop messages. We perform our analysis using the applied pi-calculus and the ProVerif tool. This provides a powerful and expressive framework for protocol analysis and allows to check a wide range of security properties based on checking correspondence assertions. We show how it is possible to model the protocol’s counter-style timestamps in this framework. We define ProVerif assertions that allow us to check for secrecy of long and short term keys, authenticity of entities, message insertion, deletion, replay and reordering. We find that the protocol provides most of these security features, however it allows undetectable message deletion and the forging of emergency messages. We discuss the relevance of these results and make recommendations to further enhance the security of ERTMS.

The railway system has benefited from the rapid technology revolution since the 1990s. The mechanical and manpower intensive railway system has gradually evolved into a centralize- and digital-controlled, information- and communication-based system. IT security was not considered during the system (re)design. This paper begins with discussing the need and absence of procedures to sustain operations when an IT security breach has occurred or is suspected.

Then operational security is introduced. It is a new research field which focuses on operational procedures taking into account the effects of safety as well as security-related changes in the system e.g. due to failures or threats. The scope of operational security and general requirements on operational procedures will then be discussed. Lastly, we give an outline of a proposed project with its planned work packages.

The three-key Triple Data Encryption Algorithm (Triple Data Encryption Algorithm is also known in the literature as Triple-Des, or Triple DEA or TDEA) (3Des ) is a symmetric encryption algorithm currently used in the European Traffic Management System (ERTMS) for integrity and authentication purposes. In a recent publication [1], 3Des has been withdrawn in favour of Advanced Encryption Standard (AES ) [2] (The National Institute for Science and Technology (NIST) standard [1] allows to both algorithms can be used for specific purposes until 2030 with the intention of gradually phasing out 3Des towards AES ). In this paper, we have investigated, from a practical point of view, known attacks to 3Des and proved that, in order to carry out such attacks, a disproportionate amount of hardware and money would be necessary. In practical terms this means that these attacks do not represent a realistic risk.

The complexity of railway control system makes some requirement deficiencies hard to find, which results in system failures. It is essential to locate those deficiencies using logs recorded during failure events. In this paper, a model checking based failure analysis approach was proposed and applied to a case of abnormal emergency brake. First, a system model describing the system requirement and an event model depicting the logs were constructed. Next the compositional model was verified through model checking in UPPAAL which then produced a counterexample trace that describes the system behaviour in the failure event. By analysing this trace, an inadequacy was found in the requirement and a modification strategy was brought up which was formally verified to be effective.

In recent years, formal methods have become an important approach to ensure the correct function of complex hardware and software systems. Many standards for safety critical systems recommend or even require the use of formal methods. However, building a formal model for a given specification is challenging. This is, because verification results must be considered with respect to the validity of the model.

This leads to the question: “Did I build the right model?”. For system development the analogous question “Did I build the right system?”. This is often answered with requirements traceability through the whole development cycle. For formal verification this question often remains unanswered.

The standard model, which is used in development of safety critical applications is the V-model. The core idea is to define tests for each phase during system development. In this paper, we propose an approach - analogously to the V-model for development - which ensures correctness of the formal model with respect to requirements. We will illustrate the approach on a small example from the railways domain.

The paper presents an experience of verifying a large scale, real-life dataset describing various aspects of railway station design. We discuss how a number of assorted digital artefacts were pooled together and converted into a set-theoretic model over which a type inference procedure is run. The typed model is then used to confirm or contradict logical conjectures over data elements. We employ a number of state-of-the-art SMT solvers as a verification back-end. The project is ongoing but has already identified a number of issues in topology definition and signalling data that were missed by other automated tests and not revealed by simulation tools.

In the railway domain, an electronic interlocking is a computerised system that controls the railway signalling components (e.g. switches or signals) in order to allow a safe operation of the train traffic. Interlockings are controlled by a software logic that relies on a generic software and a set of application data particular to the station under control. The verification of the application data is time consuming and error prone as it is mostly performed by human testers.

In the first stage of our research [3], we built a model of a small Belgian railway station and we performed the verification of the application data with the nusmv model checker. However, the verification of larger stations fails due to the state space explosion problem. The intuition is that large stations can be split into smaller components that can be verified separately. This concept is known as compositional verification. This article explains how we used the ocra tool in order to model a medium size station and how we verified safety properties by mean of contracts. We also took advantage of new algorithms (k-liveness and ic3) recently implemented in nuxmv in order to verify LTL properties on our model.

Formal verification of safety-critical systems is crucial for demonstrating their safety to the certification bodies. In particular, the railway network validation requires rigorous analyses and the use of formal methods to meet railway standards. This student paper outlines objectives and the current progress of the work on verification of complex railway networks consisting of the areas with different signalling and interlocking.

The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies.

The real-time prediction of train movements in time and space is required for ensuring the reliability in operational management and in the information that is relayed to passengers. In practice, however, accurate predictions of train arrival times are very difficult to achieve, given the nature of uncertainty and unpredictability in train movements. This is often due to truly random delay causes that results in a constantly changing probability distribution in delay events as the effects of those causes. The overall consequence is less reliable estimates in train arrival times being made, which can potentially reduce the ability of traffic controllers to effectively plan and respond to disruptions. This paper presents a series of methods that are currently being applied for developing a preliminary working prototype of a future rail advisory system, which is the main objective of an ongoing PhD research project. The system prototype is expected to be capable of relaying advice to a traffic controller with the goal of minimising the effects of a disruption as much as possible and to potentially avoid future disruptions, for which accurate train movement and delay predictions using methods in predictive reasoning and machine learning are vital.

Like other contemporary safety standards EN-50128 requires to identify potential functional and non-functional hazards and to demonstrate that the software does not violate the relevant safety goals. Examples of safety-relevant non-functional hazards are violations of resource bounds, especially stack overflows and deadline violations, as well as run-time errors and data races. They can cause erroneous and erratic program behavior, invalidate separation mechanisms in mixed-criticality software, and even trigger software crashes. Classical software verification methods like code review and testing with measurements cannot really guarantee the absence of errors. Abstract interpretation is a formal method for static program analysis which supports formal soundness proofs (it can be proven that no error is missed) and which scales. This article gives an overview of abstract interpretation and its application to compute safe worst-case execution time and stack bounds, and to find all potential run-time errors, and data races. We discuss the tool qualification of abstract interpretation-based static analyzers and describe their contribution with respect to EN-50128 compliant verification processes. We also illustrate their integration in the development process and report on practical experience.

In order to analyse extensively the safety of the deployed railway software systems, RATP rely on rigorous verification methodologies based on formal methods. During the past few years, RATP has developed a new formal verification method called PERF, supported by a rich proof tool-chain. The main purpose of this method is to perform a non-intrusive verification on the implemented software. Unlike many formal methodologies, it does not require any intervention in the early stages of the software development.

In this paper, we present the PERF methodology as well as the different part of its supporting tool-chain with some feedback on the its application in some real projects. We also present the ongoing and future work around the PERF tool-chain.

It is common practice in critical software development, and compulsory in railway software developed according to EN 50128 standard, to separate software specification from software implementation. Verification activities should be performed to ensure that the latter is a correct refinement of the former. When the specification is formalized, for example in B method, the refinement relation can even be formally proved. In this article, we present how a similar proof of refinement can be performed at the level of the programming language used for implementation, using the SPARK technology. We describe two techniques to specify abstractly the behavior of a software component in terms of mathematical structures (sequences, sets and maps) and a methodology based on the SPARK tools to prove automatically that an efficient imperative implementation is a correct refinement of the abstract specification.

Systerel Smart Solver (S3) is a formal verification toolset built around a synchronous modeling language (HLL), and a SAT-based symbolic Model Checker developed by Systerel. It allows building efficient formal verification solutions specially fitted for a given mission in a given development process, with a built-in focus on trustworthiness. The architecture of such a solution is described, and its application to the proof of high-level properties unambiguously implying the safety of large industrial railway control systems is reported.

In this paper, we report on our recent improvements in the Alt-Ergo SMT solver to make it effective in discharging proof obligations (POs) translated from the Atelier-B framework. In particular, we made important modifications in its internal data structures to boost performances of its core decision procedures, we improved quantifiers instantiation heuristics, and enhanced the interaction between the SAT solver and the decision procedures. We also introduced a new plugin architecture to facilitate experiments with different SAT engines, and implemented a profiling plugin to track and identify “bottlenecks” when a formula requires a long time to be discharged, or makes the solver timeout. Experiments made with more than 10,000 POs generated from real industrial B projects show significant improvements compared to both previous versions of Alt-Ergo and Atelier-B’s automatic main prover.