Abstract: In order to solve the realistic problems such as that the current mainstream validation method for safety critical system cannot prove whether the system exists defects, this paper researches to set up a formalized model for software function logic to achieve the verification of software requirements specification, and finally generate code C by taking the point control system for trackside equipment interlocking control as the specific research object, according to the software requirements specification, aiming at the safety point control system function, and using formal approach to software development method (method B). The research shows that the code C automatically generated by formal model can run normally and meet the software requirements of point control system after passing the verifications of automatic machine proof and manual interactive proof. In this paper, the formal method is applied to the whole process of software development of point control system, the technical route and development method used can effectively improve the safety and reliability of point control system, and reduce the workload in the coding stage, which has important reference significance to the development of other safety critical systems.

Key words: point control system, method B, formal verification, code generation

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

关键词: 道岔控制系统, B方法, 形式化验证, 代码生成