The safe functioning of a train control system is critically dependent on the validity of the movement authorities issued to a train by the track-side radio control blocks (RBC). In order to guarantee that the movement authorities are safe, the RBC needs to consult the interlocking logic. The RBC and the interlocking logic has to be configured with data specific to the yard of operation. This paper aims to validate the data using formal methods. Specifically we present an approach for proving that the trains maintain safe distance between them when they follow the movement authorities issued by the RBC in a yard. We use UPPAAL [13] for modelling the train control system system for a small yard including the continuous dynamics of trains. The UPPAAL model-checker is used to verify the safety of all train movements permitted by the model. We demonstrate that errors in the logic can be detected by the proposed method in feasible time. As opposed to previous approaches using theorem proving techniques, our method lends itself easily to automation, which is thereby more acceptable to railway engineers.
展开▼
