A dedicated algorithm for verification of interlocking systems

Abstract

A railway interlocking is the system ensuring a safe train traffic inside a station by monitoring and controlling signalling components. Modern interlockings are controlled by a generic software that uses data, called application data, reflecting the layout of the station under control and defining which actions the interlocking can perform. The safety of the train traffic relies thereby on application data correctness, errors inside them can lead to unexpected events, such as collisions or derailments. Automatising and improving the verification process of application data is an active field of research. Most of this research is based on model checking, which performs an exhaustive verification of the system but which suffers from scalability issues. In this paper, we propose to use our knowledge of the system in order to design a polynomial verification algorithm that can detect all the possible safety issues provided that an assumption of monotonicity hold.