摘要
计算机联锁系统是铁路信号控制系统中最为基础的核心设备,是有着苛刻安全要求的复杂控制系统.传统开发方法很难完备证明系统满足既定的安全需求,介绍采用Prover形式化开发工具对联锁软件安全需求进行形式化验证.通过模型检验的形式化验证方法,遍历系统输入变量的所有状态空间,验证联锁特定应用满足系统安全需求的要求,确保系统的安全性得以正确实现.基于Prover工具,采用面向对象的高级编制语言PiSPEC,模型化代码设计和调试工具,自动生成定制化开发文档,为基于布尔逻辑的联锁软件的安全验证提供了解决方案,在保证系统安全性的基础上,以全状态空间查找反例的检验方法进一步提升产品的质量.
NETL