摘要：中国的城市轨道交通已经进入了快速发展的时代,基于通信的列车自动控制(CBTC)系统作为当今主流的城市轨道交通的控制系统,其系统安全的重要性不言而喻,区域控制器(ZC)作为CBTC子系统之一,承担着列车管理,移动授权计算等与安全相关的功能。系统开发过程当中复杂系统的场景可导致需求描述出现逻辑漏洞,使整个系统产生逻辑上的冲突,本文面向区域控制器的不同场景,提取场景的需求规范,并进行建模和验证,以此来证明的区域控制器场景需求中有没有逻辑冲突,保证系统需求逻辑的正确性。本文首先基于区域控制器系统的结构及功能,从UML半形式化描述入手,按照模型转换规则得到CBTC区域控制器的CSP模型,并将模型转化成为PROB验证工具可以识别的CSPM语言,然后运用PROB软件对模型的死锁,活锁和确定性进行验证。最后提取出区域控制器的八个正常行车场景和三个故障场景描述的需求规范,然后运用CSP建模和验证方法对需求模型的逻辑性进行验证,证明了方法的可用性。