Formal methods for railway signalling

At the moment, railway signalling systems are designed in a manner which is based on concepts of interlocking and signalling which have grown up over the last 150 years. Considerable use is made of `relay diagrams´ and tables to define interlocking and routing. The excellent safety record of railways worldwide is due to a large extent to the rigour of the regulations which have been evolved by generations of signalling and telecommunications engineers. With the increasing use of microelectronics and computing in railway signalling, it is reasonable to ask if the rules promulgated by the UK Institute of Railway Signalling Engineers can be formulated in a mathematical way, which will suit the development of computer-controlled interlocking and routing. In particular, this paper considers the application of the specification language HOL and computer languages such as Pascal