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