Efficient verification of railway infrastructure designs against standard regulations

Railway construction projects rely heavily on computer aided design (CAD) tools to map out railway station/infrastructure layouts. The various disciplines within a project, such as civil works, track works, signalling, or catenary power lines, work with coordinated CAD models. These CAD models contain a major part of the work performed by engineers, and are a collaboration tool for communication between disciplines. The signalling component layout is worked out by the signalling engineers as part of the design process. Signals, train detectors, switches (also known as points), etc., are drawn using symbols in a 2D geographical CAD model. An example of a layout drawing made by Anacon AS engineers from a CAD model is given in Fig. 1.

Track layout details, which are input for the signalling design, are often given by a separate division of the railway project. At an early stage and working at a low level of detail, the signalling engineer may challenge the track layout design, and an iterative process may be initiated.

An interlocking is an interconnection of signals and switches to ensure that train movements are performed in a safe sequence [42]. Interlocking is performed electronically so that, e.g., a green light (or, more precisely, the proceed aspect) communicating the movement authority required for a train to travel through a station can only be lit by the interlocking controller under certain conditions. Conditions and state are built into the interlocking by relay-based circuitry or by computers running interlocking software. Most interlocking specifications use a route-based tabular approach, which means that a train station is divided into possible routes, which are paths that a train can take from one signal to another. These signals are called the route entry signal and route exit signal, respectively. An elementary route contains no other signals in-between. The main part of the interlocking specification is to tabulate all possible routes and set conditions for their use. Typical conditions include:

The blocks, which may represent things such as chairs, doors, or railway signals, also create the opportunity to store higher-level information in a CAD model, other than the purely geometrical description. For example, if one uses a railway signal block to model a signal in a railway station, a program can count the number of signals in a CAD model.

This idea can be extended by adding any number of attributes to a block. For a railway signal, we can add attributes that describe, e.g., to which track it signals, along with its type, function, and direction. The CAD object database does then not only contain the geometrical objects, such as lines, curves, triangles, cubes, etc., but groups these primitives into higher-level concepts which are closer to the representation that one uses to reason about the actual working of the railway infrastructure.

With a good library of blocks (which we call a symbol library), the engineer can more efficiently build the geometric CAD models which lead to human-readable drawings, but they are also building a machine-readable model of high-level railway concepts. We call this semantic CAD. While this concept is also a part of building information modeling (BIM), BIM also includes many other concepts such as 3D visualization, time (“4D”), and cost (“5D”).

The verification of signalling and interlocking rules requires information about properties and relations between objects, e.g., which signals and signs are related to which track, and their identification, capabilities, and use. This information is better modelled by the railway-specific hierarchical object model railML [40]. In the CAD industry-standard DWG file format, each geometrical object in the database has an associated extension dictionary, where add-on programs may store any data related to the object. Our tool uses this method to store the railML fragments associated with each geometrical object or symbol, see Fig. 2 . Thus, we can compile the complete railML representation of the station from the CAD model.

It is necessary to decide which objects in the CAD model should be associated with which data types, i.e. what attributes should be stored in the symbols. (This is similar to specifying an object’s class in an object-oriented programming language.) To do this, we create an object type description which augments the symbol library with class information. Whenever the user adds a symbol, its data editor is determined by the assigned class, and vice versa: when e.g. a railML object is imported into CAD, its corresponding symbol is inserted in the graphical model.

Besides the CAD model layout, the design of a railway station’s signalling consists also of specifications for the interlocking and train protection (speed control) systems. These specifications are used to build the interlocking controllers and speed controllers, and they model the behavior of the signalling equipment and its interaction with trains. These systems are tightly linked to the station layout.

A formal representation of the interlocking and train protection specifications is embedded in the CAD document in a similar way as for the railML infrastructure data, using the document’s global extension dictionary. Thus, the single CAD document showing the human-readable, geographical layout of the train station also contains a machine-readable model which fully describes both the component layout and the functional specification of the interlocking and train protection systems. This allows analysis of the operational aspects of the train station directly in a familiar editable CAD model. See Fig. 3 for an overview of this architecture.

