1.5. Formal Approaches to Signalling Safety

In seeking to adopt rigorous techniques British Rail (now Railtrack), along with several other railway authorities, advance the opinion that the more formal analysis will improve the quality and safety of their products and services. While the reasons for introducing computer controlled railway signalling may be largely economic, it seems that with the advent of design notations such as the Geographic Data Language the overall safety case can be strengthened because of the possibility to produce formal proofs of the behaviour of the interlocking. Even without formal proofs the possibility to test (simulate) the design long before tracks are laid down, and with full confidence that the same software will control the live network, is a considerable boost to safety and productivity. In principle at least, the introduction of more rigorous techniques will improve productivity in the long run because a formal proof that the Geographic Data are safe may remove much of the need for testing the design.

These arguments indicate that what is required is a framework within which to conduct various forms of analysis on Geographic Data. Simulation and testing remain central concerns in signalling engineering---if only because of the need to test the final data/control configuration for each instantiation of the data. In the context of this thesis the `formal correctness' of the Solid State Interlocking is not in itself the issue. Rather, the central problem is that of automatically checking SSI data through an appropriate language of logical assertions and proof. There appear to be two distinct approaches to providing the analytic framework required: either we attempt to formalise the principles of railway signalling, or we reduce a given design to a formal specification (or model) whose properties we verify. A brief survey of related work will help to illustrate these choices.

1.5.1. Related Work
1.5.2. Contributions and Thesis Overview

Matthew Morley, Edinburgh. Date: 29 November, 1998