SAFETY-LEVEL COMMUNICATION IN RAILWAY INTERLOCKINGS

This paper illustrates the formal analysis of a simple protocol to con vey critical data between the distributed solid state control elements in the signalling systems operated by Railtrack (British Railways). T he analysis concentrates on temporal properties of the protocol, and o ne safety property in particular which informal analysis suggests can be violated in certain combinations of circumstances. A formal model i s developed so that a rigorous, mathematically informed, assessment ca n be made as to whether the perceived violation of safety presents a s ignificant hazard to railway traffic. The model is used to formulate p ossible strategies to overcome the problem. While demonstrating the po wer of the modelling process, this paper also illustrates the importan ce of conducting formal proofs: the failed attempt to prove safety in a corrected version of the protocol reveals a second logical flaw. Bot h flaws admit simple solutions. (C) 1997 Elsevier Science B.V.