Logic programming [41] is a family of programming languages based on formal logic. Logic programs are declarative, i.e., they describe properties of the solution of a problem rather than a calculation procedure for finding the solution. This separates the concerns of expressing rules about railway systems from the algorithms required to do automatic analysis. This separation allows one to systematically maintain a large set of rules, and decouple the tool implementation from the set of concepts, rules and expert knowledge that is specific to a railway administration.

We have successfully used the Datalog language [53], a subset of the more well-known Prolog language, for verifying many properties given as technical rules and expert knowledge. It allows concise formulations of railway concepts, and queries can be efficiently calculated.

Ideally, we would like the railway engineers themselves, without much programming education, to be able to create and maintain the set of rules which is used for the verification. This separation of logic and algorithm is a step in this direction, because non-IT experts can work on the rules without considering how the calculations are implemented. However, the strict formalism and subtle semantics of logic programming are still a challenge for an inexperienced programmer. Still, some parts of the maintentance work on the railway properties can be performed without deep knowledge of logic programming, for the following reasons:We do, however, concede that Datalog programming in general (specifically, at the level required for writing regulation properties from scratch) is outside the competence of a railway engineer. A higher-level domain-specific language including relevant constructs for a railway signalling design knowledge base could improve the likelihood of railway engineers being successful in creating and maintaining the regulations. Even more, this language could allow each company and each engineer to experiment with encoding different design heuristics and expert knowledge to see the effects on the verification and the design. Our planned future work (see Sect. 8.2) includes defining such a language and also on using a controlled natural language syntax to improve ease of comprehension [30].

We envision that a common rule base would be exchanged between all engineers working with a railway administration, and that the rule base would be worked out partly by software experts, partly by railway experts. Also, the rule base should be fairly constant, like the regulations, requiring an update frequency of perhaps once per year.

Declarative logic programming is a programming language paradigm which allows clean separation of logic (meaning) and computation (algorithm). This section gives a short overview of Datalog concepts. See [1, 41, 53] for more details. In its most basic form Datalog is a database query, as in the SQL language, over a finite set of atoms which can be combined using conjunctive queries, i.e. expressions in the fragment of first-order logic which includes only conjunctions and existential quantification.

Conjunctive queries alone, however, cannot express the properties needed to verify railway signalling. For example, given the layout of the station with tracks represented as edges between signalling equipment nodes, graph reachability queries are required to verify some of the rules. This corresponds to computing the transitive closure of the graph adjacency relation, which is not expressible in first-order logic [28, Chap. 3]. Extending conjunctive queries by allowing recursive predicate definitions is a common way to mitigate the above problem while preserving decidability and polynomial time complexity.

The Datalog language is a fragment of first-order logic extended with recursive predicate definitions, which are evaluated by computing least fixed points. We define the Datalog language as follows: Terms are either constants (atoms) or variables. Literals consist of a predicate p with a certain arity n, along with terms corresponding to the predicate arguments, forming an expression like \(p({\overrightarrow{a}})\), where \({\overrightarrow{a}} = (a_1,a_2,\ldots ,a_n)\). Clauses consist of a head literal and one or more body literals, such that all variables in the head also appear in the body. Clauses are written aswith \(\bigcup _{1\le i \le k}{\overrightarrow{x_{i}}} = {\overrightarrow{x}}\) and \(\bigcup _{1\le i \le k}{\overrightarrow{y_{i}}} = {\overrightarrow{y}}\). Datalog uses the Prolog convention of interpreting identifiers starting with a capital letter as variables, and other identifiers as constants, e.g., the clausehas the meaning ofClauses without body, which cannot then contain any variables, are called facts, those with one or more literals in the body are called rules. No nesting of literals is allowed. However, recursive definitions of predicates are possible. For example, let edge(a, b) be a graph edge relation between vertices a and b. Graph searches can now be encoded by making a transitive closure over the edge relation:In the railway domain, this can be used to define the connected predicate, which defines whether two objects are connected by railway tracks:Here, the connection predicate contains switches and other connection types. Further details of relevant predicates are given in the sections below.

