我国的城市轨道交通行业在近年来实现了飞跃式发展,而其运行系统即基于通信的列车运行控制(Communication Based Train Control,CBTC)系统凭借自身可靠、安全、高效的性质成为了城市轨道列控系统的主流趋向。在城市轨道交通中,列车通过获取移动授权(Movement Authority,MA)信息来指导它的安全运行。因此,移动授权功能的安全实现至关重要。但由于该功能逻辑复杂且实时性较强,其内部的各模块若出现任何细小的错误或设计的缺陷都有可能致使无法弥补的结果发生。为了更加准确地找出各模块中可能存在的二义性或不可达性,在对功能系统开发的过程中,采用形式化的方法对移动授权功能分析建模,并检验各模块的功能要求,对于城市轨道交通安全有着极其重要的意义。本文的研究对象为CBTC系统的移动授权功能,采用时间自动机理论对该功能进行详细的描述和分析,利用模型验证工具UPPAAL检验该功能的顽健性、实时性、可达性和安全性。首先,分析CBTC的基本构成和工作原理,尤其重点分析了移动授权的功能原理。从不同功能模块的角度,分别建立列车筛选模块、列车管理模块、安全位置模块、障碍物遍历模块和移动授权生成模块的时间自动机模型,从而构成移动授权的时间自动机网络模型。其次,分析不同的运行场景下,移动授权功能按照不同的逻辑流程实现的过程,其中各模块功能是由不同的设备信息交互实现的,从而建立各场景下移动授权的分层结构。将分层结构思想引入时间自动机理论,建立各场景下移动授权的时间自动机网络分层模型,分别包括顶层、场景层、功能层和设备层。最后,在UPPAAL的模拟器窗口中对网络模型进行模拟仿真,得到表示子模型间信息交互的消息顺序图。采用巴科斯范式(Backus-Naur Form,BNF)语法编译出不同模型在功能和安全方面的验证语句,并在验证器窗口中进行检验,实现了对功能模型的顽健性、实时性、可达性和安全性的验证。为后期CBTC系统功能的深层次研究提供了理论参考,且层次时间自动机理论也有效缓解了建模时的复杂流程与逻辑问题,可应用于城市轨道交通控制系统的开发与验证。