Modeling and Verification of Scene of C3+ATO System Based on Timed Automata

doi:10.16182/j.issn1004731x.joss.19-0662

Abstract

Abstract: The C3+ATO system is in the experimental stage in our country and has the characteristics of high automation degree and high safety requirement at present. In order to confirm whether the specific function of the high-speed railway C3+ATO system meets the corresponding technical specification under the specific scene, a formal modeling and verification method based on the timed automata is proposed. The station automatic departure scene is selected as the modeling object. The functional requirements of C3+ATO system specification are extracted and the timed automata model of the scene is established. The message sequence chart of the corresponding process is generated, and the functional attributes of the system are verified and the model is simulated at the C3+ATO train control simulation platform. The simulation results show that the model meets the security function attributes and restricted activity attributes of the system technical specification, and can provide theoretical reference for the system design, practical application and improvement of related specifications.

Key words: C3+ATO system, timed automata, UPPAAL, station automatic departure, message sequence chart

CLC Number:

TP391.9

Zhang Zhenhai, Yao Jie. Modeling and Verification of Scene of C3+ATO System Based on Timed Automata[J]. Journal of System Simulation, 2021, 33(4): 951-961.

References

[1] 成雅靖. 自主化CTCS-3级列控系统复杂场景建模与验证[D]. 北京: 北京交通大学, 2018.
Cheng Yajing.Modeling and Verification of Complex Scenarios of Autonomous Chinese Train Control System Level 3[D]. Beijing: Beijing Jiaotong University, 2018.
[2] 康仁伟. 基于时间自动机的CTCS-3级列控系统建模方法与验证研究[D]. 北京: 北京交通大学, 2013.
Kang Renwei.The Research on Modeling Methods and Verification of Chinese Train Control System Level 3 Based on Timed Automata[D]. Beijing: Beijing Jiaotong University, 2013.
[3] 万勇兵, 徐中伟, 梅萌. CTCS-3级列控系统临时限速服务器建模与形式化验证[J]. 系统仿真学报, 2013, 25(1): 132-138.
Wan Yongbin, Xu Zhongwei, Mei Meng.Modeling and Formal Verification of Temporary Speed Restriction Server for CTCS Level 3[J]. Journal of System Simulation, 2013, 25(1): 132-138.
[4] 胡雪莲, 陶彩霞. 基于MSC与UPPAAL的列控系统等级转换场景形式化验证[J]. 铁道标准设计, 2015, 59(2): 122-127.
Hu Xuelian, Tao Caixia.Formal Verification of Level Transition Process in Train Control System Based on MSC and UPPAAL[J]. Railway Standard Design, 2015, 59(2): 122-127.
[5] 刘长青. 京张智能动车组——从“中国创造”向“中国智造”的里程碑式跨越[J]. 城市轨道交通研究, 2018, 21(2): 3.
Liu Changqing.Intelligent EMU for Beijing-Zhangjiakou Line—A Milestone form “Created in China” to “Intelligent Manufacturing in China”[J]. Urban Mass Transit, 2018, 21(2): 3.
[6] 程剑锋, 冯凯, 李科. 高速铁路CTCS3+ATO列控系统技术研究[J]. 中国铁路, 2019(1): 74-77.
Cheng Jianfeng, Feng Kai, Li Ke.CTCS3+ATO High Speed Railway Train Control Technology[J]. China Railway, 2019(1): 74-77.
[7] 朱少彤. CTCS3+ATO高速列车自动驾驶系统关键设备研究[J]. 中国铁路, 2018(10): 1-6.
Zhu Shaotong.Research on Key Equipment for CTCS3+ATO System of High Speed Railway[J]. China Railway, 2018(10): 1-6.
[8] 铁总科信. 高速铁路ATO系统暂行总体技术方案: [2018]8[S]. 北京: 中国铁路总公司, 2018.
Ministry of Science and Industry of the Railway Corporation. Temporary Overall Technical Scheme of ATO System for High Speed Railway: [2018]No.8[S]. Beijing: China Railway Corporation, 2018.
[9] Song S, Chen Y D.A Test Sequence Generation Method of Zone Controller Based on Timed Automata[J]. Journal of Measurement Science and Instrumentation (S1674-8042), 2019, 10(3): 266-276.
[10] Chen Y G, Yang L, Wang D.Modeling Research of Train Tracing Based on UML Sequence Diagram and UPPAAL[J]. Journal of Measurement Science and Instrumentation (S1674-8042), 2019, 10(2): 157-167.
[11] Kunz G, Machado J, Perondi E.Using Timed Automata for Modeling, Simulating and Verifying Networked Systems Controller's Specifications[J]. Neural Computing & Applications (S0941-0643), 2017, 28(5): 1031-1041.
[12] 杨璐, 陈永刚. 基于MSC与UPPAAL的区域控制器切换场景建模与验证[J]. 铁道标准设计, 2018, 62(5): 171-174.
Yang Lu, Chen Yonggang.Modeling and Verification of Switch Scene of Zone Controller Based on MSC and UPPAAL[J]. Railway Standard Design, 2018, 62(5): 171-174.

