随着城市化进程的推进和城市人口的增加,人们越来越意识到城市轨道交通的优点,全国各地也在大力兴建城市轨道交通。基于通信的列车运行控制系统(Communication-based Train Control, CBTC)具有安全、高效等优点,是现代城市轨道交通列车运行控制系统今后的发展方向。区域控制器(Zone Controller, ZC)是CBTC系统的核心地面设备,它的主要功能是为控制范围的列车计算并分配移动授权(Movement Authority, MA)保证列车在线路上的运行安全。ZC是安全苛求系统,必须符合SIL-4级的安全等级需求,因此在对ZC系统设计和开发时,要用最为安全性高的方法。高安全性应用开发环境SCADE运用基于模型的方式为安全苛求系统提供完整的解决方案,用它来开发ZC这种高安全性的软件是十分合适的。本文采用SCADE对ZC建模,主要是对ZC的主要功能——列车管理功能和MA计算功能进行模型的建立。列车管理功能的核心是对列车状态的管理,不管列车处于何种运行状态,ZC都必须有效的对列车进行管理。MA计算是ZC的核心功能,ZC实时的与CBTC的其他子系统通信,为控制范围的列车计算MA,确保列车的运行安全。对于列车管理功能,采用SCADE的安全状态机来进行模型的建立；对于MA计算功能,采用SCADE的数据流图来进行模型的建立。最后,利用SCADE的仿真和验证工具对建立的列车管理模型和MA计算模型进行验证。对模型进行了仿真测试,保证了系统的正确性。对模型进行覆盖率分析,确保了仿真测试的完备性。使用SCADE的形式化验证功能对系统的安全属性进行验证,证明了模型的安全性。