Project Description

巴黎地铁,法国

符合 CENELEC EN 50128 的自动签核安全验证

在这个项目中,Prover Technology 与巴黎地铁合作创建了一个形式化验证解决方案,以满足巴黎地铁对联锁软件安全验证的需求。巴黎地铁为多条地铁线路选择了泰雷兹的计算机联锁,并希望在符合 CENELEC EN 50128标准的过程中使用形式化证明,从而确保联锁软件的安全性。我们提供的解决方案包括:

  • 基于非碰撞和非脱轨特性的通用、形式化安全要求
  • 将安全验证计入考虑范围的列车行为环境模型,
  • 基于Prover 认证器的签核安全验证工具,它提供了独立的形式化证明,确保联锁软件(包括其编译的二进制映像)符合安全要求。

该解决方案于 2009 年首次与泰雷兹PMI line 3bis 项目中的传统测试工作同时进行评估。 自此该解决方案进入生产使用,例如用于以下的联锁系统: 12号线南(2010年)、8号线(2011年)、12号线北(2012年)和1号线(2013年)。

logo ratp
logo thales