行業(yè)背景

在現(xiàn)代公共交通體系中，軌道交通系統(tǒng)具有不可替代的突出地位。隨著車站信號設(shè)備數(shù)量越來越龐大、車站作業(yè)任務(wù)越來越復(fù)雜，如何保證列車安全、快速、高效的運(yùn)行，是擺在相關(guān)技術(shù)人員面前的一個(gè)突出問題。計(jì)算機(jī)聯(lián)鎖系統(tǒng)是鐵路及城市軌道交通信號系統(tǒng)中極重要的子系統(tǒng)，是一種典型的基于數(shù)據(jù)驅(qū)動(dòng)的安全苛求系統(tǒng)，開發(fā)過程中需要對系統(tǒng)行為進(jìn)行驗(yàn)證并確認(rèn)數(shù)據(jù)的安全性，數(shù)據(jù)不僅關(guān)系著計(jì)算機(jī)聯(lián)鎖功能的正確實(shí)現(xiàn)，更關(guān)系到整個(gè)信號系統(tǒng)的安全完整性等級。傳統(tǒng)的聯(lián)鎖系統(tǒng)開發(fā)、設(shè)計(jì)和測試，只能從功能上保證其邏輯的正確性，而無法保證其安全需求完全得到滿足。通過形式化方法保障安全需求完全滿足，才是提高聯(lián)鎖系統(tǒng)安全性的關(guān)鍵。SmartRocket iVerifier作為上海控安擁有自主專利技術(shù)的計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化驗(yàn)證工具，打破了國外產(chǎn)品在計(jì)算機(jī)聯(lián)鎖系統(tǒng)形式化驗(yàn)證領(lǐng)域的壟斷地位，成為國內(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ī)范語言描述的安全需求，并結(jié)合聯(lián)鎖數(shù)據(jù)自動(dòng)驗(yàn)證需求是否成立。工具采用形式化方法進(jìn)行驗(yàn)證，使得每條安全需求的真?zhèn)谓Y(jié)論基于嚴(yán)格的模型檢查，若證明為假，工具提供時(shí)序仿真調(diào)試功能以供用戶推導(dǎo)出安全需求被違背的完整過程。形式化驗(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)證通過、驗(yàn)證未通過和驗(yàn)證未確定。對于驗(yàn)證通過的設(shè)備，其在任何情況下驗(yàn)證均通過；對于驗(yàn)證未通過的設(shè)備，工具提供不滿足驗(yàn)證性質(zhì)的反例，對于驗(yàn)證未確定的設(shè)備，可切換不同的策略或加長時(shí)限再次對其進(jìn)行驗(yàn)證。

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

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

03安全需求管理

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

特色優(yōu)勢

01形式化驗(yàn)證

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

02LSpec規(guī)范語言

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

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

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

成果應(yīng)用

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