Safety-level communication in railway interlockings

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.