Abstracts of Signalling related Publications
(Participants proceedings of the first FMERail Workshop, June 1998.
Abstract: When one wishes to use formal verification techniques
to reason about the behaviour of computer controlled railway signalling
systems, particularly if the objective is to check their safety properties, a
rigorous mathematical semantics for the language used to program the signalling
functions is essential to any meaningful verification strategy. This paper
motivates the need for formal semantics in such applications, and illustrates
how an operational semantics for the language used to program Railtrack's Solid
State Interlocking (SSI) may be defined.
In Science of Computer Programming, Vol. 29, Nos. 1-2, July
1997, pp 149-172.
Abstract: This paper illustrates the formal analysis of a simple
protocol to convey critical data between the distributed solid state control
elements in the signalling systems operated by Railtrack (British Railways).
The analysis concentrates on temporal properties of the protocol, and one
safety property in particular which informal analysis suggests can be
violated in certain combinations of circumstances. A formal model is developed
so that a rigorous, mathematically informed, assessment can be made as to
whether the perceived violation of safety presents a significant hazard to
railway traffic. The model is used to formulate possible strategies to overcome
the problem. While demonstrating the power of the modelling process, this paper
also illustrates the importance of conducting formal proofs: the failed attempt
to prove safety in a corrected version of the protocol reveals a second logical
flaw. Both flaws admit simple solutions.
Safety Assurance in Interlocking Design. PhD thesis,
University of Edinburgh, 1996.
Abstract: This thesis takes a pedagogical stance in
demonstrating how results from theoretical computer science may be applied to
yield significant insight into the behaviour of the devices computer systems
engineering practice seeks to put in place, and that this is immediately
attainable with the present state of the art. The focus for this detailed study
is provided by the type of solid state signalling systems currently being
deployed throughout mainline British railways. Safety and system reliability
concerns dominate in this domain. With such motivation, two issues are tackled:
the special problem of software quality assurance in these data-driven control
systems, and the broader problem of design dependability. In the former case,
the analysis is directed towards proving safety properties of the geographic
data which encode the control logic for the railway interlocking; the latter
examines the fidelity of the communication protocols upon which the distributed
control system depends.
The starting point for both avenues of attack is a mathematical model
of the interlocking logic that is derived by interpreting the geographic data
in process algebra. Thus, the emphasis is on the semantics of the programming
language in question, and the kinds of safety properties which can be expressed
as invariants of the system's ongoing behaviour. Although the model so derived
turns out to be too concrete to be effectual in program verification in
general, a careful analysis of the safety proof reveals a simple co-induction
argument that leads to a highly efficient proof methodology. From this
understanding it is straightforward to mechanise the safety arguments, and a
prototype verification system is realised in higher-order logic which uses the
proof tactics of the theorem prover to achieve full automation.
The other line of inquiry considers whether the integrity of the
overall design that coordinates the activities of many concurrent control
elements can be compromised. Therefore, the formal model is developed to
specifically answer safety-related concerns about the protocol employed to
achieve distributed control in the management of larger railway networks. The
exercise reveals that moderately serious design flaws do exist, but the real
value of the mathematical model is twofold: it makes explicit one's assumptions
about the conditions under which the faults can and cannot be activated, and it
provides a framework in which to prove a simple modification to the design
recovers complete security at negligible cost to performance.
In proceedings of the 6th annual Workshop on Higher Order Logic
Theorem Proving and its Applications, Vancouver, 4--6 August, 1993, LNCS Vol.
Abstract: Higher Order Logic is used to analyse safety
properties of a computer based railway signal control system. British Rail's
Solid State Interlocking is a data driven controller whose behaviour is
governed by rules stored in a geographic database. The correctness of these
data are highly critical to the system's safe operation. Taking as our starting
point Gordon's implementation of program logics in Higher Order Logic, we
formalise the data correctness problem in a natural way, designing tactics to
automate much of the verification task. Our approach requires quadratic time
and linear space, and is thought to be adequate for the current generation of
Solid State Interlockings. Properly formalised, the compositional proof
strategy we suggest will allow us to scale up our analyses arbitrarily.
Matthew Morley, Edinburgh. Date: 29 November, 1998