参考项目

我们已经在全世界范围内交付了针对铁路应用的信号系统设计自动化解决方案。

我们在全球各地部署我们的解决方案

Prover已经成功为全球干线铁路和城市轨道交通运营商提供了信号系统设计自动化解决方案,包括巴黎地铁、纽约地铁和斯德哥尔摩地铁等地铁运营商,加拿大客运铁路、瑞典国家铁路和中国的干线铁路,以及纽约和斯德哥尔摩的轻轨和通勤铁路等。这里有Prover信号系统设计自动化解决方案的应用案例。

这些项目包含了各种类型,包括基于Prover Trident完整工具链的形式化验证,符合CENELEC SIL-4级别的签署验证,仿真和测试用例生成等。 Prover可全方位地为信号系统设计自动化提供技术服务。

以下是对我们已交付的部分项目的介绍。这些参考项目介绍了项目的目的、目标环境和我们提供的解决方案。

斯德哥尔摩地铁的Prover Trident应用

在这个项目中,Prover公司向Ansaldo STS提供了Prover Trident解决方案,为干线铁路公司Roslagsbanant进行了联锁软件的开发和安全验证。

纽约地铁的SSI软件的形式化验证

纽约地铁NYCT需要对信号系统进行升级改造,安装部署CBTC信号系统,并用SSI联锁系统来代替旧的继电器联锁,我们对新联锁系统软件进行了形式化验证。。

巴黎地铁RATP的形式化验证解决方案

Prover公司与RATP巴黎地铁合作进行了形式化验证解决方案的开发,实现了对联锁软件安全需求的形式化验证。

加拿大太平洋货运铁路应用Prover iLock

加拿大太平洋货运铁路Canadian Pacific (CP)需要在联锁软件设计和测试中提升运力并实现设计一致性,在2010年我们为他们提供了自动化工具Prover iLock满足了他们的需求。

斯德哥尔摩中央站的形式化验证

斯德哥尔摩中央站和邻接联锁系统是继电器联锁系统,我们提供了Prover Extractor来提取电气原理图中的形式模型m,并使用Prover iLock进行了安全性的形式化验证。

瑞典ERTMS2级形式化规范

Ansaldo STS在项目ESTER中需要向瑞典交通部Trafikverket交付ERTMS2级轨旁系统,其中包括计算机联锁子系统。瑞典交通部要求使用形式化验证来证明联锁软件的安全性,我们对安全需求进行了形式化描述并使用Prover Cetifier进行了安全性形式化验证,验证结果作为安全证明文件的一部分。

挪威国铁公司Bane NOR的形式化验证

在挪威铁路Nordlandsbanen项目中,Prover使用Prover iLock对ABB提供的计算机联锁软件进行了安全性形式化验证。

比利时Infrabel平交道口控制软件的形式化验证

Infrabel 公司要对约800个平交道口控制系统进行升级,使用计算机控制器代替基于继电器的旧控制系统,Prover使用形式化语言PiSPEC进行了逻辑设计和安全需求表达,并使用Prover iLock 配置并形式化验证了安全需求。

中国青藏线联锁软件的仿真与形式化验证

GE为中国国铁青藏线铁路提供超过20部联锁系统,我们应用Prover iLock实现了测试规范和安全需求,对VHLC硬件平台上的联锁软件进行了仿真测试和安全性形式化验证。

斯德哥尔摩轻轨联锁软件

GE交通部门(现Alstom)使用我们的Prover iLock工具进行了联锁软件的设计开发,在满足EN50128标准的前提下,进行了信号规则形式化和安全性验证,大大缩短了交付时间。

英国西门子Modular系统联锁软件的生成和验证

在Network Rail的Modular信号系统项目中,我们为英国西门子提供了基于Westrace Mk II的联锁软件代码生成和自动化测试,并进行了安全性形式化验证,显著降低了系统开发成本。