科研之友
微信
新浪微博
Facebook
分享链接
摘要
为解决目前安全苛求系统研发中的功能安全问题，以用于轨旁设备联锁控制的道岔控制系统为研究对象，基于系统需求规范，使用形式化软件开发方法（B方法）对系统的功能逻辑建立形式化模型，完成对需求规范、系统功能及决策过程的验证，最终生成C语言形式的可执行代码。在分析系统各类属性与联锁逻辑关系的基础上，使用一阶逻辑和公理化集合论的数学方式，严格定义系统各层的B语言模型。通过对不变式的证明义务进行证明，验证系统中的安全、时间特性，检查出需求规范中的缺陷，提出增强系统稳健性的改进方案，进一步修正系统设计原型。通过不变式冲突和死锁检验进一步确认系统的正确性。研究表明，在所有证明义务通过机器自动证明和手动交互式证明的验证后，B模型自动生成的C代码能够正常运行并且功能满足实际联锁需求。将形式化方法应用于系统开发的全过程，所使用的技术路线及开发方法可以有效提高道岔控制系统的安全可靠性，并减少编码阶段工作量，对其他安全苛求系统的开发有重要参考意义。
-
单位西南交通大学; 北京全路通信信号研究设计院集团有限公司
