Keywords

1 Introduction

In the last few decades railway domain has proved to be a fruitful area for applying various formal methods. Yet the latest railway challenges will require novel modelling techniques and adequate formal verification tools support. Integrating modern railway signalling systems within an outdated national railway networks is currently one of the major challenges. Indeed a gradual railway modernisation process means that heterogeneous railway signalling networks will be inevitable due to practical constraints. In some situations mainline services must be integrated with urban networks which simply require different signalling solutions as high service availability can only be achieved with a moving block signalling solutionFootnote 1. To give an example Crossrail is a major ongoing railway project where mainline services will be integrated with a high performance urban railway system. This particular network will operate with three different signalling systems. In western and eastern branches of the network fixed block signalling systems will operate whereas the central area will be operated with a moving block principle. Novel signalling interfaces will be developed to ensure a smooth and safe rolling stock signalling transition. In short this PhD study aims to address the challenge of modelling and verification of railway networks with different signalling systems.

The following section overviews key difficulties in formally modelling and verifying such systems which are in fact cyber-physical systems. Secondly we discuss more notable related work examples and present technical contributions this research aims to achieve. Last two sections discuss the current work on modelling and verification of a distributed railway network in the Event-B language and future research objectives.

2 Formal Methods in Railway Domain

Formal methods - a mathematical model driven methods provide a systematic approach for developing complex systems. They offer an approach to specify systems precisely via a mathematically defined syntax and semantics as well as formally validate them by using semi-automatic or automatic techniques. At the moment among the biggest challenges in the field is ensuring safety and correctness of cyber-physical systems.

For years formal methods have been successfully applied to the railway domain however yet a considerably little work has been done in including a cyber-physical nature of railway for a safety reasoning. Established railway operation principles did not require that so formal methods mainly focused on a static railway data verification - control table verification. However modern signalling systems were developed to reduce an overdesign and hence increase the capacity of railway networks. Railway operational principles have been rapidly moving towards a continuous agent communication and a more dynamic parameter (e.g. permitted speed profile) computation which are indeed two essential aspects of cyber-physical systems - communication and computation. Therefore to model and reason about safety of a modern signalling system we believe it is paramount to consider a cyber-physical nature of railway.

In general cyber-physical systems [30] have tight integration of communication, computation and control aspects and include discrete as well as continuous behaviours. Indeed the difficulty in modelling and verifying cyber-physical systems is a necessity to consider all these aspects together. To this date there exists no formal framework which could capture a tight integration of these systems aspects [18]. Furthermore for a lot of safety-critical system the dynamic nature of an environment has to be considered in the model as well. For instance a lossy communication aspect is particularly important when modelling modern-radio based railway signalling systems or railway systems with signalling transitions. Hybrid systems formal verification challenges arise mainly due to continuous variables with non-linear dynamics [3, 31]. An algorithmic verification of hybrid systems with available model checking tools is limited even under severe restrictions whereas simulation tools coverage is not adequate for a safety reasoning. In spite of that system validation through simulation is still the most prevalent method used by railway industry today. Alternative methods such as a deductive verification method are not limited by the state space and combined with computer algebra systems can deal with non-linear dynamics though some problems for an automated deductive verification still have to be resolved [4].

Related work. Over the years formal methods were primarily applied only for a discrete safety reasoning of the railway systems. The literature review revealed that only a small fraction of all railway oriented research considered a cyber-physical nature of railway systems. The following paragraphs discuss a more notable related work on distributed dynamic railway systems which are a class of cyber-physical systems.

To authors knowledge the earliest attempt to formally analyse distributed railway solid-state interlocking systems was completed by Morley [23]. In this interesting work author developed a formal model of a protocol for a cross boundary route locking and releasing mechanism. By analysing temporal properties of the model he discovered that in certain scenarios safety properties can be violated. Few years later a paper by Cimatti et al. [10] presented an industrially driven formal methods study where authors formally modelled a communication protocol for safety-critical distributed systems including distributed railway interlocking systems. Their method used Statecharts diagrams to specify high level protocol properties and the objectGEODE model checker for the protocol validation. In other work a different concept of distributed railway control system was introduced by Haxthausen and Peleska [14]. Their presented engineering concept of the control system relied on a radio based communication and switch boxes - systems which can only control a single railway point. Authors formally modelled the system with the RAISE [13] specification language which allowed to develop a formal model incrementally using a refinement process and prove refinement and safety properties with available justification tools. The timing properties of the design were considered in the extended work [22]. Similar ideas for distributed railway interlocking system were also presented in [8, 15] where authors used Statecharts and Petri Nets to model and verify decentralised railway interlocking.

