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.rjjo.cn/resource/share/2000003945。
作者信息：
謝迎鋒1，王 蓉2
(1.北京全路通信信號研究設計院集團有限公司，北京100070；2.北京交通大學，北京100040)
此內容為AET網站原創，未經授權禁止轉載。