Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Despite the quite long story of successful application of formal methods in the railway domain, it cannot be yet said that a single mature technology has emerged. The evolution of the technology of railways signaling systems in this long term has had a strong influence on the way formal methods can be applied in their design and implementation, and at the same time important advances had been also achieved in the formal methods area.

The evolution of railways signalling systems has seen railways moving from a protected market based on national railway companies and national manufacturers to an open market based on international standards for interoperability, in which systems of systems are providing more and more complex automated operation, but maintaining, and even strengthening, demanding safety standards.

The scope of the formal methods discipline has enlarged from the methodological provably correct software construction of the beginnings to the analysis and modelling of increasingly complex systems, always on the edge of the ever improving capacity of the analysis tools, thanks to the technological advances in formal verification of both qualitative and quantitative properties of such complex systems.

In spite of these advances, the verification of complex railway signalling systems is still a main challenge and an important percentage of the cost in the development of these systems. We can maybe speak of a “grand challenge”, that is, where progress with regards to this challenge would contribute to advance the whole field of verification of complex computer-based systems.

The thesis we will put forward in this talk is that the complexity of future railway systems of systems can be addressed with advantage only by a higher degree of distribution of functions on local interoperable computers - communicating by means of standard protocols - and by adopting a multi-level formal modelling suitable to support the verification at different abstraction levels, and at different life-cycle times, of the safe interaction among the distributed functions. A vision that can make railway applications closer to the emerging field of the so called cyber-physical systems, made of collaborating computational elements controlling physical entities, that will pervade the human activities in the future.

The paper is organized as follows: after recalling the first applications of formal methods to railway signalling equipments in Sect. 2, we briefly introduce model checking and direct code verification in Sects. 3 and 4 respectively. Section 5 discusses the Model Based development approach, also in connection with the CENELEC safety guidelines. Section 6 discusses a series of challenges put forward by the evolution of the domain. Section 7 discusses the possibility, offered by recent advance in the quantitative evaluation technology, to model and evaluate dependability issues as well. Section 8 concludes the paper.

2 Early Applications of Formal Methods to Railway Signalling

In its more general definition, the term formal methods encompasses all notations having a precise mathematical semantics, together with their associated analysis and development methods, that allow to describe and reason about the behaviour and functionality of a system in a formal manner, with the aim to produce an implementation of the system that is provably free from defects – although actually the aim of a complete proof can be only partially achieved, for example because correctness of the actually executed code requires the proof of correctness of the compiler as well, which is not normally available.

A general but comprehensive definition is given by the safety standard Def Stan 00–55 [47], where a formal method is said to be composed of the following three ingredients: “a software specification and production method that comprises:

  • a collection of mathematical notations addressing the specification, design and development phases;

  • a well-founded logical inference system in which formal verification proofs and other properties can be formulated;

  • a methodological framework within which software can be developed from the specification to the implementation in a formally verifiable manner.”

Railway signalling has been traditionally considered as one of the most fruitful areas of intervention for formal methods [23]. Already since the end of the eighties, a series of railway signalling products have benefited from the application of the B formal method [1] in the design process. This method targets software development from specification through refinement, down to implementation and automatic code generation, with formal verification at each refinement step: writing and refining a specification produces a series of proof obligations that need to be discharged by formal proofs. The B method is accompanied by support tools, which include tools for the derivation of proof obligations, theorem provers, and code generation tools. Hence it fits perfectly the definition of formal method that we have cited above.

The SACEM system for the control of a line of Paris RER [16] is the first acclaimed industrial application of B. Since then, B has been adopted for many later designs of similar systems by Matra (now part of Siemens). One of the most striking application has been the Paris automatic metro line 14: the report on the verification activities in [6], tells that indeed several errors were found and corrected during proof activities conducted at the specification and refinement stages. By contrast, no further bugs were detected by the various testing activities at system level that followed the code generation and integration.

