基于Prover的联锁软件形式化验证过程研究

计算机联锁系统是铁路信号控制系统的核心设备,是有着苛刻安全要求的复杂控制系统。本文采用Prover形式化开发工具对联锁软件安全需求进行形式化验证。通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间.验证联锁特定应用满足系统安全需求,确保系统的安全性得以正确实现。在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量。

Formal Verification Process of Interlocking Software Based on Prover

The computer interlocking system is the core equipment in railway signaling control system and complex control system with strict safety requirements.So,we adopt formal method to verify the safety requirements of interlocking software based on the Prover tool.Using a model-check formal verification method,all the state space of the system's input variables are traversed to judge whether interlocking specific applications can meet the system safety requirements so as to ensure that the safety of the system is realized properly.On the basis of guaranteeing the safety of the system,the verification method of searching counter examples in whole state space can further improve the quality of the products.