At the Dutch station Hoorn-Kersenboogerd, computer equipment is used for the safe and in time movement of trains. The computer equipment can be divided in two layers. A top layer offering an interface and means to help a human operator in scheduling train movement. And a bottom layer which checks whether commands issued by the top layer can safely be executed by the rail hardware and which acts appropriately on detection of a hazardous situation. The bottom layer is implemented with a programmable piece of equipment namely a Vital Processor Interlocking (VPI). This paper introduces the most important features of the VPI at Hoorn-Kersenboogerd. This particular VPI is modelled in µCRL. Furthermore, the paper touches upon correctness criteria and tool support for VPI's, and suggests ways for verification of properties of VPI's. Experiments show that it is indeed possible to efficiently verify these correctness criteria. (A)
Samenvatting