The success of B has had a major impact in the sector of railway signalling by influencing the definition of the EN50128 guidelines [20], issued by the European Committee for Electrotechnical Standardization (CENELEC). These guidelines address the development of Software for Railway Control and Protection Systems, and constitute the main reference for railway signalling equipment manufacturers in Europe, with their use spreading to the other continents and to other sectors of the railway (and other safety-related) industry. The EN50128 document is part of a group of documents regarding the safety of railway control and protection systems, in which the key concept of Safety Integrity Level (SIL) is defined, a number ranging from 0 to 4, where 4 indicates a high criticality, 0 gives no safety concern. The SIL is actually a property of the system, related to the damage a failure of the system can produce, and is usually apportioned to subsystems and functions at system level in the preliminary risk assessment process. Also software functions are associated a level (Software SIL); assigning different SILs to different components helps to concentrate the efforts (and therefore the production costs) on the critical components. The EN50128 guidelines however dictate neither a precise development methodology for software, nor any particular programming technique, but classify a wide range of commonly adopted techniques in terms of a rating with respect to the established SIL of the component. Formal methods are rated as highly recommended for the software requirements specification and software design of systems/components with the higher levels of SIL. Formal proof is also highly recommended as a verification activity. The norm however does not dictate any process in which formal methods take a role, but just gives a list of the most common formal methods at the time of writing. Moreover, other combinations of highly recommended techniques, not including formal methods can be chosen: for example, testing combined to full traceability to requirements is a compliant, commonly used, approach to software verification of highest SIL software components.

Anyway, we can see that B-based methods have not so spread in railway software development, as one could have expected by their impressing record of successful applications in the domain. Indeed, methods like B end up to require a substantial change to the traditional software development life cycle already adopted in an industrial setting. The related investment cost is often perceived as not justified in the light of the forecast benefits, and their adoption is not welcome both to managers, and to development teams more skilled in programming than in theorem proving. On the other hand, accompanying the traditional life cycle with formal specification and verification techniques has often proved to have less impact and has gained a better acceptance by managers and development teams pushed by the need to show compliance to CENELEC norms, sometimes as a tradeoff with respect to the promise of a full formal proof of correctness achievable with a method that encompasses the whole development, like B.

The SACEM and similar systems are examples of ATP/ATC (Automatic Train Protection/Control) systems that guarantee safe speed and braking control for trains, along the line, where the main safety criterion is to guarantee that two trains travelling at speed in the same direction stay a safe distance apart.

The basic concept in ATP/ATC is the braking curve: safety is guaranteed if the speed is always below the line, should the speed be above the line, emergency braking is enforced. These systems, which accommodate both train distancing and protection of singular points of the line, are constituted by on-board components that receive information from wayside components. In the early computer-based systems of this kind, this communication is rather simple and occurs at specific points of the line. As a consequence, the safety enforcing algorithms were not excessively complex and were directly amenable to formal specification.

The other main class of signalling systems, that of interlocking, exhibits instead complex logic relations and event-based behaviour that were not conveniently encoded in assertion-centric formalisms as the plain B method (and indeed this class has prompted evolutions of B itself).

3 Railway Signalling Equipments - The Model Checking Advent

Model checking [14] has raised the interest of many railway signalling industries, being the most lightweight from the process point of view, and being rather promising in terms of efficiency.

Interlocking systems have immediately called for a direct application of model checking, since their safety properties are quite directly expressed in temporal logic, and their specifications by means of control tables can be directly formalized. An interlocking is the safety critical system that controls the movement of the trains in a station and between adjacent stations. The interlocking monitors the status of the objects in the railway yard and allows or denies the routing of the trains in accordance with safety and operational rules. In most computer based interlocking systems the instantiation of such rules on a station topology is stored in a control table, that is iteratively read and executed by an appropriate interpretation engine.

However, due to the high number of boolean variables involved, automatic verification by model checking of sufficiently large stations typically incurs in combinatorial state space explosion problem. The first applications of model checking have therefore attacked portions of an interlocking system [7, 29], but even recent works [27, 48] show that routine verification of interlocking designs for large stations is still a challenge. SAT-based Bounded Model Checking [8] is currently the most promising option and is used in industrial solutions.

We leave the discussion of this particular application domain and the related extensive bibliographic references to the companion papers [9, 32, 39, 40].

We can observe that model checking is used in this context as a side verification and validation activity inside a more traditional, and domain dependent, development cycle: a completely formal development cycle along the definition of formal methods given above is not respected, but the approach concentrates on the formal verification of the most sensitive and complex kernel of such systems.

