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

Formal Modeling and Verification of CBTC Computer Interlocking System Based on Communication Sequential Process and B Method

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

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.