The Datalog logic in its simplest form does not contain any notion of negation, which is often crucial for practical applications. A common feature of Datalog implementations is to extend the logic with negation using negation as failure semantics. This means that negation of predicates in rules is allowed with the interpretation that when the satisfiability procedure cannot find a model, the statement is false. To ensure termination and unique solutions, the negation of predicates must have a stratification, i.e. the dependency graph of negated predicates must have a topological ordering. This means that whenever a rule with a negated predicate is evaluated, the negated predicate must already be completely evaluated, so that the absense of a term from the predicate can be known definitely (see [53, Chap. 3] for details). In practice, this requirement is often easy to fulfill.

Datalog is sufficiently expressive to describe static rules of signalling layout topology and interlocking. For geometrical properties, it is necessary to take sums and differences of lengths, which requires extending Datalog with arithmetic operations. For our prototype tool, we have used XSB Prolog as the logic programming system, which supports both Datalog with negation-as-failure, and arithmetic. A more expressive language is required to cover all aspects of railway design, e.g. capacity analysis and software verification, but for the properties in the scope of this paper, a concise, restricted language which ensures termination and short running times has the advantage of allowing tight integration with the existing engineering workflow.

With Datalog as specification language, we build a knowledge-base system to perform the verification. A knowledge-base system consists of a set of facts and rules, along with an inference engine which answers queries by applying logical inference rules. For an introduction to knowledge-base systems in general, see [53, Chap. 3] or [46, Chap. 8 and 12]. We give here an overview of how we encode railway signalling properties as Datalog predicates, which in turn may be automatically checked for consistency. In our verification tool, we organize our knowledge base in the following manner:Each of these aspects are described in more detail below.

Derived concepts are properties of the railway model which can be defined independently of the specific station. A library of these predicates is needed to allow concise expression of the rules to be checked.

With the input documents represented as facts, and a library of derived concepts, it remains to define the technical rules to be checked. All technical rules presented herein are based on the Norwegian infrastructure manager’s regulations.⁴

Some examples of technical rules representing conditions of the railway station layout are given below.

Property 1 may be represented in the following way:The stationBoundary predicate contains objects which represent the boundaries of a station model. For models which contain a single station, which is the common use case for our CAD prototype application, the stationBoundary can be taken to be the model boundary. Note that the station boundary is usually not the same as the station border, which is defined by regulations.Checking for rule violations can be expressed as:which in Datalog query format becomes ruleViolation 1 (B,S)?.

This property is represented as follows:

This property can be elaborated into the following rules:A basic property of tabular interlockings is that each consecutive pair of main signals normally has an elementary train route associated with it, i.e.:

This can be represented as follows:This type of rule is not absolutely required for a railway signalling design to be valid and safe. Some rules are hard constraints, where violations may be considered to be errors in the design, while other rules are soft constraints, where violations may suggest that further investigation is recommended. This is relevant for the counterexample presentation section below.

Property 5 can be represented as follows:The train detectors in the trainDetectors predicate are in our prototype usually axle counters, as these are the preferred train detection method for newer construction projects. The most common alternative to axle counters are track circuits, which are delimited by isolated joints in the tracks. The property encoding above only assumes that detection section delimiters can be used to derive detection sections, and can thus be adapted to layouts using track circuits.

The following objects can give flank protection:An example situation is shown in Fig. 5. While the indicated route is active (A to B), switch X needs flank protection for its left track. Flank protection is given by setting switch Y in right position and setting signal C to stop.

Property 6 can be elaborated into the following rules:

When rule violations are found, the railway engineer will benefit from information about the following:Also, classification of rules based on e.g. discipline and severity may be useful in many cases. In the rule databases, this may be accomplished through the use of structured comments, similar to the common practice of including structured documentation in computer programs, such as JavaDoc (see Fig. 7 for an example of how we do this). A program parses the structured comments and forwards corresponding queries to the logic programming solver. Any violations returned are associated with the information in the comments, so that the combination can be used to present a helpful message to the user. We implemented a prototype CAD add-on program for Autodesk AutoCAD (see Fig. 8 for a screen-shot).