On the basis of such extensive usage in this domain, Model checking has indeed gained a mention in the 2011 revision of the EN50128 guidelines [21], as one of the recommended formal methods.

4 Code Formal Verification

The cited guidelines [21] recognize that most of the industrial application of model checking regards hardware design verification. Direct application of model checking to software code verification is considered to be still a challenge, because the correspondence between a piece of code and a finite state model on which temporal logic formulae can be proved is not immediate: in many cases software has, at least theoretically, an infinite number of states, or at best, the state space is just huge. This discipline, commonly named software model checking [41], has in the last years developed to gain a spread application in several industrial domains; some software model checkers, such as CBMC [12], hide the formality to the user by providing built-in default properties to be proven: absence of division by zero, safe usage of pointers, safe array bounds, etc. On this ground, such tools are in competition with tools based on Abstract Interpretation, that we discuss next. It is likely that software model checking will in the next years gain a growing industrial acceptance also in the railway domain, due to its ability to prove the absence of typical software bugs, not only for proving safety properties, but also to guarantee correct behaviour of non safety related software. An interesting application of CBMC to automatic test generation in the railway domain is reported in [3].

Another technique for code formal verification is the assertion-based formal proof: the code is annotated at various locations with assertions that predicate over variables’values. The assertions are used as pre- and post- conditions to various operations in the code. The proof consists of showing that the execution of the included program fragment when preconditions hold, implies that post-conditions hold when the fragment terminates.

Assertion-based formal proof, referred as highly recommended in the 2011 revision of the EN50128 guidelines [21], finds its most prominent industrial application within the SPARK subset of the Ada language and associated proof tools, which in the railway sector is considered inside the OpenETCS initiative [43].

Abstract interpretation is based on the theoretical framework developed by Patrick and Radhia Cusot in the seventies [15]. However, due to the absence of effective analyses techniques and to the lack of sufficient computer power, only after twenty years software tools have been developed to support it so that applications of the technology at industrial level could take place. The focus of the application of the technology is mainly on the analysis of source code for runtime error detection, which means detecting variables overflow/underflow, division by zero, dereferencing of non-initialized pointers, out-of-bound array access.

Since the correctness of the source is not in general decidable at the program level, the tools implementing abstract interpretation work on a conservative and sound approximation of the variable values in terms of intervals, and consider the state space of the program at this level of abstraction. The problem boils down to solve a system of equations that represent an over-approximate version of the program state space. Finding errors at this higher level of abstraction does not imply that the bug also holds in the real program. The presence of false positives after the analysis is actually the drawback of abstract interpretation, that hampers the possibility of fully automating the process. Uncertain failure states (i.e., statements for which the tool cannot decide whether there will be an error or not) have normally to be checked manually and several approaches have been put into practice to automatically reduce these false alarms. The process developed at General Electric Transportation Systems [28] for the verification of railway signalling software includes abstract interpretation analysis, employing the Polyspace tool [17] and handles false positives through a step of abstraction refinement.

Abstract interpretation is not explicitly listed among recommended techniques in CENELEC 50128, although static analysis is, and most sophisticated static analysis tools include abstract interpretation. It is not often referred as a formal methods either, although it provides the three ingredients of a formal method of the Def Stan 00–55 definition. In our opinion, this technique is one way the decades of research on formal methods have infiltrated industrial embedded software development.

5 Model Based Design and the CENELEC Guidelines

The adoption of modelling technologies into the different phases of development of software products is constantly growing within industry. Designing model abstractions before getting into hand-crafted code helps highlighting concepts that can hardly be focused otherwise, enabling greater control over the system under development.

Indeed, the 2011 revision of EN50128 recognizes the usefulness of modelling at several stages of the development cycle. EN50128 lists recommended techniques in a series of tables that follow the different stages of the software development cycle. In the 2011 version we see that there are two techniques that are cross-cutting over the main development phases, namely Formal Methods and Modelling. Indeed, both can be adopted as a paradigm to shape the complete software development cycle. The example of the B method is a good representative of the former, although the list of formalisms cited in the standard include other assertional techniques, such as Z and VDM, process algebras, algebraic specification, temporal logic and model checking.

