GoA4级全自动运行系统驾驶模式切换的安全性建模
信息技术与网络安全 2期
谢迎锋1，王 蓉2
(1.北京全路通信信号研究设计院集团有限公司，北京100070；2.北京交通大学，北京100040)
摘要： 摘 要： 为验证具体场景下GoA4级全自动运行系统驾驶模式是否符合对应技术规范，提出一种基于时间自动机的形式化建模与验证方法。GoA4级的驾驶模式是系统自动切换，且增加了自动实现蠕动模式和远程限制监督模式切换。选取全自动运行模式、蠕动模式和远程限制监督模式的相关切换作为建模对象，提取全自动运行系统规范中的功能需求，生成对应流程的消息顺序图，并对模块间的交互信息进行分析；然后，以基于时间自动机的数学理论为基础，采用时间自动机建模方法对RM模式向FAM模式切换、FAM模式向CAM模式切换、FAM模式向RRM模式切换进行建模；最后，采用巴科斯范式(BNF)语法，达到了对其安全性、受限活性、实时性进行验证的结果。
中圖分類號： U284.48
文獻標識碼： A
DOI： 10.19358/j.issn.2096-5133.2022.02.003
引用格式： 謝迎鋒，王蓉. GoA4級全自動運行系統駕駛模式切換的安全性建模[J].信息技術與網絡安全，2022，41(2)：15-19.
文獻標識碼： A
DOI： 10.19358/j.issn.2096-5133.2022.02.003
引用格式： 謝迎鋒，王蓉. GoA4級全自動運行系統駕駛模式切換的安全性建模[J].信息技術與網絡安全，2022，41(2)：15-19.
Security modeling of driving mode switching in GoA4 level automatic operation system
Xie Yingfeng1，Wang Rong2
(1.CRSC Research & Design Institute Group Co.，Ltd.，Beijing 100070，China； 2.Beijing Jiaotong University，Beijing 100040，China)
Abstract： Abstract： In order to verify whether the driving mode of GoA4 level automatic operation system conforms to the corresponding technical specifications in specific scenarios, a formal modeling and verification method based on time automata was proposed.GoA4 driving mode is automatic system switching, and adds automatic creeping mode and remote limit supervision mode switching.In this paper, the relevant switches of fully automatic operation mode, peristaltic mode and remote restriction supervision mode were selected as modeling objects, and the functional requirements in fully automatic operation system specifications were extracted, the message sequence diagram of corresponding processes was generated, and the interaction information between modules was analyzed. Then, based on the mathematical theory of time automata, the time automata modeling method was used to model the switch from RM mode to FAM mode, from FAM mode to CAM mode, and from FAM mode to RRM mode.Finally, the security, limited activity and real-time performance of the model were verified by using BNF syntax.
Key words : driving mode；automatic operation system；UPPAAL；security verification
0 引言
全自動運行系統(Fully Automatic Operation，FAO)是基于現代計算機、通信、控制和系統集成等技術實現列車運行全過程自動化的新一代城市軌道交通系統。國際公共交通協會(UITP)統計，預計到2025年全球將有2 300公里線路采用全自動運行系統。隨著全自動運行系統的發展，對其安全性、實時性、功能性的要求越來越高[1]。GoA3(Grades of Automation 3)級和GoA4(Grades of Automation 4)級的一個很重要的區別是，GoA3級是司機確認之后實現列車運行等級從高級向低級以及駕駛模式的切換，但是對于GoA4級全自動運行系統，是系統自動實現駕駛模式切換(Driving Mode Wwitch，DMS)。
在基于通信的列車運行控制系統(Communication Based Train Control System，CBTC)中，列車駕駛模式和運行等級的正確切換，對保證列車安全有重要影響，駕駛模式的正確建立和轉換直接影響到行車安全與運營效率。2017年11月15日新加坡地鐵事故的其中一個原因就是駕駛模式轉換不正確。因此，對列車運行的駕駛模式的研究有重要意義。
本文詳細內容請下載：http://m.tom3567.com/resource/share/2000003945。
作者信息：
謝迎鋒1，王 蓉2
(1.北京全路通信信號研究設計院集團有限公司，北京100070；2.北京交通大學，北京100040)
此內容為AET網站原創，未經授權禁止轉載。