城轨CBTC系统联锁表数据安全逻辑验证方法研究

联锁表是联锁安全逻辑的体现,本文针对联锁表数据的安全逻辑验证问题,提出一种基于CSP的验证方法。首先对联锁表数据进行建模,将联锁表数据抽象为调度员、道岔、信号机、区段和联锁控制器5个进程的并发组合模型,并对各进程进行建模。依据联锁系统安全约束条件,从功能性和安全性两个方面,通过对模型正确性的验证来说明数据的安全逻辑正确性。最后以北京地铁亦庄站联锁表数据的安全逻辑验证为例,说明该方法的可行性。

Data safety logic verification method of interlock table for Urban Transit CBTC System

The interlock safety logic was reflected by interlock table. This paper proposed a verification method based on CSP (Communicating Sequential Processes) to solve the data safety logic verification problem of interlock table, modeled data of the interlock table at first, abstracted five processes of dispatchers, switch, signal machine, segment and interlocking controller from the data of interlocking table, and further modeled the processes respectively. The correctness of the model was verified from the functional and safety aspects. At last, an example of data safety logic verification with the interlock table in Yi Zhuang Station of Beijing Metro illustrated the feasibility of the method.