罗 娟，王燕芩

（卡斯柯信号有限公司，上海 200071）

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

罗 娟，王燕芩

（卡斯柯信号有限公司，上海 200071）

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

计算机联锁；安全需求；通用应用；形式化验证

联锁系统是涉及到生命财产安全的高安全性系统，其安全性除了体现在冗余结构的系统硬件上，还应考虑系统软件的安全性。软件的安全性需通过系统逻辑设计与安全需求的一致性和特殊的安全防护措施保证。在安全需求实现时，若存在系统需求描述不准确，则会造成需求设计实现不准确，这一系列因为人为失误可能导致最终的系统功能失效，威胁行车安全。为了确保系统需求的正确实现，本文提出形式化方法对既有联锁系统应用进行安全验证，确保系统实现与安全需求要求的一致性。联锁系统是铁路信号系统中的安全相关的重要系统，根据EN50128的要求，联锁系统的安全性需达到SIL4的安全等级，因此对其进行安全验证十分必要。

1 研究背景

对于安全相关的系统，在正常功能性需求外，含大量安全需求。……