上海控安SmartRocket系列产品推介（三）：SmartRocket iVerifier计算机联锁系统验证工具

行业背景

在现代公共交通体系中，轨道交通系统具有不可替代的突出地位。随着车站信号设备数量越来越庞大、车站作业任务越来越复杂，如何保证列车安全、快速、高效的运行，是摆在相关技术人员面前的一个突出问题。计算机联锁系统是铁路及城市轨道交通信号系统中极重要的子系统，是一种典型的基于数据驱动的安全苛求系统，开发过程中需要对系统行为进行验证并确认数据的安全性，数据不仅关系着计算机联锁功能的正确实现，更关系到整个信号系统的安全完整性等级。传统的联锁系统开发、设计和测试，只能从功能上保证其逻辑的正确性，而无法保证其安全需求完全得到满足。通过形式化方法保障安全需求完全满足，才是提高联锁系统安全性的关键。SmartRocket iVerifier作为上海控安拥有自主专利技术的计算机联锁系统形式化验证工具，打破了国外产品在计算机联锁系统形式化验证领域的垄断地位，成为国内轨道交通领域保证联锁系统安全性的首款形式化验证工具。

产品概述

SmartRocket iVerifier是一款应用于轨道交通领域的计算机联锁系统验证工具。该工具支持自动解析由LSpec规范语言描述的安全需求，并结合联锁数据自动验证需求是否成立。工具采用形式化方法进行验证，使得每条安全需求的真伪结论基于严格的模型检查，若证明为假，工具提供时序仿真调试功能以供用户推导出安全需求被违背的完整过程。形式化验证由工具根据通用应用和特定站型配置自动运行，执行效率高、方便调试、省去大量人力成本。

产品功能

01 自动化验证

支持勾选实例化设备进行一键验证。验证方法为simpleCAR，其中验证策略包括前向搜索和后向搜索，验证结果包括验证通过、验证未通过和验证未确定。对于验证通过的设备，其在任何情况下验证均通过；对于验证未通过的设备，工具提供不满足验证性质的反例，对于验证未确定的设备，可切换不同的策略或加长时限再次对其进行验证。

02 辅助反例调试

支持查看验证未通过设备下的全部变量周期图，点击某一周期，将对BOOL逻辑梯形图上变量进行赋值变化，站场图亦会展示该周期下设备的状态，支持同时查看梯形图和站场图，支持对站场图中设备进行搜索定位。

03 安全需求管理

支持在线导入安全需求文件或对安全需求进行增删查改，支持根据需求编号查找对应的形式化语言LSpec描述和自然语言描述，支持一键解析安全需求，通过解析查找其语法错误，并定位该错误。

特色优势

01 形式化验证

全过程采用自动化的模型检查方法，该方法通过冲突引导方式快速定位到违背安全需求的状态空间，同时通过抽象规约技术从部分搜索状态中推导出全状态空间的正确性，提高证明效率。

02 LSpec规范语言

设计了基于线性时间逻辑（Linear temporal logic, LTL）的LSpec规范语言。该语言将谓词逻辑中的量词与时间逻辑中的时延相结合，可以表示关系性质和时序性质，从而无二义地描述联锁系统的安全需求。

03 可视化调试

支持对站场平面图进行仿真，支持将违背安全需求的状态空间以周期图形式呈现，支持梯形图与站场图进行交互，为测试人员提供用户友好的反例调试工具。

04 增量式验证

提供LSpec规范语言在线编辑器，支持在开发周期中根据验证结果对形式化安全需求进行修改，支持对部分已修改需求重新进行验证，降低时间成本。

成果应用

轨道交通

SmartRocket iVerifier为行业龙头客户提供联锁系统形式化验证服务，以建立符合CENELEC EN 50128:2011 SIL4等级的签核安全验证。目前已解析超过1000条形式化需求，验证超过10000个实例，利用该工具已实现对试点站的联锁系统形式化验证。