About modelling, the norm lists a series of techniques that include formally based ones, such as Finite State Machines, Statecharts and Petri Nets. In the norm, the term modelling refers mainly to the description of some aspects of a system in support for its development and verification, but a recent trend in industry, and in particular in the industry of embedded systems, has seen modelling as a way of defining a model-based development cycle. This is particularly true in the case of embedded safety-critical applications industry which has been the first in line to adopt so called Model Based Development or Model Based Design (MBD), that employs modelling and simulation platforms like Simulink/Stateflow (toolboxes of Matlab from Mathworks) [46] or the SCADE Suite (from Esterel Technologies) [45] for lower-level design, to support the development of embedded applications. The adoption of automatic code generation, or automatic test cases generation, is also growingly followed in software production for safety critical systems. A typical notation for modelling the discrete behaviour of a system is that of Statecharts, hierarchical extended finite state machines: introduced by Harel [30], they have specialized in various dialects, supported by formal specification environments: among the most adopted commercial environments we can find the mentioned Stateflow and SCADE. UML State Diagrams as well are essentially Statecharts, and are supported by several free and commercial tools.

One example from the railway signalling domain is the model based development cycle defined by General Electric Transportation Systems (GETS), The company employed modelling first for the development of prototypes [4] and afterwards for requirements formalization and automatic code generation [24]. The production process for Automatic Train Protection (ATP) Systems has been based on modelling by means of Simulink/Stateflow descriptions. Extensive simulation of Stateflow diagrams with scenarios taken from the field was conducted, aiming at 100 % structural coverage of the diagrams’states. After automatic code generation from the diagrams, back-to-back model/code testing is conducted automatically with the same simulation scenario. Back-to-back testing has the main aim of confirming that the code generator has not introduced flaws in the code [26].

The kind of testing described above is one of the techniques that are encompassed by so called Model Based Testing (MBT). Another common MBT technique is Automatic Test Generation (ATG) in which test cases are automatically generated from the model in order to guarantee an extensive coverage of the system functionalities as described by the model.

The SCADE suite as well has been widely adopted in the railway field: its usage is reported by several companies. The activities that are supported by the suite are essentially the same as for Stateflow, but one point in favour of SCADE is that the suite includes a C Code Generator certified according the EN50128 guidelines. This allows to eliminate from the development process those steps that in the previous example were aimed at guaranteeing safety of the code generator.

Model Based Design is often not numbered among formal methods, essentially for one of two main reasons (or for both): the first is that some modelling frameworks are not based on a formal semantics, and they allow designers to write non precise or non completely defined models (that is, the mathematical notations ingredient is missing); the second reason is that in many cases no formal proof technique is given to demonstrate that the code is a correct concretization of the abstract specifications (that is, the inference system ingredient is missing). This is not always the rule, and indeed models can be made precise by using semantically sound description formalisms. Formal verification of models can be conducted with the aid of model checking techniques, as it happens for the two main tool frameworks mentioned above, that both include Design Verifier, a SAT based model checker, especially when one wants to verify that given safety properties are satisfied.

Hence, having a formally based modelling formalism in which system functions are described and proved to satisfy given properties, with automatic code generation, by means of a certified code generator, is another way the three ingredients of formal description, formal proof and software production, are assembled in a full formal method [25].

6 New Challenges

Railway signalling is a rapidly evolving domain, with different evolution driving forces, such as:

  • the quest for more performant equipment in order to increase the capacity of lines;

  • the need of decreasing operational costs;

  • the European interoperability regulations;

  • the evolution of the railway market;

  • the technology improvements, which include contrasting supporting features, such as increasing computing power, which allows more functions to be concentrated in one platform, and more performant (wireless) communication, which favours distribution of functionalities over several distributed computing units.

In the following sections we briefly discuss these different evolution lines, from the point of view of the application of formal methods.

6.1 Evolution of ATP Systems: ETCS and CBTC

