形式化方法应用于计算机联锁软件的安全验证研究

摘要

铁路信号系统中的联锁系统对安全性要求极高,仅通过普通的功能测试无法保障其安全性.采用形式化验证的方式可以验证联锁系统的应用逻辑与安全需求的一致性.将通用安全需求结合具体的站场图进行实例化,得到具体的安全需求后输入带归纳功能的布尔可满足问题(SAT)约束求解器进行验证,通过覆盖所有的实例、所有周期以及每个周期所有的状态空间,保证了验证方法的完备性.