Project Description

Infrabel,比利时

形式化验证安全和设计规范

在这个项目中,Prover 提供了工具和服务来帮助因弗拉贝尔提高平交道口系统招标要求规范的质量。因弗拉贝尔计划用计算机控制器取代大约 800 个基于继电器的平交道口。由于这些系统的安全苛求属性和需求规范的复杂性,因弗拉贝尔决定执行需求验证以检测和消除规范中的错误和歧义。这样做的目的是向供应商提供更高品质的规范,从而降低计算机化轨道控制交付延迟的风险。因弗拉贝尔选择 Prover对需求规范进行形式化验证,其技术解决方案包括:

  • 以 PiSPEC 语言形式化安全要求
  • 以 PiSPEC 语言形式化设计要求
  • Prover iLock 工具链,用于配置平交道口应用程序和应用程序的安全验证

总共指定了 54 个平交道口配置系列(27 个有障碍物,27 个没有障碍物),并接受了大约 119 项有安全要求的形式化验证。这有助于发现平交道口需求规范中的意外行为,并在招标开始之前对需求规范进行更正和更新。

logo infrabel