One major innovation in ATP systems is the shift from Fixed block to Moving block. In the Fixed block a line is topologically segmented into blocks, and appropriate sensors tell whether a block is free or not. The occupancy of the leading train includes the whole block which the train is located on; the following train is allowed to move only up to the last unoccupied block’s border. In the Moving block, the train position and its braking curve is continuously calculated by the trains, and then communicated via radio to the wayside equipment, which establish protected areas for each train, each one called Limit of Movement Authority (LMA), or simply Movement authority (MA), up to the nearest obstacle (tail of the train in front).

The ERTMS/ETCS (European Rail traffic Management Systems / European Train Control System) [18] has been proposed to become the single train control system for the future transeuropean railway network. The project plans to gradually install the ERTMS/ETCS equipment side by side to the traditional national equipment, also exploiting the three successive ERTMS/ETCS levels, with increasing degree of information flowing from way-side to on-board equipment. In level 2 and 3, GSM-R (GSM radio communication specific to the railway industry) is adopted to continuously transfer information to the train on the status of the line ahead. Moving block is adopted in level 3, of which anyway no implementation currently exist yet.

ERTMS/ETCS makes use of standardized components (European Vital Computer on board, Radio Block Center, Eurobalise,...) and protocols (Euroradio), produced by a consortium of the main European signalling manufacturers. Specifications issued by ERTMS/ETCS are structured as a natural language requirement document, including tables, state diagrams and sequence charts to add some formality.

Several formal modelling and verification studies have been conducted regarding ETCS protocols and components; the most systematic approach to the formalization of ETCS natural language requirements has been the EuRailCheck project by the European Railway Agency [11] where UML diagrams augmented with constraints in a Controlled Natural Language have been exploited to produce formalized requirement fragments. Automated validation analysis of such fragments has then been possible by means of a customization of the NuSMV model-checker. The OpenETCS project [31] is now working at providing a full, open formal specification of ETCS protocols and components.

In the case of ETCS, the attention of the formal methods community has shifted from the consolidated train control logic (the braking curve principle), to the safety and real-time performance of radio-based control, which is going to be the sole mean by which the conditions of the track ahead are communicated to the train, since even signals will no more be present on the line [19].

In the domain of metro signalling equipments, An emerging standard is CBTC (Communication-Based Train Control) [44], where the train’s exact position (which is not a trivial issue to determine), is continuously communicated to the Radio Block Center (RBC) via GSM-R, which in its turn continuously communicates the LMA to the following train. So CBTC can provide a continuous automatic train protection as well as improved performance, system availability and operational flexibility. CBTC is mostly installed in (automatic) metro lines, and includes not only ATP functions, but other higher level functions as well, such as ATO (Automatic Train Operation), ATS (Automatic Train Supervision), and interlocking. As opposed to the interoperability-oriented ETCS systems, CBTC is standardized at a very high level of abstraction: international standards only define systems functions and subsystems at a very high level [37]. Every CBTC vendor has its own solutions: the trend is to provide turnkey, proprietary and closed systems, facilitated by the fact that metros are closed environments. This may produce vendor lock-in phenomena, especially with respect to long-term maintenance.

CBTC can be classified as a Systems of Systems (SoS), that is, large-scale systems composed from the combination of several, often pre-existing, communicating systems to provide some functionality that cannot be provided by a single system. The research on SoS engineering needs to address the challenges posed by the increasing complexity of the requirements mapped to the complexity of the underlying constituent systems, in particular for what concerns formal verification of overall safety properties.

6.2 Integrating ATC/ATP and Interlocking Systems

The interface between ATC/ATP systems, which span over a full length line, and Interlocking Systems, which are mostly concentrated within a station, is subject to several solutions and studies. A common choice at this regard is to define a proper interface between the two separate systems. The INESS project has addressed the formal definition of the interface of ERTMS with interlocking systems [35].

An approach that exploits a tighter integration is to define a chain of distributed ATP components that act both as a sensor (axle counter) for occupancy of a section and as control over occupancy of next section to achieve fixed block distancing. Interlocking functions on (small) stations insisting on some section are included in the interested component.

An opposite trend is to concentrate in a multistation interlocking many functions, either ATP on a line, interlocking for the interested stations and ATS, in one centralized computer or network of computers.

We want also mention the formal verification process adopted by Ansaldo STS, that include Software model checking [13], applied to the ERTMS/ETCS RBC system that control train separation on a section of line that includes points (such as in a forking junction), and hence include interlocking functions on a small number of entities.

