随着城市规模的发展，城市轨道交通系统在城市中的角色也越来越重要。城市轨道交通信号系统是保证列车运行安全，实现行车指挥和列车运行现代化，提高运输效率的关键系统设备。基于通信的列车控制(CBTC)系统代表着信号系统的发展方向。计算机联锁系统(CBI)是CBTC的重要组成部分，它能实现对信号机、道岔等设备的严格控制。要提高联锁系统的安全性和可靠性，在设计开发过程中必须有相应的措施。本文从建模角度出发研究联锁系统，为联锁系统的开发提供参考和指导，主要做了以下几方面的工作。　　 本文介绍了计算机联锁的基本原理和结构，分析了联锁软件的功能需求，为联锁逻辑中的进路控制、道岔控制、屏蔽门控制等业务流程进行了UML建模，进而指导联锁系统的设计及编码等工作。　　 本文提出了一种基于时间自动机的进路控制流程模型。将联锁进路控制过程分解为进路选排、道岔控制、进路锁闭、信号控制、进路取消等子过程，对各子过程分别建模并组建了时间自动机网络。　　 本文利用系统分析和验证工具UPPAAL，对进路控制流程的时间自动机网络进行了仿真和验证。根据联锁需求抽象和提取形式化逻辑表达式，分别从功能性、时序性和安全性角度进行了验证和分析。研究结果表明，借助时间自动机模型及其验证工具UPPAAL，能够尽早发现联锁软件设计中出现的错误，提高开发效率，保证联锁系统的安全性。