**Chapter 2**
The next chapter fills out the background, concentrating on the syntax
and semantics of the Geographic Data Language, and explains the
overall organisation of the data in the SSI. The Geographic Data
Preparation Guide
[9]
defines the language informally, in a manner that is intelligible to
signalling engineers, but to prove properties of programs written in
the language a more rigorous understanding is needed. In this chapter
therefore, a formal semantics is proposed that is faithful to the
informal description. This defines the execution model that is
elsewhere assumed to be valid.

**Chapter 3**
The starting point was not a formal description of the Geographic Data
Language, but a model of a much simplified signalling scheme. The
model is derived by a systematic translation of the data into CCS. The
execution model abstracts from such details as minor and major cycles,
concentrating only on the transitions allowed by the rules held in the
database. The focus then is on the *properties* of the
Geographic Data, and their formulation in terms of a predicate
**F** of the states of the abstract machine *M*.
For the simple example we can verify these properties by model
checking: we prove **F** is invariant, that is
*M* sat. *max(Z*.**F** & [-]*Z)*
in the terminology of the modal mu-calculus, using the Concurrency
Workbench and tools developed for the task. However, this verification
method does not scale beyond the small examples tried---the problem is
one of abstraction in the *proof*.

**Chapter 4**
This chapter examines the invariance proof in detail. Instead of
trying to establish that (all reachable) states of the model are safe
we prove that the transitions *preserve safety*. This gives a
much more direct demonstration that the Geographic Data are safe
because the data really define the state transitions of the SSI (with
respect to the semantics). The (co-)inductive nature of the proof is
explained here in terms of the proof tableau constructed by the model
checker used in
Chapter 3:
the idea is to show that if a state *S* is safe (i.e.,
*S* sat. **F**) then every state *S'* that is
immediately reachable from *S* is safe: *S'* sat.
**F**. We do not worry about whether *S* is
reachable. Since the proof method is to be mechanised, time is taken
here to identify the steps needed to demonstrate that these
*verification conditions* are true.

**Chapter 5**
The arguments formulated in
Chapter 4
are interpreted here in the framework of Floyd-Hoare logic. In this
chapter the syntax and semantics of the Geographic Data Language are
formalised as a theory of higher-order logic, and embedded in the HOL
proof system. From this theory the program logic is derived, and the
proof obligation formulated in the goal
{**F**}*c*{**F**},
for each command *c* in the data. Through the tactics of the
HOL system, and a modest amount of ML programming, we recover a fully
automatic proof method which is linear in both in the length of
**F** and the number of commands *c* (and
independent of the number of states of the SSI). We show that the
range of application of this prototype Geographic Data verifier can be
considerably extended through techniques for decomposing the
invariance proofs. Decomposition according to the structure of
*c* comes for free with Floyd-Hoare logic, so we concentrate on
decomposing **F**.

**Chapter 6**
Here the model presented in
Chapter 3
is developed in a different way to analyse properties of the inter-SSI
communications---specifically, those by which two Interlockings
cooperate in locking routes over their common boundary. The logic to
achieve this route locking (and release) is also encoded in Geographic
Data. It is found that unfavourable message delays can lead to
circumstances in which hazards that compromise the safety of railway
traffic can arise *in principle*. Since such hazards are not
precluded *in practice*, a strict interpretation of the term
`safety' leads to the conclusion that this is a design flaw in the
remote route request protocol. In fact the risk implied by this fault
in the generic program is difficult to quantify precisely---which is
sufficient reason to study the problem formally. Our analysis leads to
several recommendations to eliminate the flaw, and we prove that it is
possible to implement the protocol so that it cannot then, of itself,
lead to unsafe states in the railway.

Finally, **Chapter 7** concludes this work with a
summary, and indicates the likely impact of our findings on the
industrial usage of formal methods and the practice of interlocking
design. The application of the theorem prover developed in
Chapter 5
to `live' data from the Leamington Spa signalling scheme is described
in this final chapter. Also considered are the concrete
recommendations coming from the analysis in
Chapter 6:
these indicate that only very minor changes to the SSI generic
program would be needed to address the concerns raised there.

Matthew Morley, Edinburgh. Date: 29 November, 1998