6.3 The Evolution of the Market

At the dawn of formal methods introduction in the railway signalling arena the market was a protected one, based on national railway companies and national manufacturers. Nowadays, the market is open and the national manufacturers have been merged in large multi-national companies.

However, most experiences in formal method applications to even complex systems have been carried on till now by a single manufacturer, or single railway operator on single systems.

New challenges are provided by the quest for interoperability. For what concerns interoperability of trains across national borders, a full solution by ERTMS/ETCS is still far from sight. Currently, and for many years from now on, an interoperable train travelling over Europe should be able to switch from ETCS lev. 2 to many national systems, until a complete deployment of ETCS is accomplished on all lines that maybe of interest for the market of train transport (a complete deployment that, for economic reasons, it is quite unlikely in the next future for secondary lines). In principle, it could be cheaper to equip trains with Multistandard systems that adopt well-defined (that is, formalized) transition procedures.

On the other hand, the partial ETCS implementation can raise the risk of new, virtual, barriers to interoperability, As an example, Italy requires all trains running on the national main network to be equipped by SCMT, essentially an ETCS Level 1 ATP. The cost of such equipment has represent an obstacle to trains from other countries to enter Italy; in particular, this is one of the reasons why at the time of writing there is no through passenger railway service between Italy and Slovenia, although the Slovenian infrastructure is fully compatible with the Italian one, for what concerns electric traction power (3kV DC), for historical reasons, and through Intercity trains were running till few years ago.

Interoperability of trains has stressed the standardization of board to ground communication: trains equipped with on-board systems produced by different vendors do travel on infrastructures equipped by different vendors: this is the main target of the standard definition of ETCS. Still, national variants (introduced for special needs) exist that may impede full interoperability across nation borders; moreover, the standard leaves implementation freedom to some other aspects. For example, the (ground-based, fixed) RBC to RBC communication is less strictly standardized: in Italy, the Milano-Bologna and the Bologna-Firenze high speed lines are equipped with ETCS level 2 by different manufacturers. In Bologna, the two lines were connected till recently through the old station, equipped with traditional signalling. Since June 2013, a new through underground station directly connects the two lines; a specific interface, implemented on a dedicated computer, between the last and first RBCs of the two lines, produced by different vendors, was needed to let them communicate.

Lowering costs and closing the standardization gaps are the objective of the openETCS initiative [31], which aims to create a new open standard for formal functional requirement specifications and open proof for ETCS systems.

Vendor lock-in phenomena can be raised also in the case of interlocking systems, for what concerns certification aspects: the configuration and verification process is expensive, monolithic and not easily repeatable. Moreover, certification has to be repeated for every deployed system, since the track layout changes from station to station. Hence, in case of modifications to the layout, reconfiguring the system on a new layout may be very expensive also for small layout changes. The configuration and verification process itself is often proprietary, and therefore an infrastructure company can become locked to the vendor for any modification of the track layout.

6.4 The Evolution of Interlocking Systems

As already said, formal verification of IXL control tables has been studied since years, SAT-based Bounded Model Checking verification currently being the most promising direction. However, control tables are a legacy of the relay-based equipments.

Formal methods, and software design disciplines in general, have inspired a different approach to interlocking design: in the Geographic approach [5] the interlocking logic is made up by composition of small elements (or objects, if the object oriented paradigm is chosen) that take care each of the control of a physical element (point, track circuit, signal), connected by means of predefined composition rules, mimicking the topology of the specific layout. Several interlocking equipments are now developed following this paradigm, that has been followed in the INESS project [35] to provide a full formal UML-based specification.

Pushing further the concept, with the aim to study alternative paradigms for the formal verification of interlocking systems, in [22] a distributed architecture is envisaged: elements of the geographic approach configured as a set of distributed communicating processes: each process controls a given layout element. The route is instead a global notion: a route has to be established by proper cooperation of the distributed elements. The communication among processes follows the physical layout of the station/yard and a route is established by the status of the elements that lie along the route.

