上海控安iVerifier计算机联锁系统验证工具概述-德赢Vwin官网网

行业背景

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

产品概述

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

产品功能

01自动化验证

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

02辅助反例调试

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

03安全需求管理

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

特色优势

01形式化验证

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

02LSpec规范语言

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

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

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

成果应用

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

声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表德赢Vwin官网网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。举报投诉

验证工具

验证工具

+关注

关注
0

文章
10

浏览量
7484
轨道交通

轨道交通

+关注

关注
1

文章
157

浏览量
15228

计算机接口位于什么之间

计算机接口是计算机硬件和软件之间、计算机与外部设备之间以及计算机各部件之间传输数据、控制信息和状态信息的硬件设备和软件程序。它在计算机系统中

发表于 10-14 14:02 •341次阅读

信号继电器在计算机系统中的应用

信号继电器在计算机系统中的应用是一个重要且复杂的领域，它作为电气控制的关键元件，在计算机系统中发挥着信号转换、隔离、放大以及控制等多种作用。以下将从信号继电器的基本概念、工作原理、特性、在计算机系统中的应用场景、优势以及未来发展

发表于 09-27 16:29 •353次阅读

计算机存储系统的工作原理和功能

计算机存储系统作为计算机系统中至关重要的组成部分，其原理和功能对于理解计算机的运行机制具有关键意义。以下将详细阐述计算机存储

发表于 09-26 16:42 •851次阅读

计算机存储系统的构成

计算机存储系统是计算机中用于存放程序和数据的设备或部件的集合，它构成了计算机信息处理的基础。一个完整的计算机存储

发表于 09-26 15:25 •782次阅读

计算机系统的硬件组成和主要部件

计算机系统的硬件组成是计算机运行的基础，它包含了多个关键部件，这些部件相互协作，共同实现计算机的各种功能。

发表于 09-10 11:41 •2156次阅读

简述计算机总线的分类

计算机总线作为计算机系统中连接各个功能部件的公共通信干线，其结构和分类对于理解计算机硬件系统的工作原理至关重要。以下是对计算机总线结构和分类

发表于 08-26 16:23 •1424次阅读

微处理器如何控制计算机系统

微处理器，作为计算机系统的核心部件，承担着控制整个计算机系统运行的重要任务。它不仅是计算机的运算中心，还是控制中心，负责执行程序指令、处理数据以及协调计算机各部件之间的工作。以下将详细

发表于 08-22 14:21 •476次阅读

计算机系统的组成和功能

计算机系统是一个复杂而庞大的概念，它涵盖了计算机硬件、软件以及它们之间相互作用的所有元素。为了全面而深入地探讨计算机系统，本文将从定义、组成、功能、发展历程以及未来趋势等方面进行详细阐述。

发表于 07-24 17:41 •913次阅读

计算机系统中的关键组件有哪些

在计算机系统中，关键组件的协同工作构成了其强大的数据处理和运算能力。这些组件不仅决定了计算机的性能，还影响着用户的使用体验。以下是对计算机系统中关键组件的详细阐述，包括它们的定义、功能、特点以及相互之间的关系。

发表于 07-15 18:18 •1510次阅读

工业控制计算机的硬件组成有哪些

工业控制计算机（Industrial Personal Computer，IPC）是一种专门为工业环境设计的计算机系统，具有高可靠性、高稳定性、高实时性等特点。在工业自动化、智能制造等领域中，工业

发表于 06-16 11:33 •1639次阅读

工业计算机与普通计算机的区别

在信息化和自动化日益发展的今天，计算机已经成为了我们日常生活和工作中不可或缺的工具。然而，在计算机领域中，工业计算机和普通计算机虽然都具备基

发表于 06-06 16:45 •1361次阅读

【量子计算机重构未来 | 阅读体验】+ 初识量子计算机

欣喜收到《量子计算机——重构未来》一书，感谢德赢Vwin官网论坛提供了一个让我了解量子计算机的机会！自己对电子计算机有点了解，但对量子计算机真是一无所知，只是听说过量子纠缠、超快的运算速

发表于 03-05 17:37

计算机系统由什么两部分组成计算机系统的层次结构

计算机系统是由硬件和软件两部分组成的。硬件部分包括计算机的实体组件，如中央处理器（CPU）、内存、存储设备、输入输出设备、显示器等。CPU是计算机系统的核心部件，负责执行指令、运算和控制计算

发表于 02-01 14:13 •3618次阅读

计算机系统如何应对大模型时代的挑战与机遇

“操作系统管理着计算机的资源和进程，以及所有的硬件和软件。计算机的操作系统让用户在不需要了解计算机语言的情况下与

发表于 01-23 11:06 •542次阅读

工业计算机与商用计算机的区别

工业计算机与商用计算机的区别工业计算机和商用计算机是两种应用于不同领域的计算机系统。虽然它们在技术方面存在一些共性，但在功能、设计、可靠

发表于 12-27 10:50 •617次阅读

搜索历史

上海控安iVerifier计算机联锁系统验证工具概述

评论