基于通信的列车控制系统(Communication-based Train Control,CBTC)已成为城市轨道交通信号系统的首选解决方案。作为其中关键部分,计算机联锁(Computer Based Interlocking,CBI)系统负责保障行车安全的逻辑运算,是典型的安全苛求系统。为适应现代城轨高密度和高安全性的行车要求,联锁系统增加了新的功能要求,其逻辑运算更为复杂。因此,如何保证城轨联锁系统开发的安全性和正确性显得尤为重要。本文利用高安全应用开发环境(Safety critical application development environment,SCADE)图形化建模的方式对城轨联锁系统进行描述,以减少传统文本方式描述的模糊性,满足开发高安全性系统的要求。针对CBTC系统有CBTC模式和后备模式两种运营模式的特点,以具体联锁区的站场图为例,在详细分析了联锁数据的基础上,根据信号设备的特点和联锁与其他系统的交互信息定义合适的数据结构。将进路控制划分为进路建立和进路解锁两个模块,其中进路建立包括进路请求,进路检查,进路方向锁闭、保护区段锁闭,信号控制,进路解锁模块分为正常解锁,折返解锁,保护区段解锁、取消解锁、故障解锁。对以上各模块采用数据流图和状态机结合的方式进行建模。对于自动通过,自动触发进路单独设计。最后编写测试案例,利用SCADE的simulate对进路控制流程进行仿真。设计CBTC模式下信号机灭灯的安全属性,建立安全属性与观测器组合模型,对系统功能进行形式化验证,并对验证结果进行分析,表明设计的模型满足功能要求和安全要求。