SmartRocket iVerifier
SmartRocket iVerifier是一款应用于轨道交通领域的计算机联锁系统验证工具。该工具支持自动解析描述安全需求的LSpec规范语言，支持结合联锁数据自动验证安全需求。工具采用形式化方法进行验证，使得每条安全需求的真伪结论基于严格的数学证明，若证明为假，工具提供仿真调试功能以供用户推导出安全需求被违背的完整过程。同时形式化验证由工具根据通用应用和特定站型自动生成相应数据并自动执行，执行效率高，省去大量人力成本。
自定义规范语言，该语言将谓词逻辑中的量词和线性时序逻辑相结合，使得语言既可以表示关系性质、又可以表示时序性质，从而清楚、无二义性地描述安全需求。
全过程采用自动化的模型检查方法，通过冲突引导方式快速定位到违背安全需求的状态空间，同时通过抽象规约技术从部分搜索状态中推导出全状态空间的正确性，提高证明效率。
支持对站场平面图进行仿真，支持将违背安全需求的状态空间以周期图形式呈现，支持梯形图与站场图进行交互，供测试人员对反例进行调试。
提供LSpec规范语言在线编辑器，支持根据验证结果对形式化语言进行查看与修改，支持对语言进行语法检查，并提示与定位错误。
管理员轻松管理多个用户使用权限
用户只需要点击上传按钮输入所要验证的安全需求文档和待验证的系统设计文档，再点击验证按钮即可根据安全需求一键式自动验证系统设计，最后的验证结果自动分类为验证通过，验证未通过和通过推导成功通过的安全需求三种情况。
该工具的核心功能——验证功能是采用的形式化验证方法，形式化验证方法使用数学证明来确保系统满足要求，每条属性的真伪结论基于严格的数学证明，证明为真的属性任何情况下进行仿真都不会出错，即覆盖率可以达到100%。
点击选择安全需求验证未通过的每个轨道交通设备，工具不仅会提供该设备的具体每个周期的验证结果（截止到最后出现反例的周期），还会提供该设备的逻辑关系模型图供用户点击该设备的关联设备以进行追溯。
基于模型检验的形式化验证方法内核，该工具即使针对大型的联锁系统也只需要花费少量时间即可进行完整的安全验证，快速验证即可快速发现系统设计错误并进行改正，实现良性循环，大大缩短了系统设计的周期。
该工具的内核验证功能采用的是基于模型检验的形式化验证方法，模型检验技术已在航空电子，电子设计自动化等行业中得到使用的证明，即可以对超大型系统进行验证，同样我们的工具可以对超大型联锁系统进行验证。
