信号系统是城市轨道交通的主要技术装备,它担负着指挥列车运行、保证行车安全、提高运输效率的重要任务。计算机联锁(CI)又是城市轨道交通信号系统的重要组成部分,它实现信号、道岔与进路的制约关系,从而保证了行车的安全。城市轨道交通的计算机联锁把联锁关系和ATP功能结合起来,不仅逻辑复杂,而且还增加了许多特殊的功能,对安全性、可靠性和实时性都提出了更高的要求。并且随着计算机技术的在信号系统的应用,传统的设计、分析和测试方法已经无法满足计算机联锁的安全需求。为此我们采用形式化的方法对联锁软件进行安全性设计和验证,以此来保证系统设计开发的正确性和安全性。论文以城市轨道交通计算机联锁软件的核心—进路控制过程为研究重点,根据安全苛求系统的设计要求,提出了联锁软件设计的“V”型框架。论文基于该框架提出的需求分析、系统设计、形式化建模、形式化需求分析和验证的总体思路展开研究。本文首先介绍了联锁软件的基本结构和原理,分析了联锁软件的功能需求和性能需求,在此基础上重点分析了联锁的进路控制流程,从进路的建立到解锁对进路控制的各个模块和消息处理流程进行了分析和设计。本文提出了基于时间自动机对进路控制流程进行建模。首先根据进路控制流程的各个功能模块分别建立子自动机,对于进路控制中的消息处理单独建立时间自动机模型。最后利用UPPAAL工具建立系统的时间自动机网络。基于时间自动机的形式化建模,利用有向图形象地描述系统的逻辑行为,通过加入时间约束集描述系统的实时性,从而避免了联锁软件设计中的不一致、模糊性和不完备性。最后,论文利用UPPAAL对进路控制流程的时间自动机网络进行了模拟仿真和验证。通过BNF语法提取待验证的形式化需求规范,利用UPPAAL验证工具对系统的功能性和安全性进行了验证和分析。研究结果表明,利用时间自动机模型及其验证工具的形式化建模和验证方法可以有效减少系统设计中的故障,为计算机联锁软件的设计完善提供了参考和指导。