城市轨道交通在通信、控制、计算机技术大发展的背景下已经成为许多国家和城市建设的重点。计算机联锁系统是城市轨道交通系统的重要组成部分,对防护列车运行安全具有重要意义。随着计算机技术在CBTC(Communication Based Train Control)联锁系统的广泛应用,系统的复杂性和不确定性大大增加,对系统的安全保障也随之变得更加困难,因此联锁系统在设计开发阶段需要有科学完备的分析和验证。由于传统的需求分析方法具有不完备的缺点,本文采用时间自动机的形式化方法对CBTC联锁系统进行建模分析,以此提高系统的安全性。本文首先对CBTC联锁系统进行了详细的介绍,分析了联锁系统的主要功能需求,并对联锁在进路控制流程中的功能模块进行了划分,分析了CBTC联锁系统进路控制的主要流程。然后,根据联锁逻辑过程以及时序流程,提取联锁系统的功能约束,依据时间自动机理论对CBTC联锁系统进路控制流程中的道岔模块、进路模块、信号机模块进行了形式化建模,主要包括道岔请求、道岔选排、道岔锁闭、信号请求、进路检查、区段锁闭、信号开放等功能模型,最后得到了CBTC联锁系统进路控制过程的时间自动机模型,并利用时间自动机的时钟约束特性设计了联锁系统的“缓放”、“缓吸”逻辑,最后利用共享全局变量和通道的方式组建了CBTC联锁逻辑的时间自动机网络。最后,借助时间自动机工具UPPAAL对时间自动机网络进行仿真得到进路控制流程的时序图,分析了系统模块之间的通信过程以及状态迁移；并人工提取所建进路控制系统的功能需求、安全需求、时间约束,在验证器中利用规范验证语言对其进行形式化描述并进行了形式化验证,表明联锁系统满足预期功能,证明了该方法在CBTC联锁逻辑分析中的可行性。