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

被引:0
作者
Lei Yuan [1 ]
Junfeng Wang [1 ]
Renwei Kang [1 ]
机构
[1] Beijing Jiaotong Univ, State Key Lab Rail Traff Control & Safety, Beijing, Peoples R China
来源
PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTER, NETWORKS AND COMMUNICATION ENGINEERING (ICCNCE 2013) | 2013年 / 30卷
关键词
Train Control System; TSRS; Timed Automata; UPPAAL;
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:355 / 358
页数:4
相关论文
共 50 条
[1]   Modeling and verification of temporary speed restriction of CTC-S3 train control system [J].
State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, Beijing 100044, China ;
不详 .
Xinan Jiaotong Daxue Xuebao, 2013, 4 (708-714) :708-714
[2]   Analysis of abnormal braking of CTCS-3 train control system based on timed automata [J].
Chen, Jiao ;
Tang, Tao ;
Lim, Yu .
2017 CHINESE AUTOMATION CONGRESS (CAC), 2017, :5531-5536
[3]   Dynamic Timed Automata for Reconfigurable System Modeling and Verification [J].
Tigane, Samir ;
Guerrouf, Faycal ;
Hamani, Nadia ;
Kahloul, Laid ;
Khalgui, Mohamed ;
Ali, Masood Ashraf .
AXIOMS, 2023, 12 (03)
[4]   Verification of timed automata based on similarity [J].
Dembinski, P ;
Penczek, W ;
Pólrola, A .
FUNDAMENTA INFORMATICAE, 2002, 51 (1-2) :59-89
[5]   Fault diagnosis based on timed automata: Diagnoser verification [J].
Knotek, Michal ;
Simeu-Abazi, Zineb ;
Zezulka, Frantisek .
2006 IMACS: MULTICONFERENCE ON COMPUTATIONAL ENGINEERING IN SYSTEMS APPLICATIONS, VOLS 1 AND 2, 2006, :889-+
[6]   Timed automata approach to real time distributed system verification [J].
Krákora, J ;
Waszniowski, L ;
Písa, P ;
Hanzálek, Z .
WFCS 2004: IEEE INTERNATIONAL WORKSHOP ON FACTORY COMMUNICATION SYSTEMS, PROCEEDINGS, 2004, :407-410
[7]   Formal verification of multitasking applications based on timed automata model [J].
Libor Waszniowski ;
Zdeněk Hanzálek .
Real-Time Systems, 2008, 38 :39-65
[8]   Formal verification of multitasking applications based on timed automata model [J].
Waszniowski, Libor ;
Hanzalek, Zdenek .
REAL-TIME SYSTEMS, 2008, 38 (01) :39-65
[9]   Control System Design for Height Measurement of BGA Balls Based on Timed Automata [J].
Wang, Hengsheng ;
Lu, Zimin ;
Wang, Fuliang .
IEEE TRANSACTIONS ON COMPONENTS PACKAGING AND MANUFACTURING TECHNOLOGY, 2014, 4 (03) :528-537
[10]   Timed Automata Supervisory Control of a Glass Bonding System [J].
Chianello Correia, Eduardo Ottavio ;
Carrilho da Cunha, Antonio Eduardo .
IFAC PAPERSONLINE, 2017, 50 (01) :12345-12350