城市轨道交通是解决大城市拥堵、方便百姓出行的重要手段之一。基于通信的列车自动控制系统CBTC (Communication Based Train Control)是保证城市轨道交通行车安全、高效运营的系统,区域控制器ZC (Zone Controller)作为CBTC系统的关键设备,具有实现列车管理、移动授权计算等安全功能。本文针对ZC子系统功能的安全验证,传统仿真、测试的方法存在操作量大、完备性不强,单一形式化方法难以描述ZC子系统复杂功能的问题,给出了一种基于TCSP (Timed Communicating Sequential Process)的分层建模与验证方法来对ZC子系统安全性验证进行了研究。本文采用的分层建模方法是将ZC子系统分为系统层和功能层,层间靠系统数据关联,并采用加入时间机制的建模方法来表达系统的实时性,用UML-RT (Unified Modeling Language-Real Time)顺序图形象直观的描述系统交互层,利用标签迁移系统LTS (Labelled Transition System),实现半形式化UML-RT到形式化语言TCSP的转换,结合内部功能处理层的TCSP模型,建立整体的基于TCSP的ZC子系统分层模型,层次清晰、要素明确。在现有的通信顺序进程验证软件PAT(Process Analysis Toolkit)上运行,基于LTL (Linear Temporal Logic)断言对技术规范提出的数据相关需求进行验证。论文选取任务启动及正常行车场景案例进行分析。车地交互系统每个周期根据系统输入和控制规则得到移动授权MA (Movement Authority),在没有故障和突发事件的情况下,下个周期依照相同的规则得到对应MA信息,若有回撤现象发生,不符合安全条件。根据跳变故障迹找到系统存在的问题并给出解决方案,使ZC子系统满足需求规范相关要求,最大限度的避免系统设计可能的缺陷和错误,确保ZC子系统功能的正确性,对进一步提高ZC子系统安全性有重要意义。