行業(yè)背景

在現(xiàn)代公共交通體系中，軌道交通系統(tǒng)具有不可替代的突出地位。隨著車(chē)站信號(hào)設(shè)備數(shù)量越來(lái)越龐大、車(chē)站作業(yè)任務(wù)越來(lái)越復(fù)雜，如何保證列車(chē)安全、快速、高效的運(yùn)行，是擺在相關(guān)技術(shù)人員面前的一個(gè)突出問(wèn)題。計(jì)算機(jī)聯(lián)鎖系統(tǒng)是鐵路及城市軌道交通信號(hào)系統(tǒng)中極重要的子系統(tǒng)，是一種典型的基于數(shù)據(jù)驅(qū)動(dòng)的安全苛求系統(tǒng)，開(kāi)發(fā)過(guò)程中需要對(duì)系統(tǒng)行為進(jìn)行驗(yàn)證并確認(rèn)數(shù)據(jù)的安全性，數(shù)據(jù)不僅關(guān)系著計(jì)算機(jī)聯(lián)鎖功能的正確實(shí)現(xiàn)，更關(guān)系到整個(gè)信號(hào)系統(tǒng)的安全完整性等級(jí)。傳統(tǒng)的聯(lián)鎖系統(tǒng)開(kāi)發(fā)、設(shè)計(jì)和測(cè)試，只能從功能上保證其邏輯的正確性，而無(wú)法保證其安全需求完全得到滿(mǎn)足。通過(guò)形式化方法保障安全需求完全滿(mǎn)足，才是提高聯(lián)鎖系統(tǒng)安全性的關(guān)鍵。SmartRocket iVerifier作為上海控安擁有自主專(zhuān)利技術(shù)的計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化驗(yàn)證工具，打破了國(guó)外產(chǎn)品在計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化驗(yàn)證領(lǐng)域的壟斷地位，成為國(guó)內(nèi)軌道交通領(lǐng)域保證聯(lián)鎖系統(tǒng)安全性的首款形式化驗(yàn)證工具。

產(chǎn)品概述

SmartRocket iVerifier是一款應(yīng)用于軌道交通領(lǐng)域的計(jì)算機(jī)聯(lián)鎖系統(tǒng)驗(yàn)證工具。該工具支持自動(dòng)解析由LSpec規(guī)范語(yǔ)言描述的安全需求，并結(jié)合聯(lián)鎖數(shù)據(jù)自動(dòng)驗(yàn)證需求是否成立。工具采用形式化方法進(jìn)行驗(yàn)證，使得每條安全需求的真?zhèn)谓Y(jié)論基于嚴(yán)格的模型檢查，若證明為假，工具提供時(shí)序仿真調(diào)試功能以供用戶(hù)推導(dǎo)出安全需求被違背的完整過(guò)程。形式化驗(yàn)證由工具根據(jù)通用應(yīng)用和特定站型配置自動(dòng)運(yùn)行，執(zhí)行效率高、方便調(diào)試、省去大量人力成本。

產(chǎn)品功能

01自動(dòng)化驗(yàn)證

支持勾選實(shí)例化設(shè)備進(jìn)行一鍵驗(yàn)證。驗(yàn)證方法為simpleCAR，其中驗(yàn)證策略包括前向搜索和后向搜索，驗(yàn)證結(jié)果包括驗(yàn)證通過(guò)、驗(yàn)證未通過(guò)和驗(yàn)證未確定。對(duì)于驗(yàn)證通過(guò)的設(shè)備，其在任何情況下驗(yàn)證均通過(guò)；對(duì)于驗(yàn)證未通過(guò)的設(shè)備，工具提供不滿(mǎn)足驗(yàn)證性質(zhì)的反例，對(duì)于驗(yàn)證未確定的設(shè)備，可切換不同的策略或加長(zhǎng)時(shí)限再次對(duì)其進(jìn)行驗(yàn)證。

02輔助反例調(diào)試

支持查看驗(yàn)證未通過(guò)設(shè)備下的全部變量周期圖，點(diǎn)擊某一周期，將對(duì)BOOL邏輯梯形圖上變量進(jìn)行賦值變化，站場(chǎng)圖亦會(huì)展示該周期下設(shè)備的狀態(tài)，支持同時(shí)查看梯形圖和站場(chǎng)圖，支持對(duì)站場(chǎng)圖中設(shè)備進(jìn)行搜索定位。

03安全需求管理

支持在線(xiàn)導(dǎo)入安全需求文件或?qū)Π踩枨筮M(jìn)行增刪查改，支持根據(jù)需求編號(hào)查找對(duì)應(yīng)的形式化語(yǔ)言L(fǎng)Spec描述和自然語(yǔ)言描述，支持一鍵解析安全需求，通過(guò)解析查找其語(yǔ)法錯(cuò)誤，并定位該錯(cuò)誤。

特色優(yōu)勢(shì)

01形式化驗(yàn)證

全過(guò)程采用自動(dòng)化的模型檢查方法，該方法通過(guò)沖突引導(dǎo)方式快速定位到違背安全需求的狀態(tài)空間，同時(shí)通過(guò)抽象規(guī)約技術(shù)從部分搜索狀態(tài)中推導(dǎo)出全狀態(tài)空間的正確性，提高證明效率。

02LSpec規(guī)范語(yǔ)言

設(shè)計(jì)了基于線(xiàn)性時(shí)間邏輯（Linear temporal logic, LTL）的LSpec規(guī)范語(yǔ)言。該語(yǔ)言將謂詞邏輯中的量詞與時(shí)間邏輯中的時(shí)延相結(jié)合，可以表示關(guān)系性質(zhì)和時(shí)序性質(zhì)，從而無(wú)二義地描述聯(lián)鎖系統(tǒng)的安全需求。

03可視化調(diào)試
支持對(duì)站場(chǎng)平面圖進(jìn)行仿真，支持將違背安全需求的狀態(tài)空間以周期圖形式呈現(xiàn)，支持梯形圖與站場(chǎng)圖進(jìn)行交互，為測(cè)試人員提供用戶(hù)友好的反例調(diào)試工具。

04增量式驗(yàn)證
提供LSpec規(guī)范語(yǔ)言在線(xiàn)編輯器，支持在開(kāi)發(fā)周期中根據(jù)驗(yàn)證結(jié)果對(duì)形式化安全需求進(jìn)行修改，支持對(duì)部分已修改需求重新進(jìn)行驗(yàn)證，降低時(shí)間成本。

成果應(yīng)用

軌道交通
SmartRocket iVerifier為行業(yè)龍頭客戶(hù)提供聯(lián)鎖系統(tǒng)形式化驗(yàn)證服務(wù)，以建立符合CENELEC EN 50128:2011 SIL4等級(jí)的簽核安全驗(yàn)證。目前已解析超過(guò)1000條形式化需求，驗(yàn)證超過(guò)10000個(gè)實(shí)例，利用該工具已實(shí)現(xiàn)對(duì)試點(diǎn)站的聯(lián)鎖系統(tǒng)形式化驗(yàn)證。