中圖分類號： U284.48 文獻(xiàn)標(biāo)識碼： A DOI： 10.19358/j.issn.2096-5133.2022.02.003 引用格式： 謝迎鋒，王蓉. GoA4級全自動運行系統(tǒng)駕駛模式切換的安全性建模[J].信息技術(shù)與網(wǎng)絡(luò)安全，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 引言
全自動運行系統(tǒng)(Fully Automatic Operation，F(xiàn)AO)是基于現(xiàn)代計算機(jī)、通信、控制和系統(tǒng)集成等技術(shù)實現(xiàn)列車運行全過程自動化的新一代城市軌道交通系統(tǒng)。國際公共交通協(xié)會(UITP)統(tǒng)計，預(yù)計到2025年全球?qū)⒂? 300公里線路采用全自動運行系統(tǒng)。隨著全自動運行系統(tǒng)的發(fā)展，對其安全性、實時性、功能性的要求越來越高[1]。GoA3(Grades of Automation 3)級和GoA4(Grades of Automation 4)級的一個很重要的區(qū)別是，GoA3級是司機(jī)確認(rèn)之后實現(xiàn)列車運行等級從高級向低級以及駕駛模式的切換，但是對于GoA4級全自動運行系統(tǒng)，是系統(tǒng)自動實現(xiàn)駕駛模式切換(Driving Mode Wwitch，DMS)。
在基于通信的列車運行控制系統(tǒng)(Communication Based Train Control System，CBTC)中，列車駕駛模式和運行等級的正確切換，對保證列車安全有重要影響，駕駛模式的正確建立和轉(zhuǎn)換直接影響到行車安全與運營效率。2017年11月15日新加坡地鐵事故的其中一個原因就是駕駛模式轉(zhuǎn)換不正確。因此，對列車運行的駕駛模式的研究有重要意義。
