Recent work by King [51] records the current signalling rules applied by Railtrack. King's layered Z specification is intended to form part of requirements specification documents used for the procurement of signalling systems. The first layer defines the concept of network topology in terms of primitive track components (points, plain track and diamond crossings) and their allowable interconnections. Paths, and the concept of interference between paths, are defined on this static component. The second layer formalises the dynamic signalling rules in a conceptual foundation---since this is supposed to be independent of any particular technology, trains themselves are modelled (in terms of the paths they are on and in which they may come to a halt).
The third layer in King's specification is an instantiation of the conceptual foundation (e.g., SSI, which introduces signals, routes and sub-routes as control elements). However, since King does not address the question of whether the rules formalised in the conceptual foundation are `safe' (or at least consistent), it is inevitable, as the author himself points out, that verification of the safety properties of any formal refinement of the conceptual foundation will be needed. The Z specification cannot therefore be used to define safety requirements---although safety can of course be defined in terms of the conceptual foundation.
Wong [99] also attempts to codify the dynamic signalling rules in a formal theory. He proposes a scheme design methodology that links a theorem prover for higher-order logic with CAD tools for signalling scheme plans. The theorem prover automatically checks that the network described is legal with respect to some simple rules for assembling network components (e.g., that it forms a finite connected graph). Wong goes on to generate control tables for each route inferred from the scheme plan---these are specification documents used to guide the preparation of Geographic Data for an SSI installation. This is practically interesting because of the difficulty of certifying that the route setting conditions specified in the control table are sufficient (for safety).
However, Wong does not use his HOL theory directly to address the question of the adequacy of control table route specifications. Instead he derives the behaviour of the railway from the network structure, presenting the model as a finite state automaton. In higher-order logic a `time' varying function describes the state of the network at any instant, and the behaviour is governed by the dynamic signalling rules. Wong demonstrates how to prove that the automaton is safe with respect to the property that no two conflicting routes can be simultaneously set. Unhappily Wong's demonstration is somewhat vacuous since the notion of conflict in defining the formal property is identical to that used to encode Nock's requirements. Cullyer and Wong [26] have used a similar model to examine safety related properties of a level crossing.
Some related work on behalf of the Danish State Railways has been carried out by Mark Hansen [56] under the aegis of the ProCos project. Her VDM specification is also based on a description of the network topology, and the purpose of the model is to clarify formal requirements (functional, as well as safety) for interlockings to be developed on a per station basis. This work emphasises model validation (through simulation), and requirements capture. The principal requirement is that trains do not collide. Modulo the usual caveats about coupling trains, this is expressed in a predicate that asserts that no track section contains more than one train. An attribute of track sections in the model is, therefore, that they may be associated with a set of trains. The hidden assumption here is that track-side equipment is capable of determining that a second or subsequent train has entered an already occupied track section. Track circuits are unable to decide this, for example, although more sophisticated train detection systems can relay train identities to the control system (trains and tracks communicate).
The authors cited above record the (static and) dynamic signalling rules in a mathematical theory. The natural focus in these enterprises is on requirements capture, with safety requirements dominating. But this begs the question of how to demonstrate that a purported implementation conforms to the requirements---in particular, to verify that the interlocking is safe. Another body of work addresses the verification problem directly.
Atkinson and Cunningham [4] describe a signalling case-study that exercised a tableaux proof system for Modal Action Logic (a variant of PDL). This took a simple interlocking (the Forest scheme [8] illustrated on page 215) described by a system of MAL axioms derived from the Geographic Data and the network topology, and further action rules to describe permitted train movements. The idea is to prove that a modal property p is a consequence of such a specification Spec: the MAL prover attempts to refute the goal Spec => -p. The logic has a refutation complete decision procedure to prove such goals---meaning that if a counter model exists it will always be found. The procedure is semi-decidable however, so cannot always prove Spec => p when it is true. This case-study can fairly be said to demonstrate the capabilities of the FOREST tools, but the model is too concrete to be a specification, and too impoverished (in its notion of time and computation step in calculating signal aspects, for example) to be useful as a vehicle for proving safety of the interlocking.
In a similar, but much more successful vein, Stålmarck and Säflund model interlockings for the Swedish railway authorities (Banverket, and SJ, the railway company) using propositional logic [88]. They have developed dedicated tools for analysing safety related properties of Sternol programs which are used in interlocking design. A Sternol program is a system of equations, with one equation---really, a guarded command---for each value a variable in the program can take. One group of equations may refer, for example, to the aspect of a particular signal. The Circuit Verification Tool [88] is used to verify that exactly one of the guards in the equations for a program variable is true at any time. This guarantees determinism (in each execution cycle), and such a Sternol program can therefore be implemented by executing the equations in any order (cyclically). For SJ and their subcontractors this is an important safety property of their interlockings.
By representing a Sternol program in propositional logic it is possible to go on to examine other safety properties by proving Prog => p. Given the size of such formulas, this would be a severe challenge but for Stålmarck's (patented) natural deduction style proof technique for Boolean satisfiability. The time complexity of the algorithm is polynomially related to the number of subterms in the formula, with the exponent (hardness) being determined by the number of simultaneous free assumptions needed in the natural deduction proof tree. The empirical evidence is that for many practical problems the degree of hardness is low by this measure, so the proof technique is effective for extremely large formulae (exceeding 10^5 connectives). To obtain counter models an ordering on the subterms in the formula is needed; this does not affect the hardness of the proof, but makes space requirements (i.e., the length of the proof) sensitive to the order chosen.
The Vital Processor Interlocking (VPI) analysed by Groote et al. [37] for the Dutch Railway Company has an execution model that is similar to the Sternol programs described above: a sequence of equations that are solved once a cycle, each of which defines the value of an internal control variable or system output. Groote and his colleagues formulate safety requirements in a modal logic so as to express properties relating to finite sequences of program steps (or states): next formulae refer to a finite future, just formulae refer to finite immediate past, and static formulae refer only to the current state. To prove that the program satisfies a modal property both are translated into propositional logic, and Prog => p is checked using Stålmarck's method. In general, if the property refers to n time steps then this many time-indexed copies of the program are needed for the proof. Clearly n and the size of Prog, in terms of the number of subformulae, determine the range of application of this approach to VPI program verification. Taken literally, n may be `large' (21 s in the example), but a time abstraction alleviates the complexity problem so that the results are encouraging.
Returning, finally, to the problem of verifying safety properties of Geographic Data, we should note British Rail's own research which tackles the problem from an automata-theoretic perspective. Ingleby and Mitchell [48] represent SSI behaviour in a Mealy machine having next state and output functions nxt and out. Safety properties are characterised as state predicates (static properties in Groote's terminology [37]) and output predicates (also static). The problem is to demonstrate that the automaton modelling the interlocking is safety transitive: if safe(s) asserts that state s is safe, the interlocking is safety transitive if for all states s and inputs i, safe(s) => safe(nxt(s,i)). This proof concept ([74], illustrated more coherently in Chapter 4) is an instance of a powerful proof technique for safety properties called co-induction.
Ingleby's data decompositions [47] (discussed further in Chapter 5) are what makes this approach to automatic verification of safety properties of Geographic Data practical at all: these lead to state clustering in the automaton, and a local proof strategy, but complicate the task of generating counter models and tracing the location in the data where the safety properties are being violated. Related work has been reported by Conroy and Pulley [21] whose models are Büchi automata. These authors are plagued by the enormous combinatorial complexity of the reachable state space in signal interlockings. For the Hoorn-Kersenboogerd interlocking [37], Groote puts the reachable state space somewhere between 10^30 and 10^500 states: the lower bound arises because the VPI records circa 100 Boolean inputs---SSI receives up to 512 such inputs in each major cycle (ignoring the occasional panel request) and the internal state is a vector of (at most) 1,216 bytes.