The safety guaranteeing system at station Hoorn-Kersenboogerd

At the Dutch station Hoorn-Kersenboogerd computerized control is used for the safe and in time movement of trains. It can be divided in three layers. A top layer assisting an operator in scheduling train movement. A bottom layer with hardware that can monitor and change the state of the railway. And an intermediate layer mainly checking whether commands issued by the top layer can safely be executed by the bottom layer. The intermediate layer is responsible for the safety of the railway. It is implemented with a programmable piece of equipment namely a Vital Processor Interlocking (VPI). This paper introduces the most important features of VPIs and models them using the process algebraic language μCRL. The form of correctness criteria of VPIs is described and these criteria are classified in the categories STATIC, JUST and NEXT. We verify the correctness criteria by transforming both the program and the criteria to propositional logic. We describe our experiences with tool support, both for the transformation and for proving formulas. Experiments show that it is also rather straightforward to verify correctness criteria on larger railway yards