贺欢欢，陈永刚，罗雅允，张彩珍

(1.兰州交通大学自动化与电气工程学院，兰州 730070;2.兰州交通大学电子与信息工程学院，兰州 730070)

移动授权的形式化建模与验证

贺欢欢1，陈永刚1，罗雅允1，张彩珍2

(1.兰州交通大学自动化与电气工程学院，兰州 730070;2.兰州交通大学电子与信息工程学院，兰州 730070)

基于通信的列车运行控制系统(Communications-Based Train Control System， CBTC)相较于传统的基于轨道的列车运行控制系统，无论是从功能方面还是性能方面都有了很大的改进。在系统的研发过程中，对其进行建模和验证，能够发现系统设计的缺陷，进而保证系统的安全性和功能性。移动授权(Movement Authority， MA) 是CBTC系统的核心功能，用来保证列车的安全运行间隔。通过对移动授权生成原理的研究，采用时间自动机和其自动验证工具UPPAAL对其进行建模以及验证，验证结果表明，搭建的移动授权模型能够达到规定的安全要求和功能要求。因此UPPAAL能够对复杂的实时系统进行仿真验证。

CBTC；MA；时间自动机；UPPAAL

基于通信的列车运行控制系统CBTC相较于传统的基于轨道的列车运行控制系统具有安全性高、线路运输能力大、实时性好和轨旁设备少等优点。世界上主要的经济发达国家已经相继研发出了自己的基于通信的列控系统，并且已经趋于成熟。而我国CBTC系统的开发还处于初步阶段，移动授权的生成是联系CBTC系统中各子系统的纽带，并且直接影响行车效率和行车安全。采用形式化方法时间自动机对移动授权进行建模，并利用其自动验证工具UPPAAL对模型的功能性能和安全性能进行验证。……