The safety guaranteeing system at station Hoorn-Kersenboogerd

Abstract

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 VPIs, and suggests ways for verification of properties of VPIs. Experiments show that it is indeed possible to effciently verify these correctness criteria.