基于B方法的道岔控制系统形式化建模与验证OA
Formal Modeling and Verification of Point Control System Based on Method B
为解决目前安全苛求系统研发中的功能安全问题,以用于轨旁设备联锁控制的道岔控制系统为研究对象,基于系统需求规范,使用形式化软件开发方法(B方法)对系统的功能逻辑建立形式化模型,完成对需求规范、系统功能及决策过程的验证,最终生成C语言形式的可执行代码.在分析系统各类属性与联锁逻辑关系的基础上,使用一阶逻辑和公理化集合论的数学方式,严格定义系统各层的B语言模型.通过对不变式的证明义务进行证明,验证系统中的安全、时间特性,检查出需求规范中的缺陷,提出增强…查看全部>>
刘宁;韩程;王峥;侯锡立;王恪铭
西南交通大学唐山研究生院,河北唐山 063000北京全路通信信号研究设计院集团有限公司,北京 100070通号粤港澳(广州)交通科技有限公司,广州,511400北京全路通信信号研究设计院集团有限公司,北京 100070北京全路通信信号研究设计院集团有限公司,北京 100070
交通工程
道岔控制系统B方法形式化验证代码生成
《铁路通信信号工程技术》 2022 (6)
5-11,7
国家重点研发计划资助项目(2016YFB1200602)
评论