Verification by discrete simulation of interlocking systems

In the railway domain, an interlocking is the system controlling active components in a station in order to ensure a safe train traffic. The behaviour of modern interlockings is defined by particular data, called appli- cation data, describing the actions that the interlocking can take and under which conditions. However, appli- cation data are either prepared manually or prepared automatically by tools that do not guarantee a sufficient level of safety. Given the high level of safety required by such a system, the verification of the application data is a critical concern. Recent researches dealing with this issue are based on model checking. Due to the state space explosion problem, this approach does unfortu- nately not scale for large stations. In this paper, we present an innovative approach for the verification of interlocking data, based on a discrete event simulation, which does not suffer of the state space explosion prob- lem. Although sacrificing exhaustiveness, we show ex- perimentally on a real life instances that this approach is able to detect any introduced errors in the application data within seconds