Towards Risk Prediction: Runtime Verification of Train Control Systems for Overspeed Protection

In railways, overspeed protection is the central function of Automatic Train Protection (ATP). Any failure of this function can cause serious people injury or property loss. In practical applications, incorrect protection curves can be caused by misconfigurations of line data or mistakes in coding. These defects are hard to be fully eliminated during the development phases. In this paper, we propose an online monitoring approach to provide on-going protections for ATP. In our method, dynamic models are introduced to describe behaviour of the system as monitoring specifications. This avoids the so-called state explosion problem that is caused by complicated line data. Furthermore, we present a concrete example taking from Beijing Yizhuang metro line. The verification results show that this online monitoring method is feasible to predict potential risks of train operations.

I. Introduction

In railways, overspeed protection is the central function of Automatic Train Protection (ATP) system. It is responsible for detecting dangerous train operations by calculating safe speed of a train according to Movement Authority (MA). The function then compares the current speed of the train with the calculating results. Whenever an overspeed is detected, the ATP triggers a brake immediately to avoid a collision. In fact, safety assurance of ATP is one of the main challenges in the railway signalling.