中图分类号： U284.48
文献标识码： 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

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