[1]	Dong Zhiming, Hu Zhongqi, Dai Haoran, Gao Jiancheng. An Automated Generation Method for Combat Simulation Scenarios Based on Large Language Models [J]. Journal of System Simulation, 2026, 38(5): 1129-1145.
[2]	Li Xiaonan, Chao Tao, Ma Ping, Yang Ming, Wang Yuxuan. Robust Identification of Black-box Nonlinear SSM Using Expectation-maximization [J]. Journal of System Simulation, 2026, 38(5): 1146-1158.
[3]	Liu Yingang, Ma Ming, Zhang Ronghua. Dynamic Task Planning for Wargaming Based on Large Language Models [J]. Journal of System Simulation, 2026, 38(5): 1187-1204.
[4]	Su Hongjia, Zhang Cheng, Liu Fei. SoS Effectiveness Evaluation Method Based on Fuzzy Functional Dependency Network Analysis [J]. Journal of System Simulation, 2026, 38(5): 1224-1238.
[5]	Mei Huawei, Yang Penghui, Yu Yang. Ultra-short-term Photovoltaic Power Prediction Based on Improved PatchTST Considering Data Drift [J]. Journal of System Simulation, 2026, 38(5): 1239-1254.
[6]	Li Quan, Su Peng, Wan Haiying, Zhang Chengxi, He Zhijian, Ni Yiyang, Zhao Zhonggai, Liu Fei. Modeling of Penicillin Fermentation Process Based on a Multi-stage LHS-EPRCC Method [J]. Journal of System Simulation, 2026, 38(5): 1255-1276.
[7]	Zhou Zicong, Zeng Junjie, Hu Yue, Zhu Zhengqiu, Yin Quanjun. Multi-agent Reinforcement Learning Method for Wargame Simulation Based on Suboptimal Demonstration Guidance [J]. Journal of System Simulation, 2026, 38(5): 1277-1289.
[8]	Shi Min, Guo Shisheng, Wang Suqin, Li Zhaoxin, Zhu Dengming. Annotation-free 6-DoF Grasp Detection Method Integrating Physical and Geometric Priors [J]. Journal of System Simulation, 2026, 38(5): 1290-1302.
[9]	Jiang Yanji, Xiao Xingyi, Dong Hao, Yu Miao, Huang Jinshan, Liu Daqian, Fei Bowen. Detection Method for 3D Lanes Based on Graph Relationship Optimization Integrating Point and Lane Features [J]. Journal of System Simulation, 2026, 38(5): 1303-1319.
[10]	Zhang Xin, Zhang Ping, Zhang Chen, Liu Wei, Han Boyang. Research on Calculation Model of Excavation Resistance Under Heterogeneous Soil Conditions [J]. Journal of System Simulation, 2026, 38(5): 1320-1332.
[11]	Wang Wei, Liu Dong, Cui Xinhao, Li Bo, Xiao Yiyong, Ren Yi. Multi-level Digital Model of Dynamic Earned Value Management for Complex Engineering Projects and Its Applications [J]. Journal of System Simulation, 2026, 38(5): 1350-1364.
[12]	Peng Lijun, Su Tingqi, Liu Peijin, He Lin, Zhou Xiewu, Zhang Minxin. Detection Method for Laboratory PPE Compliance Wearing Based on Human Key Points [J]. Journal of System Simulation, 2026, 38(5): 1365-1382.
[13]	Teng Jing, Tong Wencong, Zhang Zhongjie, Yao Xing, Li Junxian. Automatic Speed Guidance Method and Simulation Evaluation for Trams at Intersections [J]. Journal of System Simulation, 2026, 38(5): 1426-1439.
[14]	Jiang Shengchao, Pei Yunqing, Zhai Hongying, Wu Guojian, Gao Fang. Power Flow Calculation Based on Block-encoded Adiabatic Quantum Newton-Raphson Method [J]. Journal of System Simulation, 2026, 38(5): 1453-1465.
[15]	Qin Lang, Xie Jiacheng, Qiao Xiaojun, Wang Xuewen, Xiao Zhijie. Robot Trajectory Planning and Adjustment Method for Abnormal Pose of Actuator [J]. Journal of System Simulation, 2026, 38(5): 1466-1483.