The Safety Guaranteeing System at Station Hoorn-Kersenboogerd (Extended Abstract )
Jan Friso Groote, S.F.M. van Vlijmen, J.W.C. Koorn · 1995
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 Interlocking1 (VPI). This pcper introduces the most important features of VPIs and models them using the process algebraic language pCRL. The form of correctness criteria of VPIs as described and these criteria are classified in the categories STATIC, JUST and NEXT. A rather complete list of correctness requirements is given in W.J. Fokkink, Safety Criteria for Hoorn-Kersenboogerd Railway Station (to appear as Technical Report, Logic Group Preprint Series, Utrecht University, The Netherlands, 1995).