系统仿真学报 ›› 2021, Vol. 33 ›› Issue (4): 951-961.doi: 10.16182/j.issn1004731x.joss.19-0662
张振海, 姚婕
收稿日期:
2019-12-19
修回日期:
2020-05-29
出版日期:
2021-04-18
发布日期:
2021-04-14
作者简介:
张振海(1983-),男,博士,副教授,研究方向为交通信息工程及控制。E-mail:764411629@qq.com
基金资助:
Zhang Zhenhai, Yao Jie
Received:
2019-12-19
Revised:
2020-05-29
Online:
2021-04-18
Published:
2021-04-14
摘要: C3+ATO系统目前在我国处于试验发展阶段且具有自动化等级高、安全标准高等特点。为验证具体场景下高速铁路C3+ATO系统功能是否符合对应技术规范,提出一种基于时间自动机的形式化建模与验证方法。选取车站自动发车场景作为建模对象,提取C3+ATO系统规范中的功能需求,建立场景的时间自动机模型,生成对应流程的消息顺序图并对系统功能属性进行验证,在C3+ATO列控仿真平台仿真验证。仿真验证结果证明:模型满足系统的安全功能属性和受限活性需求,为后续系统设计开发、实际应用及相关规范完善提供理论参考。
中图分类号:
张振海, 姚婕. 基于时间自动机的C3+ATO系统场景建模与验证[J]. 系统仿真学报, 2021, 33(4): 951-961.
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.
[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] | 李智杰, 石昊琦, 李昌华, 张颉. 基于改进遗传算法的影像中心布局优化方法[J]. 系统仿真学报, 2022, 34(6): 1173-1184. |
[2] | 陈斌, 刘悦, 杨亚磊. 基于STN的机场航班过站保障时间协同规划建模[J]. 系统仿真学报, 2022, 34(6): 1196-1207. |
[3] | 杨凯, 陈纯毅, 胡小娟, 于海洋. 蒙卡渲染画面多特征非局部均值滤波降噪算法[J]. 系统仿真学报, 2022, 34(6): 1259-1266. |
[4] | 陈麒, 崔昊杨. 基于改进鸽群层级的无人机集群视觉巡检模型[J]. 系统仿真学报, 2022, 34(6): 1275-1285. |
[5] | 王沐晴, 张磊, 范秀敏, 骆晓萌, 朱文敏. VR外设驱动的虚拟人姿态优化仿真方法[J]. 系统仿真学报, 2022, 34(6): 1296-1303. |
[6] | 陆承, 靳学胜. 基于Steam VR的交互仿真水枪灭火训练系统设计[J]. 系统仿真学报, 2022, 34(6): 1312-1319. |
[7] | 高宏鼐, 付丽疆, 夏倩, 郭亚. 可观测度在光合作用模型性能评估中的应用[J]. 系统仿真学报, 2022, 34(6): 1330-1342. |
[8] | 倪凌佳, 黄晓霞, 李红旮, 张子博. 基于协作式深度强化学习的火灾应急疏散仿真研究[J]. 系统仿真学报, 2022, 34(6): 1353-1366. |
[9] | 蒙盾, 胡卓, 张华军. 基于改进A*算法的多层邮轮疏散系统仿真[J]. 系统仿真学报, 2022, 34(6): 1375-1382. |
[10] | 郭宇飞, 赵康, 海永清. 面向有限元分析的三角网格布尔运算方法[J]. 系统仿真学报, 2022, 34(5): 1003-1014. |
[11] | 吴桐, 王清辉, 徐志佳. 三周期极小曲面多孔材料渗透率尺度特性研究[J]. 系统仿真学报, 2022, 34(5): 1015-1024. |
[12] | 蒋阳升, 王思琛, 高宽, 刘梦, 姚志洪. 混入智能网联车队的混合交通流元胞自动机模型[J]. 系统仿真学报, 2022, 34(5): 1025-1032. |
[13] | 梁江涛, 王慧琴. 基于改进蚁群算法的建筑火灾疏散路径规划研究[J]. 系统仿真学报, 2022, 34(5): 1044-1053. |
[14] | 张其文, 张斌. 基于教学优化算法求解置换流水车间调度问题[J]. 系统仿真学报, 2022, 34(5): 1054-1063. |
[15] | 邢根上, 鲁芳, 李书山, 罗定提. 基于产品体验性的供应链交货模型与仿真研究[J]. 系统仿真学报, 2022, 34(5): 1064-1075. |
阅读次数 | ||||||
全文 |
|
|||||
摘要 |
|
|||||