Prover iLock®

开发铁路联锁系统应用软件的桌面工具

关于 Prover iLock®

Prover iLock 是一个桌面工具,用于为轨道联锁系统生成完整的被记录、测试和验证的应用软件,并可以在目标平台上进行编译和安装。 对于PiSPEC IP捕获的信号规则以及特定的联锁配置,也就是由PiSPEC IP在配置应用程序时形式化的场景和对象要求,Prover iLock会将其实例化。

接着Prover iLock就可以自动化:

  • 将实例化的需求转换为通车服务代码
  • 形式化验证代码符合安全要求
  • 使用模拟和测试功能
  • 记录该应用程序,并生成用于安装测试的测试说明

版本5的新功能

新的布局编辑器

体验更加灵活、有效和精确的轨道布局编辑器。在多年使用旧的编辑器的过程中,我们了解到什么是在绘制轨道布局和放置对象时,对效率和可靠性真正重要的因素。使用新的布局编辑器,您可以更轻松地添加、删除或移动轨道、信号和开关(点)。如果您愿意,可以从已有的数据库中导入布局,并在 Prover iLock 中对其进行可视化。您可以使用您选择的矢量图形程序编辑或添加符号,因为现在的信号都是标准的可缩放向量图形(SVG)。布局以LCF格式保存,可以轻松检查内容和版本之间的差异,以及满足CENELEC EN50128 SIL4要求所需的配置数据验证。

新包装管理器

只需在Windows中双击软件包捆绑文件,即可安装新的Prover iLock软件包。 新的软件包管理器将检查软件包的完整性,并向您显示已安装的软件包和需要安装的软件包。

PSL 4内核

Prover iLock 验证器中的模型检查器已升级为目前市场上最快捷的型号,即我们的PSL4。Prover iLock 验证器继续为形式化验证工作提供广受好评的图形用户界面,与此同时您还会体验到更快的速度,以及比以往更多的证明策略。

请填写右侧表格,立即查看ProveriLock®的演示视频。

Prover iLock® 由以下软件模块组成

Prover iLock 基础模块

控制正在开发的系统,并提供用于创建特定应用程序配置的内置布局编辑器。 它定义了系统的轨道布局、单个轨旁设备的配置设置、速度限制数据等。 这一配置也可以从文件中导入。

Prover iLock 验证器

只需按下一个按钮,即可对所有安全要求进行形式化验证。 形式化验证是指使用数学证明方法来确保系统满足所有的要求,从而在验证中提供100%的覆盖率。

Prover iLock仿真器

只需按下一个按钮,即可对所有测试案例进行功能测试。该仿真器具有强大的调试器,还支持交互式仿真,可以在轨道布局的图形显示中对模拟进行可视化和实现相应控制。

Prover iLock编码器

只需按下一个按钮,即可为系统生成软件代码。 编码模块支持诸多领先的联锁平台,同时可以使用编程语言C语言生成代码。

Prover iLock文档生成器

该程序可以为系统生成文档,包括控制表、测试和验证报告,以及工厂表格和通车测试表格。

以上这些模块可以一起使用,也可以单独使用,当然使用任何其他模块都需要基础模块。 在没有 Prover iLock 编码器参与的情况下使用此工具时,其他模块可用于代码导入流程中,用于分析Prover iLock 以外开发的代码。

Prover iLock编码器

Prover iLock 编码器可以为在Prover iLock中创建的系统设计生成软件代码,这免除了手动编写软件代码的需要,从信号工程师那里释放了资源,进而可以让他们更高效地完成相应的其他工作。

Prover iLock 编码器的优点:

  • 在不同应用程序中实现软件代码一致性
  • 高效代码(已采用代码优化)
  • 对所使用资源的有效验证
  • 与手动编写的代码相比,代码质量更高

Prover iLock 编码器支持关键系统和非关键系统的代码生成。它具有灵活的框架, 用于不同目标语言的代码生成器可以在其中组合。 生成过程将产生所有必要的配置文件和数据,包括与相邻系统和轨旁设备的接口,还可以用于编译所生成代码的脚本。生成的代码可以用于集中式联锁系统和分布式联锁系统。 对于分布式系统,Prover iLock 编码器将生成通讯链接的配置,包括其传输的通信变量。

Prover iLock 编码器支持多种专有语言和联锁平台,以及用于商业现货硬件的标准C语言代码生成器。 另外,该编码器可以根据需要添加对其他联锁目标和通信协议的支持。

