区域控制器(Zone Controller-ZC)是基于通信列车运行控制系统(Communications Based Train Control system-CBTC)系统的地面控制核心设备,负责列车移动授权的计算和运行安全保障。ZC是一个复杂庞大的安全关键系统,其软件开发在规范刻画、设计、验证等诸多方面面临挑战。近年来,基于模型的软件开发方法在安全关键领域逐渐被认可,本文研究基于SCADE模型的ZC软件开发方法,主要工作体现在如下方面：(1)以轨道交通控制系统为背景,研究了安全关键性系统的相关安全标准,分析了模型驱动开发的优势,并介绍了SCADE模型开发工具。(2)研究了SCADE理论基础一同步编程理论。研究了LUSTRE语言的语法规则和LUSTRE语言对反应式系统的进行模型描述的抽象方法。分析了数据流图和安全状态机这两种形式化建模机制的语义基础、建模方法以及模型的特性。研究了同步编程理论对模型的两种确认方法模拟仿真和形式化验证。(3)采用SCADE模型工具,对ZC进行建模。对ZC进行了形式化描述,建立ZC的SCADE,总体模型。通过分析区域控制器控制列车的典型场景,将ZC的主要功能划分为列车管理功能、进路匹配功能和MA计算功能,详细的设计了各功能的软件流程。采用安全自动机建模机制,建立了列车管理功能的模型；采用数据流建模机制,建立了进路匹配功能和MA计算功能的模型。(4)采用SCADE仿真与验证工具,对ZC模型进行检验。采用故障模式及影响分析方法,对ZC的主要功能进行了安全分析。使用SCADE模拟仿真模块,对模型进行了测试,使用SCADE形式化验证器,对模型的安全属性进行了验证,从而确认了模型的正确性。通过对课题的研究,本文得出以下结论：基于SCADE模型的开发避免了对软件的重复性描述,避免了人工编写代码,能在系统设计初期发现设计缺陷,提高了软件质量和开发效率。