黄友能，张鹏基，侯晓鹏，唐　涛

(1.北京交通大学 电子信息工程学院，北京　100044；2.北京交通大学 轨道交通运行控制系统国家工程研究中心，北京　100044)

基于通信的列车控制系统(Communication Based Train Control,CBTC)是保证城市轨道交通列车安全、高效运行的系统，其区域控制器(Zone Controller,ZC)子系统主要实现为管辖范围内列车计算移动授权(Movement Authority,MA)、区域控制器边界切换等功能[1]，这些功能的安全性是保障行车安全的基础，因此针对ZC子系统功能的安全验证就显得尤为重要。

ZC子系统主要通过无线传输方式接收车载子系(Vital OnBoard Computer,VOBC)的信息，因此在车地通信过程中不可避免会出现信号延迟或发送失败等情况，同时，由于ZC子系统在同一时间段内会与管辖范围内的所有列车进行交互，因此要求该系统应具有较强的并发性与实时性。另外，ZC子系统在计算移动授权的过程中，需要考虑列车连续变化参数(距离、速度和加速度等)的演化过程，以及设备交互的一些离散事件，具有明显的混成特性[2]。

关于列车控制系统安全验证的既有研究工作，有的针对系统的并发性与实时性进行建模与验证，如同济大学的徐中伟教授等利用Petri网模型和故障树实现了对联锁软件的安全性评估等[3]，但缺少相应的验证环节。有的针对系统混成特性进行研究，如北京交通大学的吕继东博士利用混合通信进程对系统进行建模仿真，但缺少相应的验证软件[4]。北京交通大学的刘金涛博士利用动态微分逻辑形式化语言对CTCS-3级列车控制系统进行了仿真与验证，但验证过程需要大量的推导公式，效率和重用性都较低。……