基于形式化方法的城轨FAO系统在线危险预测技术

doi:10.3969/j.issn.1673-4440.2021.06.015

铁路通信信号工程技术 ›› 2021, Vol. 18 ›› Issue (6): 76-81.DOI: 10.3969/j.issn.1673-4440.2021.06.015

基于形式化方法的城轨FAO系统在线危险预测技术

杨艳艳¹，王祺²，柴铭^2，3

1．北京城市轨道交通咨询有限公司，北京 100068；
2．北京交通大学电子信息工程学院，北京 100044；
3．轨道交通运行控制系统国家工程研究中心，北京 100044

收稿日期:2020-11-05 修回日期:2021-05-10 出版日期:2021-06-25 发布日期:2021-08-13
基金资助:
北京市自然科学基金项目（L181005）

Online Hazard Prediction of FAO Based on Formal Verification

Yang Yanyan¹, Wang Qi², Chai Ming^{2, 3}

1. Beijing Metro Consultancy Co., Ltd., Beijing 100068, China；
2. School of Electronics and Information Engineering, Beijing Jiaotong University, Beijing 100044, China；
3. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing 100044, China

Received:2020-11-05 Revised:2021-05-10 Online:2021-06-25 Published:2021-08-13

摘要/Abstract

摘要： 提出基于形式化验证的FAO系统在线危险预测技术。利用形式化方法可信检验FAO系统的运行时行为，预测可能出现的列车运行危险，以实现FAO系统的实验室安全性验证。基于混成自动机建立列车运行控制模型，结合线路数据以及车载运行状态，计算列车运行可达集，实现对危险的预测。以北京燕房线FAO为例，设计运行时验证系统，通过仿真试验验证在线危险预测技术具有可行性。

关键词: 全自动运行, 形式化验证, 混成自动机, 危险预测

Abstract: A formal verification-based hazard prediction technology for FAO system is proposed. With formal methods, the runtime operational behavior is fully verified and possible hazards are predicted. This technique provides a laboratory verification method to prove the operational safety of FAO systems. Train control models are established with hybrid automata combined with line engineering data. Based on on-board equipment operational status and train control data, the reachable set of train operations is computed and hazards are predicated. A runtime verification system is designed and the feasibility of the online hazard prediction technology is verified with a simulation system of Beijing Subway Yanfang Line.

Key words: FAO, formalized verification, hybrid automata, hazard prediction

中图分类号:

U284.48

杨艳艳, 王祺, 柴铭. 基于形式化方法的城轨FAO系统在线危险预测技术[J]. 铁路通信信号工程技术, 2021, 18(6): 76-81.

Yang Yanyan, Wang Qi, Chai Ming. Online Hazard Prediction of FAO Based on Formal Verification[J]. Railway Signalling & Communication Engineering, 2021, 18(6): 76-81.

图/表 6

参考文献

[1]张艳兵，戴克平.自主化全自动运行系统研究与应用[J].都市快轨交通，2017，30(6):1-6.
Zhang Yanbing, Dai Keping. Research and Application of Independently Developed Fully Automatic Operation System[J]. Urban Rapid Rail Transit, 2017, 30(6):1-6.
[2]宗明，郜春海，何燕.基于CBTC控制的全自动驾驶系统[J].都市快轨交通，2006，19(3):34-36.
Zong Ming, Gao Chunhai, He Yan. Fully Automatic Operation System Based on CBTC[J]. Urban Rapid Rail Transit, 2006, 19(3): 34-36.
[3]康峰.适用于FAO互联互通系统的VOBC远程唤醒通信流程[J].铁路通信信号工程技术，2019，16(9):89-93.
Kang Feng. Communication Process of VOBC Remote Wake-up for Interoperability of FAO System[J]. Railway Signalling & Communication Engineering, 2019, 16(9): 89-93.
[4]张艳兵，王道敏，肖衍.城市轨道交通全自动驾驶的发展与思考[J].铁道运输与经济，2015，37(9):70-74.
Zhang Yanbin, Wang Daomin, Xiao Yan.Development and Thoughts on Full-Automatic Operation of Urban Rail Transit[J]. Railway Transport and Economy, 2015, 37(9): 70-74.
[5] Ming Chai, Bernd-Holger Schlingloff. System Monitoring with A Five-valued LTL[J]. Multiple-Valued Logic and Soft Computing, 2016(26): 33-54.
[6]喻钢，刘晓文，熊静，等.高速铁路列控中心软件安全性需求形式化建模[J].铁道学报，2013，35(7):74-79.
Yu Gang, Liu Xiaowen, Xiong Jing, et al. Formalized Modeling of Safety Requirements of High-Speed Train Control Center Software System[J]. Journal of the China Railway Society, 2013, 35(7): 74-79.
[7]李中浩.城市轨道交通CBTC互联互通发展趋势及建议[J].城市轨道交通研究，2018，21(5):12-15.
Li Zhonghao. Development Trend of Urban Rail Transit CBTC Intercon-Nection/Intercommunication and Some Suggestions[J].Urban Mass Transit, 2018, 21(5): 12-15.
[8]谭力天，陈昕，李澎东，等.基于统计学模型的CBTC系统ATO停车精度自适应优化算法[J].铁路通信信号工程技术，2020，17(8):78-84.
Tan Litian, Chen Xin, Li Pengdong, et al.Adaptive Optimization Algorithm for ATO Stopping Accuracy of CBTC System Based on Statistical Model[J]. Railway Signalling & Communication Engineering, 2020, 17(8): 78-84.
[9]李晶.城轨全自动驾驶信号系统方案设计及运营场景分析[J].铁道通信信号，2016，52(2):48-52.

基于形式化方法的城轨FAO系统在线危险预测技术

Online Hazard Prediction of FAO Based on Formal Verification

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献

相关文章 1

编辑推荐

Metrics

本文评价