联锁验证工具

SmartRocket iVerifier

产品概述

SmartRocket iVerifier是国内首款iLOCK型计算机联锁系统验证工具,可以自动对所有安全要求进行正式验证,并且在验证不通过的情况下会给出反例,同时反例会呈现到对应的模型图和周期图上供用户推导出性质被违背的完整过程。除了核心的验证功能,SmartRocket iVerifier还具备需求管理、模型管理和用户管理功能,SmartRocket iVerifier为一个完整的产品。

特色功能

  • 需求管理

    支持对要验证的性质进行增删查改

  • 模型管理

    系统设计中的变量能自动生成模型

  • 自动验证

    输入需求与系统设计后一键式验证

  • 反例追溯

    验证失败提供反例周期图并可追溯

价值优势

  • 功能自动

    用户只需要点击上传按钮输入所要验证的安全需求文档和待验证的系统设计文档,再点击验证按钮即可根据安全需求一键式自动验证系统设计,最后的验证结果自动分类为验证通过,验证未通过和通过推导成功通过的安全需求三种情况。

  • 全面覆盖

    该工具的核心功能——验证功能是采用的形式化验证方法,形式化验证方法使用数学证明来确保系统满足要求,每条属性的真伪结论基于严格的数学证明,证明为真的属性任何情况下进行仿真都不会出错,即覆盖率可以达到100%。

  • 提供反例

    点击选择安全需求验证未通过的每个轨道交通设备,工具不仅会提供该设备的具体每个周期的验证结果(截止到最后出现反例的周期),还会提供该设备的逻辑关系模型图供用户点击该设备的关联设备以进行追溯。

  • 高性能

    基于模型检验的形式化验证方法内核,该工具即使针对大型的联锁系统也只需要花费少量时间即可进行完整的安全验证,快速验证即可快速发现系统设计错误并进行改正,实现良性循环,大大缩短了系统设计的周期。

  • 大容量

    该工具的内核验证功能采用的是基于模型检验的形式化验证方法,模型检验技术已在航空电子,电子设计自动化等行业中得到使用的证明,即可以对超大型系统进行验证,同样我们的工具可以对超大型联锁系统进行验证。

典型应用

轨道交通
  • 轨道交通