Proceedings of the International Conference on Computer, Networks and Communication Engineering (ICCNCE 2013)

<Previous Article In Volume
Next Article In Volume>

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

Authors
Lei Yuan, Junfeng Wang, Renwei Kang
Corresponding Author
Lei Yuan
Available Online July 2013.
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)

<Previous Article In Volume
Next Article In Volume>
Volume Title
Proceedings of the International Conference on Computer, Networks and Communication Engineering (ICCNCE 2013)
Series
Advances in Intelligent Systems Research
Publication Date
July 2013
ISBN
10.2991/iccnce.2013.89
ISSN
1951-6851
DOI
10.2991/iccnce.2013.89How to use a DOI?
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/).

Cite this article

risenwbib
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  -