Modelling British Rail's Interlocking Logic: Geographic Data Correctness

Matthew J. Morley

Abstract: This paper examines the integrity of a portion of British Railways' signal control logic as expressed in their Geographic Data Language. The issue addressed here is the correctness of the Geographic Data describing a simple signalling system, where this is motivated by the need for a proof tool to assist signalling engineers in verifying their designs. A translation of the Geographic Data Language into CCS is given which forms the first step of a rigorous demonstration that the model developed has certain desirable safety properties.

LFCS report ECS-LFCS-91-186, November 1991.

Previous | Index | Next