随着我国经济的迅速发展,城市的人口大量增加,城市交通运输压力不断增大。城市轨道交通以其速度快、运输力强、舒适性高以及对环境造成的污染低等优点成为大中型城市解决拥堵问题的首选,CBTC (Communication Based Train Control)技术在此背景下应运而生,并以其显著优势逐渐成为城市轨道交通信号系统的首选方案。联锁系统作为CBTC系统的重要组成部分,是行车安全的重要保障设备。联锁系统的安全要求级别较高,因此采用高安全性软件开发联锁系统是十分必要的。高安全性应用开发环境SCADE (Safety-Critical Application Development Environment)为软件开发人员提供了完整的基于模型的开发解决方案,以此来降低开发成本、减少开发风险和缩短验证时间。本文以郑州地铁一号线的一个联锁区为分析对象,利用SCADE对联锁的主要功能进行建模并验证。首先对国内外的联锁系统研究情况以及联锁逻辑建模的情况进行了探讨,对CBTC的主要结构和子系统进行了阐述。研究了SCADE的基础理论,探讨了基于同步编程理论的两种建模方法：数据流图方法和安全状态机方法,分析了建模机制的语义基础、模型特点以及适用对象。分析了联锁的主要内容以及与其他系统的信息传递,并将联锁系统四个主要模块：道岔模块、进路模块、信号模块和解锁模块,利用SCADE中数据流图的方法分别对其进行了逻辑设计并建立模型,最终建立整体模型。最后,使用SCADE的仿真器与验证器对建立的主要模块进行仿真并验证分析各个模型设计的正确性,确保了模型的安全性。用代码生成器KCG对模型自动生成C代码并进行研究分析。采用SCADE开发联锁系统满足了联锁系统对安全性的高要求,SCADE在联锁软件的开发中具有广阔的应用前景。