[Go Up], [Go Back].

1.5.2. Contributions and Thesis Overview

When approaching the question of automated verification, the cited work illustrates that great care should be exercised to avoid intractable state spaces on the one hand, and combinatorial explosion in checking Boolean formulae on the other. Both can be avoided by selecting an appropriate abstraction with which to work, and as long as safety can be satisfactorily formalised through invariants of the internal state of the SSI (which may still refer to system inputs and outputs of course). We concentrate on the semantics of the Geographic Data Language which, in programming terms, is a somewhat richer language than Sternol or the Vital Logic Code in VPI. The focus on semantics leads to a compositional verification strategy---but the route to this understanding of the problem is as important to record here as the final synopsis itself.

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.


[Go Up], [Go Back].
Matthew Morley, Edinburgh. Date: 29 November, 1998