The Verification of Temporary Speed Restriction of Train Control System Based on Timed Automata

DOI

10.2991/iccnce.2013.89How to use a DOI?

Keywords

Train Control System, TSRS, Timed Automata, UPPAAL.

Abstract

Temporary speed restriction (TSR) refers to the speed restriction within given time bounds beyond the required speed restriction by the lines. TSR system is a typical real-time system. There are strict logical order relations and precise time constraints for the settings, execution, confirmation and cancel of TSR command. So it is important to ensure real-time performance of TSR system. In this paper we focused on the verification of the existing specification of the TSR system of Chinese Train Control System (CTCS) which was used in high-speed railway. We expected to find some imperfections of the working process or the configuration parameters of TSR system. Therefore, a model of the timed automata for the working process of the TSR system was established on the basis of the specification which was published by the administrator of the railway. UPPAAL verification tool was applied to verify the safety and bounded liveness properties of TSR system. The result of the verification showed that some time-related configuration parameters cannot achieve real-time requirements in the existing technical specifications. We also recommended how to correct this imperfection. It showed that the modeling and verification methods we proposed can be useful to study real-time performance of train control system of high-speed railway.

Copyright

© 2013, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Lei Yuan
AU  - Junfeng Wang
AU  - Renwei Kang
PY  - 2013/07
DA  - 2013/07
TI  - The Verification of Temporary Speed Restriction of Train Control System Based on Timed Automata
BT  - Proceedings of the International Conference on Computer, Networks and Communication Engineering (ICCNCE 2013)
PB  - Atlantis Press
SP  - 355
EP  - 358
SN  - 1951-6851
UR  - https://doi.org/10.2991/iccnce.2013.89
DO  - 10.2991/iccnce.2013.89
ID  - Yuan2013/07
ER  -