社会经济的快速发展推动了我国城市轨道交通的建设进程,基于通信的列车运行控制系统(Communication-Based Train Control System,CBTC)以其高效、可靠、安全等优点迅速在城市轨道交通建设中得到广泛应用。在城市轨道交通中,CBTC系统通过为每一列通信列车提供移动授权(Movement Authority,MA)来实现列车安全间隔运行。移动授权的计算和分配是由CBTC轨旁设备区域控制器(Zone Controller,ZC)完成的。鉴于ZC系统的高安全性要求,本文采用高安全应用开发环境(Safety critical application development environment,SCADE)对区域控制器核心功能移动授权计算和生成进行建模与仿真验证,使系统的设计能够满足安全关键性系统的要求。本文采用SCADE数据流图方式对列车在运行过程中的注册、注销以及列车数据的更新管理等功能建立模型,记录和监督ZC管辖范围内的列车信息变化。然后根据移动授权计算原理分析了列车单车运行以及列车追踪运行等不同情况,采用数据流图方式对移动授权计算功能模块建立了 SCADE模型。接下来分析列车在CBTC区域主要运营场景,根据列车在不同场景下对MA需求的不同采用SCADE数据流图和安全状态机两种建模方式完成对列车主要运营场景建模。最后,利用SCADE提供的仿真器对列车典型运营场景进行仿真,并且提出安全属性对移动授权计算功能进行形式化验证,结果表明设计的模型满足功能正确性和安全性。