基于层次时间自动机的移动授权的建模与验证

基于通信的列车运行控制(communication based train control,CBTC)系统以其安全、可靠等性能优点在城市轨道交通的运营中得到广泛关注。它通过其核心功能,即为每一列通信列车提供移动授权(movement authority,MA),来实现列车安全间隔运行。针对功能安全和实时性等方面的不足,首先,建立移动授权的层次时间自动机(hierarchical time automaton,HTA)模型,其中嵌入了列车管理、安全位置、遍历障碍物和列车筛选模块,并对模块间的交互信息进行分析;其次,采用巴科斯范式(Backus-Naur form,BNF)语法对其特性进行描述;最后,利用UPPAAL对各特性验证。结果表明,移动授权模型满足实时性、顽健性、可用性、完整性、安全性5项需求,层次时间自动机理论适用于系统需求规范的验证。

Modeling and Verification of Movement Authority Based on Hierarchical Time Automaton

Communication Based Train Control (CBTC) system has been widely concerned in the operation of urban rail transit due to its safety, reliability and other performance advantages. It realizes the safe interval operation of trains through its core function that provides movement authority (MA) for each communication train. According to the deficiencies of functional security and real-time, firstly, the hierarchical time automaton (HTA) model for movement authority was established, the modules of train management, safety location, obstacle traversal and train screening were embedded, and the interactive information between the modules was analyzed. Secondly, Backus Naur-Form (BNF) grammar was adopted to describe its features. Finally, UPPAAL was used to verify the features. The results show that the movement authority model can meet the requirements of real-time, robustness, availability, integrity and security. Hierarchical time automata theory is suitable for the verification of system requirement specification.