典型文献
基于B方法的轨道交通控制系统配置数据的形式化验证
文献摘要：
轨道交通控制系统对安全性和可靠性要求极高,其正常运行依赖于正确的配置数据,因而采用有效的方法保证配置数据的正确性显得十分重要.以轨道交通控制系统的配置数据为研究对象,选取道岔、信号机、轨道区段、进路等站场型信号设备数据为研究案例,基于各个配置数据的站场型数据结构,先用自然语言描述各个配置数据和配置数据需要满足的静态规则,再使用B语言形式规约各个配置数据及其所需要满足的静态规则,建立静态形式化模型,最后使用ProB模型检验工具,验证分析已生成的各个配置数据是否满足静态规则.验证结果表明,使用B方法对轨道交通控制系统配置数据进行形式化验证,有效提高配置数据正确性,进而为轨道交通控制系统的正常运行提供可靠保障.
文献关键词：
轨道交通控制系统;配置数据;B方法;形式化验证
中图分类号：
作者姓名：
程鹏;王恪铭;王峥;姚文华;韩程
作者机构：
西南交通大学系统可信性自动验证国家地方联合工程实验室,成都 610031;西南交通大学计算机与人工智能学院,成都 614202;北京全路通信信号研究设计院集团有限公司,北京 100070;通号粤港澳(广州)交通科技有限公司,广州 511400
文献出处：
引用格式：
[1]程鹏;王恪铭;王峥;姚文华;韩程-.基于B方法的轨道交通控制系统配置数据的形式化验证)[J].铁路通信信号工程技术,2022(05):7-16
A类：
轨道交通控制系统,站场型数据结构
B类：
系统配置,配置数据,形式化验证,安全性和可靠性,取道,道岔,信号机,区段,信号设备,先用,自然语言,需要满足,语言形式,规约,ProB,模型检验,检验工具,验证分析
AB值：
0.195771
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
