基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证

作     者：王鲲 WANG Kun

作者机构：中国铁道科学研究院通信信号研究所北京100081 国家铁路智能运输系统工程技术研究中心北京100081 

出 版 物：《中国铁道科学》 (China Railway Science)

年 卷 期：2018年第39卷第3期

页      面：101-109页

核心收录：

学科分类：08[工学] 0802[工学-机械工程] 082302[工学-交通信息工程及控制] 0823[工学-交通运输工程] 0801[工学-力学（可授工学、理学学位）] 

基　　金：中国铁路总公司科技研究开发计划项目(J2016X001) 中国铁道科学研究院行业服务技术创新项目(2016YJ053) 

主　　题：城市轨道交通 CBTC 计算机联锁系统 形式化方法 通信顺序进程 B方法 

摘      要：针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实现通信顺序进程和B方法之间的同步。以1个实际站场为例,采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机,采用通信顺序进程对CBTC联锁系统与外部系统的并发交互行为建立进程,并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程同步,由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型。采用ProB工具对建立的CBTC联锁系统模型的安全性、无死锁性进行验证。发现并修改模型中的不一致、不完全、歧义等错误,从而验证了CBTC联锁系统的安全性和无死锁性,保证了系统的最终实现。