At the same time André Platzer introduced an alternative approach to exploring a state-space with model checkers in verifying systems safety. A developed formalism and logic for reasoning about hybrid systems uses a deductive verification and can be implemented in a KeyMaera X verification tool [24, 26]. The later work presented a case study where differential dynamic logic was applied for a safety verification of the European Train Control System [27]. Differential Dynamic Logic was also used to model and verify a handover protocol between two trackside train control systems (radio-block centres) by Liu et al. [21]. In a work by Cimatti et al. [11] authors proposed a different logic based on the temporal logic with regular expressions. Their motivation was driven by a need of the automatic verification method for verifying hybrid requirements for hybrid railway system. A more recent work by Iliasov et al. [17] proposed a domain specific language - Unified Train Driving Policy. The formal notation allows to express both static and dynamic properties of railway in readable syntax which can be interpreted by railway engineers without prior knowledge of formal methods. A few recent formal methods projects on cyber-physical systems applied their novel techniques for modelling and verification of hybrid railway systems [16, 28, 29].

In the previous project on modelling and verification of railway interlocking systems we discussed possible future PhD study directions for addressing the safety of heterogeneous railway networks [32]. The two year project focused on developing an expressive railway oriented simulator which would enable modelling and analysing complex railway including railway systems with mixed signalling. In the future we plan to use the system-level simulator as a specification front-end for our modelling framework discussed in the following paragraph.

This PhD research aims to focus on theories and techniques for formal modelling and verification of classes of distributed hybrid railway systems which are in fact what we define as heterogeneous railway networks. In particular we are interested in developing a railway oriented formal modelling framework which could capture dynamic distributed hybrid systems. A similar work [12, 20] has been completed for more general cooperating agent based systems by exploring design patterns or more focused on dynamic distributed hybrid systems in [25]. In our work we would like to continue in this direction but by restricting our methodology to the railway domain. First of all to develop such a formal framework to reason about distributed hybrid railway networks one needs to understand and formally define a general railway design structure. The formal framework should not only capture existing railway operation principles for which a number of domain-specific languages already exists but also allow modelling moving block signalling systems. In the previous paragraphs we also emphasised the necessity to consider a cyber-physical nature of railway for safety reasoning. Therefore an important requirement for the modelling formal framework is to allow capturing continuous evolution of agents and for that we can use existing approaches for instance hybrid automata. The modelling notation should not only have executional semantics which is exactly the simulation of railway operation but it also should offer proof semantics. The work by Damm et al. [12] proposed a generic proof-rules for reducing the complexity of the reasoning about collision avoidance systems. In this PhD research we will attempt to further improve this approach by specifically addressing the railway domain. To enable reasoning about safety of heterogeneous railway signalling we will need to include new safety rules for a system transition reasoning - a similar but more generic to presented in [21]. Lastly in order to ensure that results have potential to be useful in the industrial setting this research will be conducted in a close cooperation with Siemens Rail Automation.

In the following section we present an ongoing work which aims to develop a generic design pattern for distributed railway networks. For that we use the Event-B modelling language as a back-end formal notation which offers a refinement based modelling language. It allows to start with an abstract model for instance the skeleton of a dynamic distributed railway system and then include new details through a number of correctness preserving refinement steps for instance details of a specific signalling system. In this paper we will not discuss hybrid modelling part of the framework but we will base our work on existing methods developed for Event-B [5, 7].

3 Distributed Formal Railway Model in Event-B

The Event-B mathematical language used in the system development and analysis is an evolution of the classical B method [1] and Action Systems [6]. Perhaps due to the success of the B method and a good tool support Event-B has also been a popular language choice for modelling railway systems [2, 9, 19]. The formal specification language offers a fairly high-level mathematical language based on a first-order logic and Zermelo-Fraenkel set theory as well as an economical yet expressive modelling notation. The formalism belongs to a family of state-based modelling languages where a state of a discrete system is simply a collection of variables and constants whereas the transition is a guarded variable transformation.

Fig. 1.
figure 1

Event-B machine structure.

Full size image

A cornerstone of the Event-B method is the step-wise development that facilitates a gradual design of a system implementation through a number of correctness preserving refinement steps. The model development starts with a creation of a very abstract specification and the model is completed when all requirements and specifications are covered. The Event-B model is made of two key components - machines and contexts which respectively describe dynamic and static parts of the system. The context contains modeller declared constants and associated axioms which can be made visible in machines. The dynamic part of the model contains variables which are constrained by invariants and initialised by an action. The state variables are then transformed by actions which are part of events and the modeller may use predicate guards to denote when event is triggered (see Fig. 1). Specifying a model is not sufficient one must provide evidence about the correctness of the model as well. The Event-B method is a proof driven specification language where model correctness is demonstrated by generating and discharging proof obligations - theorems in the first-order logic. The model is considered to be correct when all proof obligations are discharged.

