中国铁道科学2018，Vol.39Issue(3)：101-109,9.DOI:10.3969/j.issn.1001-4632.2018.03.14
基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证
Formal Modeling and Verification of CBTC Computer Interlocking System Based on Communication Sequential Process and B Method
摘要
Abstract
In view of the complexity of the CBTC interlocking system,a formal method based on the integration of Communication Sequential Process (CSP) and B method was proposed.Namely,a one-to-one mapping relationship was established between the communication events of CSP and the abstract machine operations of B method,to achieve the goal that communication events could affect the states of abstract machine by controlling abstract machine operations,and to realize the synchronization between CSP and the B method accordingly.Taking an actual station as example,B method was adopted to build abstract machines for the logic state calculation of CBTC interlocking system with complex state space.CSP was adopted to set up the processes for the concurrent interaction behaviors between CBTC interlocking system and external systems.Through the mapping relationship,the abstract machines of CBTC interlocking system and the processes of external interaction behaviors were synchronized,thus a formal model of CBTC interlocking system was established based on CSP and B method.The ProB tool was used to verify the safety,deadlock-free of the model of CBTC interlocking system.The errors in the model were found and modified,such as inconsistence,incompletion,ambiguity and so on.The safety and deadlock-free of CBTC interlocking system were verified,and the final implementation of the system was guaranteed.关键词
城市轨道交通/CBTC/计算机联锁系统/形式化方法/通信顺序进程/B方法Key words
Urban rail transit/CBTC/Computer interlocking system/Formal method/Communication sequential process/B method分类
交通工程引用本文复制引用
王鲲..基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证[J].中国铁道科学,2018,39(3):101-109,9.基金项目
中国铁路总公司科技研究开发计划项目(J2016X001) （J2016X001）
中国铁道科学研究院行业服务技术创新项目(2016YJ053) （2016YJ053）
