应用编码和继电器编码形式验证

验证器模块用于对能引起应用编码出现禁忌不安全状况的多种方案的搜索进行形式认证。该工具会发现不安全方案，进行相应的测试，然后在调试器中显示出来。工程师找出并改正不安全的逻辑，重新运行Prover iLock验证器。

该过程需重复进行，直至所有的不安全逻辑被纠正。这时，验证器模块会利用数学运算证实应用编码不可能出现任何PiSPEC安全说明中提到的不安全状况。

该方法同测试、模拟和回顾存在本质的不同。对一切可能的方案和事件组合进行测试、模拟，证实即便是最小的应用也是不可能的。 测试的方法会依据一个（潜在的）测试场景，尤其是在操作中可能出现的方案列表，并确保应用编码与预期相吻合。同时，应用编码操作对其余方案是否安全尚不可知。下图说明了其应用范围的不同之处。

通过引入Prover iLock验证器，您不必再将检验限定在几个方案上。 Prover iLock验证器证实，应用编码对于所有方案均安全。 虽然一些人对此还很陌生，但形式验证可广泛用于铁路、半导体、航空电子工学以及汽车工业。经过二十多年的发展，它已经成为一个成熟的，且经过检验的验证方法。

验证登陆

Prover iLock验证器是市场上出售的、唯一支持验证登陆的解决方案。在安全分析过程中，该工具会生成数十亿字节的验证日志。为了达到检验的目的，该日志可用独立的验证登陆检查器进行检查。 如果验证日志中（在意料之中）没有发现任何错误，独立的验证登陆检查器将提供安全验证。该方法符合用于减少安全测试的CENELEC SIL-4要求，并且通过认证登陆检查器，该方法成本低，可独立验证。

Unparalleled Capacity & Performance

对于支持验证执行模式的合作伙伴硬件而言，控制数百个列车路线的应用在数个CPU小时内便可全部得到验证。 Pover科技公司多年来投入250多名员工从事SAT和基于BDD模式检验、抽象、模型和补充领域的研发。 Prover iLock验证器将这些方法同其他用于多种优缺点的方法相结合，确保其性能和容量无可匹敌。