基于B方法的轨道交通控制系统配置数据的形式化验证  

Formal Verifi cation of Confi guration Data of Rail Transit Control System Based on B Method

作　　者：程鹏[1] 王恪铭[1,2] 王峥 姚文华 韩程 Cheng Peng;Wang Keming;Wang Zheng;Yao Wenhua;Han Cheng(National-Local Joint Engineering Laboratory of System Credibility Automatic Verifi cation,Southwest Jiaotong University,Chengdu 610031,China;School of Computing and Artifi cial Intelligence,Southwest Jiaotong University,Chengdu 614202,China;CRSC Research&Design Institute Group Co.,Ltd.,Beijing 100070,China;TongHao GBA(Guangzhou)Smart Control Co.,Ltd.,Guangzhou 511400,China)

机构地区：[1]西南交通大学系统可信性自动验证国家地方联合工程实验室,成都610031 [2]西南交通大学计算机与人工智能学院,成都614202 [3]北京全路通信信号研究设计院集团有限公司,北京100070 [4]通号粤港澳(广州)交通科技有限公司,广州511400

出　　处：《铁路通信信号工程技术》2022年第5期7-16,共10页Railway Signalling & Communication Engineering

基　　金：国家重点研发计划项目(2016YFB1200602)。

摘　　要：轨道交通控制系统对安全性和可靠性要求极高,其正常运行依赖于正确的配置数据,因而采用有效的方法保证配置数据的正确性显得十分重要。以轨道交通控制系统的配置数据为研究对象,选取道岔、信号机、轨道区段、进路等站场型信号设备数据为研究案例,基于各个配置数据的站场型数据结构,先用自然语言描述各个配置数据和配置数据需要满足的静态规则,再使用B语言形式规约各个配置数据及其所需要满足的静态规则,建立静态形式化模型,最后使用ProB模型检验工具,验证分析已生成的各个配置数据是否满足静态规则。验证结果表明,使用B方法对轨道交通控制系统配置数据进行形式化验证,有效提高配置数据正确性,进而为轨道交通控制系统的正常运行提供可靠保障。Rail transportation control system requires high safety and reliability,and its normal operation depends on correct confi guration data.Therefore,it is very important to adopt eff ective ways to ensure the correctness of confi guration data.In this paper,the confi guration data of the rail transportation control system is taken as the research object,and the station signaling data such as turnout,signal,section and route are selected as the research cases.Based on the station data structure of each confi guration data,the confi guration data itself and the static rules that each confi guration data needs to satisfy are fi rstly described with natural language.Then,each confi guration data and the static rules that need to be satisfi ed are defi ned by B language,and the static formal model is established.Finally,ProB model checking tool is used to verify and analyze whether the generated confi guration data satisfi ed the static rules.The verifi cation results show that using B method to formalize the confi guration data of the rail transportation control system can eff ectively improve the correctness of the confi guration data and provide a reliable guarantee for the normal operation of the rail transportation control system.

关 键 词：轨道交通控制系统 配置数据 B方法 形式化验证 

分 类 号：U284.48[交通运输工程—交通信息工程及控制]