The rules concerning signalling layout and interlocking from Jernbaneverket ¹⁰ described above have been checked against the model (i.e., railML representation) of the Arna-Fløen project, which is an ongoing design project in Anacon AS (now merged with Norconsult AS). Each object was associated with one or more construction phases, which we call phase A and phase B, which also corresponds to two operational phases. The model that was used for the work with the Arna station (phase A and B combined) included 25 switches, 55 connections, 74 train detectors, and 74 signals. The interlocking consisted of 23 and 42 elementary routes in operational phase A and B respectively.

The Arna station design project and the corresponding CAD model has been in progress since 2013, and the method of integrating railML fragments into the CAD database, as described in Sect. 5, has been in use for more than one year. Engineers working on this model are now routinely adding the required railML properties to the signalling components as part of their CAD modelling process.

This allowed a fully automated transfer of the railML station description to the verification tool. Several simplified models were made also for testing the correct functioning of the concept predicates and rule violation predicates.

The rule collection consisted of 37 derived concepts, 5 consistency predicates, and 8 technical predicates. Running times for the verification procedure can be found in Table 2.

The tight integration into the CAD program and, as such, into the engineer’s design process, creates the demand for fast re-evaluation of all conclusions upon small changes to the railway designs.

Usually, engineers start with an empty or draft design and add/change one object at a time. The performance figures presented in Table 2 show that the current implementation is well acceptable for “one-shot” validation even for realistic designs with running times in the range of seconds. However, it is not fast enough to smoothly and transparently be integrated such that it can automatically rerun the complete verification for each small change. Running times below one second can change the user’s perception of the tool from being a separate verification process to a continuous background check. This level of performance requires other measures to be taken, especially when considering that station models can be larger than our case study, and that the regulations rule base would need to grow larger to become more useful.

An alternative approach that promises to be more efficient is incremental verification: instead of solving logic programs from scratch for each verification run, it tries to materialize all consequences of the base facts and then maintains this view under fact updates. Incremental verification is further discussed in Sect. 7 below.

Datalog systems use rules to derive a set of consequences (intentional facts), from a given set of base facts (extensional facts). Typically, Datalog systems use a bottom-up (or forward-chaining) evaluation strategy, where all possible consequences are materialized [53, Chap. 3] [1, Chap. 13]. This simplifies query answering to just looking up values in the materialization tables. Any change to the base facts, however, will invalidate the materialization. Several approaches have been suggested to reduce the work required to find a new materialization after changing the base facts.

First, if considering only addition of facts to positive Datalog programs, i.e. without negation, then the standard semi-naive algorithm [53, Chap. 3] [1, Chap. 13] is already an efficient approach, as it correctly handles additions to the materialization in an incremental manner. The real challenge is due to non-monotonic changes, i.e., when removing facts appearing positively in rules or adding facts appearing negatively in rules. Non-monotonicity is essential in our railway infrastructure verification rules. Graph reachability is prominent in many of the regulations for railway signalling, so efficiently maintaining rules involving transitivity is also essential.

Some algorithms, such as truth maintenance systems [9], work by storing more information (in addition to the logical consequences) about the supporting facts for derived facts, so that removal of supporting facts may or may not remove a derived fact, depending on whether the support is still sufficient. This allows efficient removal of facts, at the cost of requiring more time and memory for normal derivations. Inspired by the truth maintenance systems of Doyle [9], the XSB Prolog system implements incremental tabling [51] by keeping such sets of supporting facts in memory. Figure 9 shows deduced facts for a graph reachability query. In this case, whenever there are several paths connecting a pair of vertices of the graph, the reach fact for the two vertices is deduced in several ways. In the approach taken in XSB Prolog, different sets of facts that independently prove a derived fact are stored in tables. Whenever changes are made to base facts, the sets of supporting facts can be removed, and as long as the set is not emptied, the derived fact still holds.

Another class of algorithms, working without additional “bookkeeping”, can be more efficient if the re-evaluation of sets of facts is relatively easy compared to re-materializing all facts. The Propagation-Filtering algorithm [19] works on each removed fact separately, propagating it through to all rules which depend on it, while also after each step of the propagation performing a query for alternative support which would end the propagation. In contrast, the Delete-Rederive (DRed) algorithm [18] is rule-oriented and works on sets of facts, first over-approximating all possible deletions that may result from a change in base facts, then re-deriving any still-supported facts from the over-deleted state before finally continuing semi-naive materialization on newly added facts.

