摘要
联锁表是联锁安全逻辑的体现,本文针对联锁表数据的安全逻辑验证问题,提出一种基于CSP的验证方法。首先对联锁表数据进行建模,将联锁表数据抽象为调度员、道岔、信号机、区段和联锁控制器5个进程的并发组合模型,并对各进程进行建模。依据联锁系统安全约束条件,从功能性和安全性两个方面,通过对模型正确性的验证来说明数据的安全逻辑正确性。最后以北京地铁亦庄站联锁表数据的安全逻辑验证为例,说明该方法的可行性。
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.
出处
《铁路计算机应用》
2015年第5期53-56,60,共5页
Railway Computer Application
基金
北京市科委项目(KWH13001531)
轨道交通北京实验室项目(W13H100061)
关键词
CBTC
联锁表逻辑
CSP
Communication Based Train Control（CBTC）
interlock table logic
Communicating Sequential Processes（CSP）
