Jan Peleska, University of Bremen, Germany: New Distribution Paradigms for Railway Interlocking
Abstract: We discuss a new "flavour" of distributed interlocking systems, where the proper interlocking logic is allocated on cloud computers using conventional (i.e. commercial-off-the-shelf) multi-core hardware and operating systems. The servers in the cloud communicate with intelligent track elements over internet connections. Interlocking logic may even be geographically distributed on more than one server farm, introducing a new dimension of fault tolerance. This technology has been announced 2018 by Siemens Mobility, and a first application is expected to become operative this year. In this talk, it is analysed how the new distribution concept both presents opportunities for significantly higher reliability and availability, and at the same time introduces new threats to safety and security that had not been present in more conventional interlocking system architectures. We explain the basic mechanisms how safety and security are achieved in such a system, including means to safely re-use legacy interlocking software. It is shown how formal methods can be used to verify crucial safety mechanisms and allows for testing strategies with exceptional test strength. The material presented here is based on a collaboration between Siemens and Verified Systems International, a company specialised on verification and validation of safety-critical systems.
Signe Geisler, DTU Compute, Denmark (joint work with Anne Haxthausen):
Abstract: We consider the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. We describe for a real-world case study how this can be tackled by stepwise development and model checking of state transition models in an extension of the RAISE Specification Language (RSL). This method also allows different variants of the control protocols to be explored.
Per Lange Laursen and Van Anh Thi Trinh, DTU Compute, Denmark:
Abstract: This presentation investigates the modelling and model checking of an existing distributed railway control system algorithm using two different model checkers: UPPAAL and UMC. Control systems for specific railway networks are verified by providing a generic model with configuration data that describes the network and involved trains. Other variants of the control system with additional features or different modelling techniques have also been developed. Experiments are carried out on all versions in order to compare them with each other. These show that the models can handle networks of various sizes and layouts as well as verifying a real-world railway network.
Paulius Stankaitis, Newcastle University (joint work with Alexei Iliasov, Tsutomu Kobayashi, Yamine Aıt-Ameur, Fuyuki Ishikawa, and Alexander Romanovsky - SHORT contribution):
Abstract: This paper presents the rigorous development of a distributed resource allocation protocol in Event-B. The work is motivated by the challenges of ensuring safety and improving capacity of modern and emerging railway control systems. The development consists of several complementary verification steps. Ensuring deadlock freedom of the protocol is the main challenge of this work and by using proof and stochastic simulation techniques we demonstrate the continuous progress of the protocol. Protocol performance is evaluated in stressed situations by using the stochastic simulation approach.
Formal methods and tools
Thierry Lecomte, Clearsy, France: Formal Techniques for Safer Signalling Systems
Abstract: Designing safety critical railways signalling
systems is a difficult task, given the number of dimensions to analyse, the heterogeneity and the interdependency of the
devices composing these systems, and the ongoing replacement of history-based
nationwide signalling systems with a unique
interoperable one. To address all these issues, formal methods have been
experimented on real life systems to ensure safety demonstration at system,
software and data levels. The combination of existing formal proof techniques
and innovative modelling approaches makes possible the discovery of
specification errors (even for systems already deployed), the completion of
safety cases with a higher level of confidence and the seamless development of
safety critical functions.
This talk is going to present several applications of this kind, describing the technical frameworks, the added value and the results obtained so far.
Anne Haxthausen DTU Compute, Denmark (joint work with Jan Peleska and Linh Hong Vu - SHORT contribution)
Abstract: This presentation describes the RobustRailS verification method and tool set for automated, formal modelling and verification of ERTMS Level 2 based interlocking systems, and reports on its successful application to a Danish line. The tool set is centered around a domain-specific language (DSL) for describing application specific parameters (track layout and route control tables) and provides support for an automated 3 step verification and testing approach: (1) First a static check is performed on the domain-specific description, (2) then a formal, behavioural system model is automatically generated and model checked using an induction scheme by means of bounded model checker, and (3) finally model based testing of the implemented system is done using test cases, test oracles etc. automatically generated from the formal model. The static check is able to catch errors in the control tables, while the model checking is used to check that the system model is safe and can be used to catch errors in the designed control algorithms. The testing is used to catch errors in the implemented system.
Security and Blockchain technology
Jens Braband, Siemens Mobility GmbH, Germany: A Survey of Cybersecurity in Signaling
Abstract: The presentation covers main developments in Railway Signaling from the early 90s e. g. specification of ERTMS and the introduction of public networks for safety-related data transmission up to today’s challenges, e. g. IP based interlocking, use of COTS HW and SW, remote access etc. Also main developments in standardization as well as future developments are addressed.
Michael Kuperberg, Deutsche Bahn Systel Gmbh, Germany (partially based on joint work with Daniel Kindler and Sabina Jeschke):
Abstract: Conventional railway operations employ centralized custom software and hardware to ensure safe and secure train operations. A research project to make this setup more distributed and dynamic has created a blockchain-based prototype for decentralized train operations, train-to-train communications and usage billing. By using a tamper-resistant blockchain with smart contracts, the prototype enables the trains to find routes and make booking decisions which are conflict-free, safeguarded and protocolled in an auditable manner. In this talk, we present an approach for the systematic selection of a scalable and robust blockchain/DLT implementation for a Decentralized Rail Control System.
Moving block, Virtual coupling and positioning systems
Francesco Flammini, Linnæus University, Sweden (joint work with Stefania Santini and Valeria Vittorini):
Abstract: Railway infrastructure operators need to push their network capacity up to their limits in high-traffic corridors. Virtual Coupling is considered among the most relevant innovations to be studied within the European Horizon 2020 Shift2Rail Joint Undertaking as it can drastically reduce headways and thus increase line capacity by allowing to connect dynamically two or more trains in a single convoy. This talk addresses a proof of concept of Virtual Coupling by introducing a specific operating mode within the European Rail Traffic Management System / European Train Control System (ERTMS/ETCS) standard specification, and by defining a coupling control algorithm accounting for time-varying delays affecting the communication links. To that aim, one ploy is defined to enrich ERTMS/ETCS with Virtual Coupling without changing its working principles and a numerical analysis methodology is borrowed from the automotive field where it is used to study platooning. The numerical analysis supports the proof of concept with quantitative results in a case-study simulation scenario.
Davide Basile, Univ. of Florence, Italy (joint work with Alessandro Fantechi, Gianluca Mandò, Luigi Rucher):
Abstract: A promising option to improve performance and contain costs of current tramway signalling systems is to introduce an Autonomous Positioning System (APS) in substitution of traditional occupancy detecting sensors. APS is an onboard system that uses a plurality of sensors (such as GPS or inertial platform) and a Sensor Fusion Algorithm (SFA) to autonomously estimate the position of the tram with the needed levels of uncertainty and protection. Au- tonomous positioning however introduces, even in absence of faults, a quantita- tive uncertainty with respect to traditional sensors. This paper investigates this issue in the context of an industrial project: a model of the envisaged solution is adopted, and the UPPAAL Statistical Model Checker is used to study possible hazards induced by the substitution of legacy track circuits with on-board satellite positioning equipment.
Franco Mazzanti, ISTI-CNR, Italy: Modelling a Moving Block train control system: different techniques and tools
Abstract: UML behavioral diagrams (e.g. statecharts) are often accepted and encouraged as a standard communication mechanism among stakeholders. Event B machines are often exploited for the refinement of a system into an actually executable model, and for verifying its safety properties. Process Algebras are probably the most flexible specification mechanism that allows for a compositional verification of liveness properties of system of systems.
These different points of view are illustrated with respect to the same case study represented by a skeleton of moving block train control system.
Markus Roggenbach, Swansea University (joint work with Aled Walters, Yong Zhang, Phillip James, and Monika Seisenberger - SHORT contribution):
Abstract: The European Rail Traffic Management System (ERTMS) is a modern state-of-the-art railway control system which is based on the communication between trains and interlocking via a radio block centre. In the ERTMS standard level 2, the system is described using discrete control logic as well as differential equations when it comes to, e.g., braking curves. Thus, in its technical definition, the system is a hybrid one. The question now is what this means for modelling: either one provides a hybrid model, or one works with a timed model with explicit solutions of the differential equations. Both approaches are possible. In our presentation we compare how ERTMS can be modelled and verified with the three formal methods that come with verification tools: KeYmaera, Real-Time Maude, and UPPAAL. Here, KeYmaera allows us to formulate a hybrid model, which can be verified with theorem proving. Modelling with UPPAAL and Real-time Maude is done with timed models, where verification is performed through model-checking. Starting from a simple railway scenario, in all three methods we model ERTMS entailing elements of all components participating in its control cycle. Furthermore, we demonstrate that it is feasible to prove safety. Following previous work on comparing railway modelling approaches, we analyse commonalities and differences between the three tools w.r.t. modelling the ERTMS. The most prominent differences found concern: Simulation, Ability to cope with real world braking and acceleration curves, Ease of expressing control logic (control tables), Modelling without making a maximal progress assumption, Scalability.