An example where the DRed algorithm is less efficient is graph reachability, which can be encoded on the following form:Figure 10 shows key differences in update approaches for the example of a graph reachability from a given node.

Recently, the Forward/Backward/Forward (FBF) algorithm [37] used in RDFox improved the DRed algorithm in most cases by searching for alternative support (and caching the results) for each potentially deleted fact before proceeding to the next fact. Notably, this method performs better on rules involving transitivity, as deletions do not propagate further than necessary.

This method is used in the Semantic Web tool RDFox,¹¹ which has a high performance on multicore processors with in-memory databases. We are considering RDFox as an alternative candidate for the back end of our incremental railway infrastructure verification procedure.

This section summarizes a survey of tools first presented in [32], and describes tools that feature incremental evaluation and Datalog, and which have the maturity required for industrial applications. The logic programs for our verification make use of recursive predicates, stratified negation, and arithmetic. Therefore, we pay particular attention to tools that at least satisfy these needs. In addition, we are looking for high performance on relatively small (in-memory) data sets, so light-weight library-style logic engines are preferred. High-performance distributed “big data” type of tools have less value in this context.

Many other Datalog tools are available (around 30), few of them supporting incremental evaluation. An overview and our brief evaluation of them can be found in the technical report [34], and a more general overview of Datalog tools can be found in the Wikipedia page.¹²

Table 3 compares the running time and memory usage for the verification case study of Arna station presented in Sect. 6, extended to use the incremental capabilities of XSB Prolog. The extra bookkeeping required in XSB to prepare for incremental evaluation requires more time and memory than non-incremental evaluation, so we include both non-incremental and from-scratch incremental evaluation in the table for comparison. We show how updates can be calculated faster than from-scratch evaluation by moving a single object (an axle counter) in and out of a disallowed area near another object (regulations require at least 21.0 m separation between train detectors). XSB has a configurable mode for reducing the memory usage in its incremental tabling, by abstraction methods. Without using XSB’s abstraction methods, the case study verification uses over 2 GB of memory. So, for any hope of handling larger stations on a standard laptop or workstation, this must be reduced. We were not able to reduce memory usage in this case study using the abstraction methods in XSB (version 3.6.0).

While currently none of the tools seem to satisfy all conditions we hoped for in our integration, notably efficiency, but also maturity and stability, it should also be noted that the need for incremental evaluation has been identified by the community not only as theoretically interesting, but also as of practical importance. The RDFox developers aim to support incremental updates of higher-arity predicates in a later version. The XSB project has made efforts to improve its memory usage, so future versions might become feasible for our use. If reducing the memory usage would require adapting a Datalog algorithm (such as DRed), then XSB’s unrestricted Prolog might be a challenge. A different approach would be to extend another efficient Datalog tool, such as Soufflé¹³ to do incremental evaluation, which could require a significant effort.

In our CAD-integrated tool, the verification results would be updated after each incremental change made to the model (similar to how a programming IDE shows errors while typing), so the somewhat increased initial baseline verification time is unproblematic. However, we have not actually put incremental methods into use in our prototype tool because no incremental Datalog tools were found to be mature enough.