Indeed, [33] already made the case for distributing interlocking functions: the concept of [22] can in principle be pushed to the design of a new kind of distributed railway interlocking system. The logic of the interlocking will be fine-grained and distributed on processors deployed at each sensor/actuator, along the track layout, and communicating with the adjacent controllers by means of safe, possibly wireless, communication. This is in contrast to the current systems with centralized logics. Distributed computing elements would autonomously collaborate in order to initialize, configure, monitor and reconfigure - for fault tolerance or in case of modifications to the layout -, without a centralized logic, but still guaranteeing the absolute safety of the train transit through the track layout. There are a number of motivations that can push the technological bar towards distribution for interlockings, such as:

  • Easy deployment and maintenance

  • Plug-and-play reconfiguration

  • Copper-free communication if wireless links are adopted

  • Simpler interface with ERTMS/ETCS or ATP/ATC equipments

  • Vendor lock-in avoidance by means of an open interlocking protocol stack

A so fine-grained distributed interlocking, including configuration and reconfiguration, is not something that is currently in practice nor in the foreseeable future (5–10 years) of the railway industry, but the general trend to distribute intelligence in scattered locations will probably push in this direction. Formal verification that safety guarantees are enforced will play an essential role; this verification will be the basis of the definition of certified plug-in components: if such components are assembled according to a track layout and respecting the interlocking protocol, the entire system safety is guaranteed, hence sparing on costly recertification processes. The future standardisation of the interlocking protocol will aid independence of certification with respect to the interlocking rules of a particular country.

7 Beyond Safety

In the discussion above, we have mostly focused on the ability of formal methods to prove that a given system is safe. However, liveness properties are often of interest as well: at the level of the internal working of an equipment, proving that a particular system is live or responsive is often achieved by testing in the railway industry, not recurring to formal proof, since the higher costs of formal proof are reserved to the safety-related issues, according to safety guidelines. Formal methods can be a more cost effective way to guarantee liveness as well (INESS recommends, for example, livelock and deadlock absence verification [36]).

At the system level, we observe that, as a general principle, railway safety is in the end achieved at the cost of availability: halting trains is the basic form of safety enforcement. As the number of controlling elements increase, safety mechanisms that simply tend to halt trains at any single element failure could easily lower availability, capacity and QoS.

Quantitative modelling at a high abstraction level of the working of the system and of anticipated fault scenario, can be adopted for availability or capacity evaluation. Many works in the railway research literature focused on capacity analysis with the objective of optimizing the use of railway infrastructure, especially in consideration of the growth of the entire transport sector in consequence of globalization of the economy and the increasing integration of the international economies; an overview of several techniques and methodologies can be found, e.g., in [2, 10, 42]. They range from analytical methods, mainly based on mathematical formulae or algebraic expressions, to more complex optimization solutions, e.g. based on heuristics to obtain optimal saturated timetables, to simulation methods. Model-based analysis has been widely applied in the last two decades to assess performance and dependability indicators in the railway domain, exploiting a Markov-chain based modelling, or Petri-net based formalism. The potential of probabilistic model checking in an area still dominated by simulation-based engines has to be evaluated.

Anyway, quantitative analysis is carried on at a higher level of abstraction, namely at the system level, with respect to formal verification of safety, that act on the logic inside a subsystem or on the communication between subsystems. The key is hence to adopt a multi-level modelling approach to address the complexity of a railway system. The ongoing SafeCap project [34] develops modelling techniques and tools for improving railway capacity [38] while ensuring that safety standards are maintained with a multi-level modelling approach.

8 Conclusions

Formal Methods are used for industrial railway signalling applications. The evolution of systems require companies to adopt automatic verification tools to attack their complexity, which makes verification by testing only unfeasible, especially for high SIL systems. The evolution of formal methods and formal verification tools themselves opens new possibilities to tackle the complexity of these systems, not only for safety certification, but also for other dependability issues. Formal modelling can even act as a facilitator for railway signalling innovations.

In the discussion above, we can envisage two main research directions that will need to be pursued in the next year, namely i) multi-level modelling to cope with the increasing complexity of systems and of their dependability requirements and ii) formal description and verification of complex distributed systems of systems. These two directions are not actually orthogonal, but can be seen as two facets of the same vision: only extensive formal description and verification tools will have the potential to master the exponentially growing complexity of railway control applications of the future.