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.
Previous | Index | Next An error occured whilst processing this directive