Railway control systems and signalling designs are a fertile ground for formal methods. See [3, 12] for an overview of various approaches and pointers to the literature, applying formal methods in various phases of railway design. For a slightly more dated state-of-the-art survey, see [22]. In particular, safety of interlockings has been intensively formalized and studied, using for instance VDM [16] and the B-method, resp. Event-B [27]. Model checking has proved particularly attractive for tackling the safety of interlocking, and various model checkers and temporal logics have been used, see e.g. [7, 10, 17, 35, 43, 56]. Critically evaluating practicality, [13] investigated applicability of model checking for interlocking tables using NuSMV or Spin, two prominent representatives of BDD-based symbolic model checking, respectively explicit state model checking. The research shows that interlocking systems of realistic size are currently out of reach for both flavors of general purpose model checkers. To mitigate the state-space explosion problem, [21] uses bounded model checking [8] for interlockings. Instead of attempting an exhaustive coverage of the state-space, symbolically or explicitly, bounded model checking analyses (the behavior of) a given system only up to a given bound (which is raised incrementally in case analyzing a problem instance is inconclusive). This restriction allows to use SAT solving techniques in the analysis. The paper uses a variant of linear temporal logic (LTL) for safety property specification and employs so-call k-induction. The work of [55] investigates how to exploit domain-specific knowledge about interlocking verification to obtain good variable orderings when encoding the systems to be verified in a BDD-based symbolic model checker. An influential technology is the tool-based support for verified code generation for railway interlockings from Prover AB Sweden [5]. Prover is an automated theorem prover, using Stålmarck’s method [50] of tautology checking.

Also logic (programming) languages, like Prolog or Datalog, have been used for representing and checking various aspects of railway designs. For the verification of signalling of an interlocking design [24] uses a Prolog database to represent the topology and the layout, where for the verification, the work uses a separate SAT solver. Similarly, the work of [38, 39] uses logic programming for verification of interlocking systems. In particular, the work uses a specific version of so-called annotated logic, namely annotated logic programs with strong negation (ALPSN). In general and beyond the railway system domain, recent times have seen renewed research interest in Datalog, see for instance the collection [36]. Datalog has in particular been used for formalizing and efficiently implementing program analyses [48, 54], whereas [49] presents Doop, a context-sensitive points-to analysis framework for Java.

Lodemann et al. [29] use semantic technologies to automate railway infrastructure verification. Their scope is still wider than this paper in the computational sense, with the full expressive power of OWL ontologies, running times on the order of hours, and the use of separate interactive graphical user interfaces rather than integration with design tools.

The use of logic programming and knowledge-base systems has been explored in depth for railway control systems, e.g. by Fringuelli et al. [14], who use logic programming to assist a station operator in performing local control actions on a railway station. The knowledge-base system that we presented has a similar encoding of static railway station layout, but with a different goal, namely to aid in designing the layout (static design) rather than executing commands (dynamic control).

Haxthausen and Østergaard [20] perform static checking of interlockings using a DSL for specifying network layout and interlocking specification, and a C++ program for performing the checks. Their scope for static checking of interlockings is similar to ours, but their focus is on using this as a preparation step for model checking an interlocking implementation, while our focus is on allowing diverse extensions to the rule base and creating user-friendly integrated tools.

In the future work with RailComplete AS, we will focus on extending the rule base to contain more relevant signalling and interlocking regulations, and also on evaluating the performance of our verification on a larger scale. Design information and rules about other railway control systems, such as geographical interlockings and train protection systems could also be included. The current work is assuming Norwegian regulations, but the European Rail Traffic Management System (ETCS/ERTMS) is expected to dominate in the future. The work on further developing our prototype verification tool in the context of the commercial RailCOMPLETE CAD software would also need to extend the rule base to cover more of signalling regulations and extending also to other disciplines. In this process, ETCS/ERTMS regulations would also be relevant.

Involving railway engineers in knowledge base development is somewhat hindered by the fact that Datalog and logic programming, though declarative and concise, are still programming languages, and a good intuition about language semantics is required for efficient and correct development. We have started developing a higher-level domain-specific language which compiles to Datalog, for the purpose of including railway engineers more closely in the knowledge base development. Using the techniques of controlled natural languages (CNL) [26], the language is formally defined and parsable, yet readable as natural language. Writing text in a controlled natural language is a harder problem, as the formal grammar limits what can be expressed, and also how it is written. This problem can be mitigated by means of specialized text editors (e.g., as provided by the Grammatical Framework [44],[45, Chap. 7] or Attempto Controlled English [15, 25]) which guide the user towards writing acceptable sentences. Adding specific language constructs for static infrastructure analysis of railway designs ensures that the level of abstraction is close to the original regulation text. Our future work will include testing this language with railway engineers and integrating knowledge base development into the railway design tool chain. This preliminary work can be reached through the technical report [30] which will be updated in the future.