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

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

Formal method applied to safety verification for computer interlocking software

The Interlocking System is a safety critical system. Its safety cannot be guaranteed only by testing. Formal verification can be used to verify the consistency between the applied logic and the safety requirements of the System. In this article, the general safety requirements were instantiated with the specific station layout. Then the specific safety requirements were verified through inputting them to the SAT induction constraint solver. The completeness of the method was guaranteed by covering all the instances, all the cycles and all the state space of each cycle.