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 验证器结合了这些验证方法，以提供无与伦比的性能和容量。
点击查看放大截图
