典型文献
基于B方法的道岔控制系统形式化建模与验证
文献摘要：
为解决目前安全苛求系统研发中的功能安全问题,以用于轨旁设备联锁控制的道岔控制系统为研究对象,基于系统需求规范,使用形式化软件开发方法(B方法)对系统的功能逻辑建立形式化模型,完成对需求规范、系统功能及决策过程的验证,最终生成C语言形式的可执行代码.在分析系统各类属性与联锁逻辑关系的基础上,使用一阶逻辑和公理化集合论的数学方式,严格定义系统各层的B语言模型.通过对不变式的证明义务进行证明,验证系统中的安全、时间特性,检查出需求规范中的缺陷,提出增强系统稳健性的改进方案,进一步修正系统设计原型.通过不变式冲突和死锁检验进一步确认系统的正确性.研究表明,在所有证明义务通过机器自动证明和手动交互式证明的验证后,B模型自动生成的C代码能够正常运行并且功能满足实际联锁需求.将形式化方法应用于系统开发的全过程,所使用的技术路线及开发方法可以有效提高道岔控制系统的安全可靠性,并减少编码阶段工作量,对其他安全苛求系统的开发有重要参考意义.
文献关键词：
道岔控制系统;B方法;形式化验证;代码生成
中图分类号：
作者姓名：
刘宁;韩程;王峥;侯锡立;王恪铭
作者机构：
西南交通大学唐山研究生院,河北唐山 063000;北京全路通信信号研究设计院集团有限公司,北京 100070;通号粤港澳(广州)交通科技有限公司,广州,511400;西南交通大学系统可信性自动验证国家地方联合工程实验室,成都 610031
文献出处：
引用格式：
[1]刘宁;韩程;王峥;侯锡立;王恪铭-.基于B方法的道岔控制系统形式化建模与验证)[J].铁路通信信号工程技术,2022(06):5-11
A类：
道岔控制系统,公理化集合论
B类：
系统形式,形式化建模,解决目前,苛求,系统研发,功能安全,轨旁设备,联锁控制,系统需求,软件开发方法,决策过程,终生,语言形式,类属,联锁逻辑,一阶逻辑,数学方式,语言模型,不变式,验证系统,时间特性,查出,增强系统,系统稳健性,改进方案,正系统,死锁,交互式,自动生成,形式化方法,系统开发,安全可靠性,发有,形式化验证,代码生成
AB值：
0.386899
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