The following subsections present an ongoing work on modelling a distributed railway interlocking. In particular we focus on modelling the distributed resource allocation problem where processes can capture and release available resources as it is paramount for a distributed railway interlocking. To develop a protocol for a safe distributed route locking mechanism in further refinements undischarged proof obligations will be used.

3.1 Abstract Distributed Railway Interlocking Model

First of all we describe the modelling and refinement plan of a distributed railway signalling with main requirements at each step. The initial abstract model specifies the general concept of a distributed resource allocation protocol - processes capturing and releasing available resources. Starting with such a mathematical abstraction allows to simplify the development of a protocol without considering complicated railway requirements at early modelling stages.

Initial model. An abstract model of processes capturing resources.

  1. 1.

    An abstract model context - processes and resources (finite sets).

  2. 2.

    An abstract model contains events for capturing and releasing resources.

  3. 3.

    Processes can only capture not already captured resources.

  4. 4.

    Processes can only release their captured resources.

  5. 5.

    Processes could capture more than a single resource at a time.

  6. 6.

    No two or more processes can have same resources captured.

Refinement 1. Extending the model with events for requesting and granting resources and solving a contention problem.

  1. 1.

    Introducing events for requesting and granting resources.

  2. 2.

    Introducing events for detecting and solving the contention problem.

  3. 3.

    Resources can only be captured if requested and granted by the process.

  4. 4.

    Same resources can be requested by multiple processes at the same time.

  5. 5.

    Resources request from a single process cannot be partially granted.

  6. 6.

    Processes can request any set of resources.

  7. 7.

    Resources can be granted to the process if they have not been requested, granted or captured by other processes or if the conflict has been solved with detect/solve events.

Other Refinements. Introducing graph based resource structures and railway related context (not discussed in this paper).

  1. 1.

    Distributing resources in to separate zones with associated controllers.

  2. 2.

    Introducing a graph based resource structure in to the model.

  3. 3.

    Introducing a railway related context and route locking principles.

Other properties such as a system progress can be addressed by assuming that processes release resources eventually and also by introducing a resource granting queue. In the initial model we only impose a single railway related safety rule which states that collision freedom is ensured if no two or more trains share the same route. This can be simply expressed by the invariant - no two or more processes can have same resources captured.

The modelling was started by creating the abstract context with two carrier sets for processes and resources with two associated axioms stating that these sets are finite. In the dynamic part of the model we defined a global variable mrk (marked) for mapping resources to processes. Furthermore we introduced two events for capturing and releasing resources which are in fact abstract representations of a railway route locking and releasing operations. Both events have similar guards except one can only release resources if they have already been captured.

figure a

In the next model refinement a logical step then was to introduce two new events for requesting and granting resources and two buffers for storing resourced requests (req) and granted resources (ack). A process can request any subset of resources and grant event then checks whether those resources are not captured or granted for other processes. Because of new events we also needed to update the abstract capture event with stronger guards and additional action to update both buffers.

figure b

The request buffer may contain multiple requests for the same resources from different processes. So the resource grant event will only grant a set of resources to a single process if they have not been requested by other process. In case of multiple requests for the same resources from different processes we needed to introduce another two events for detecting and solving such a situation discussed in the following subsection.

3.2 Contention Problem for Distributed Railway Interlocking

A very common problem in developing distributed systems is the contention problem. In our model the problem can arise when a number of same resources have been requested by different processes. Since we do not allow partial resource allocation because of the safety principle which comes from the railway domain the system deadlocks. To resolve this we simply introduced two new events for detecting and solving this problem. The contention detection event is enabled when there exists a set of processes which all requested common resources and if those resources have not been captured yet. This event action simply copies the set of interested requests to another buffer - cnt (contention).

figure c

After that the following event grant (not shown here) nondeterministically selects a process from that buffer and grants resources for that single process and also removes its requests from the request buffer. The detect/solve process then can be repeated for remaining processes. At this level one does not need to consider which process is given a priority this becomes more important when graph based resource structure is introduced.

4 Conclusions and Future Work

In this paper we presented the main motivation of this PhD research which is the need of new formal methods techniques for modelling distributed dynamic railway networks and reasoning about their safety. The research proposed to develop a new railway oriented modelling framework with proof rules which could capture a cyber-physical nature of the heterogeneous railway networks. Then we presented an ongoing work on modelling a distributed railway signalling system which is necessary in order to explore common distributed railway design patterns and also deduce invariants for heterogeneous railway networks. In the following months we aim to complete this model and focus on hybrid framework part for modelling and reasoning about heterogeneous railway networks.