WIT Press


Safety Criteria For The Vital Processor Interlocking At Hoorn-Kersenboogerd

Price

Free (open access)

Volume

20

Pages

10

Published

1996

Size

975 kb

Paper DOI

10.2495/CR960111

Copyright

WIT Press

Author(s)

W. Fokkink

Abstract

We formulate several classes of safety criteria for railway yards in terms of observable behaviour. These criteria are meant to protect trains from collisions and from derailments. We identify a number of safety criteria, and present instances of these classes for the case of the railway yard at station Hoorn-Kersenboogerd. These criteria have all been checked by means of the Stalmarck theorem prover, using a methodology from Groote, Koorn and Van Vlijmen. 1 Introduction At a sizable number of Dutch railway stations, among which station Hoorn- Kersenboogerd, computer equipment based on a Vital Processor Interlock- ing (VPI) is used in order to ensure safe movement of trains. Apart from a number of hardware checks, a VPI essentially executes a program that con- sists of a large number of assignments of the form v =

Keywords