Prover iLock 文档生成器

Prover iLock 文档生成器为特定应用程序生成文档。 文档生成功能是可配置的,从而可以轻松适应不同的文档需求。

特定应用的典型文档包括:

  • 轨旁设备清单
  • 路线表及其保护区域
  • 详细说明所用联锁条件的逻辑公式
  • 安装所需测试活动的规范
  • 适用于特定应用程序配置的清单

使用Prover iLock 文档生成器,您可以自动生成这些文件,它们是针对特定应用程序配置的。 在传统流程中,文档的制作需要大量的精力,而在Prover iLock流程中,它就像Prover iLock 文档生成器为您提供的那样快速简便。 手动编写详细的文档(例如测试计划)很繁琐,并且容易出错,使用Prover iLock 文档生成器可以确保您获得一致的高品质结果。

Prover iLock 文档生成器可根据您的个人需求进行高度定制。 您可以包括开发和验证确认流程中任何步骤的数据,并以不同的文件格式呈现,例如:

  • 文本文件 (.txt)
  • CSV文件(.csv)
  • Microsoft Office Excel(.xls 或 .xlsx)
  • Microsoft Office Word(.doc或.docx)

Prover iLock仿真器

Prover iLock 仿真器可以针对在Prover iLock中创建的系统设计,对从通用语言PiSPEC定义生成的大量测试用例进行高效仿真,同时它还支持对导入Prover iLock的外部代码的仿真。 这种模拟可以有效压缩所用时间,比在目标硬件平台上执行要快得多,这也使得在开发过程中确定系统功能正确性变得更加高效,从而减少开发时间,也让工程师可以更好地利用他们的时间。 所有测试用例和仿真结果都可以被导出和获取,使硬件在环测试可以重复所有桌面模拟结果。

仿真器支持分布式系统,以及关键代码和非关键代码。 同时它可以混合使用分布式系统中的执行模型,从而实现对拥有通信链接、远程办公控制系统、环境模型(模拟轨旁设备的行为)和多个平台的分布式联锁系统的高精确仿真。

Prover iLock 仿真器具有强大的内置调试器,它可以高效地查明测试案例失败的原因,并且实现系统行为的可视化。 仿真也可以是交互式的,即用户可以从 Prover iLock 的图形用户界面控制对系统的输入,同时直接观察系统的响应。

Prover iLock 仿真器的优点:

  • 高效准确地模拟多个联锁平台
  • 支持通过PiSPEC IP生成的测试案例的自动测试,并且也支持更传统的手动测试
  • 易于使用,内置调试器带有梯形逻辑查看器的和仿真状态的图形可视化
  • 多个联锁系统可以连接在一起并进行仿真

点击查看放大截图

Prover iLock 验证器

Prover iLock 验证器用于在 Prover iLock 中创建的系统设计,提供针对各项安全要求的有效形式化验证。另外该验证器还支持对导入Prover iLock的外部代码的验证。

形式化验证基于自动证明搜索,并针对禁止的、不安全的状态提供 100% 的验证覆盖率:如果被验证的系统达到任何违反安全要求的状态,Prover iLock 验证器会检测并报告这一违规状态,并包括导致这一状态的事件顺序。

内置的调试器为确定为什么系统允许进入被禁止的不安全状态,提供了有效的支持。越来越多的基础架构管理人员主张,甚至强制要求进行形式化验证,他们强烈建议使用基于特定标准的形式化验证进行安全验证,这些标准就包括CENELEC EN 50128。Prover iLock 验证器提供自动化的和易于使用的形式化验证,它具备了无与伦比的速度和容量,可以确保您的联锁系统获得可预测的形式化验证结果。

经历考验的形式化验证技术,拥有无与伦比的容量和性能

Prover iLock 验证器基于市场领先的模型检查器 PSL 4,用于关键嵌入系统的安全验证。 PSL 已在航空电子、电子设计自动化、汽车和轨道信号等行业中得到验证。

Prover iLock 验证器可以提供所需的速度和容量,以便在短短几个小时的中央处理器计算时间内,对当今世界上一部分最大的联锁系统进行完整的形式化验证。Prover 已经投入了超过250年研发包括基于 SAT 的模型检查、抽象和插值在内的形式化验证技术。 Prover iLock 验证器结合了这些验证方法,以提供无与伦比的性能和容量。

点击查看放大截图