行業(yè)背景

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

產(chǎn)品概述

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

產(chǎn)品功能

01自動化驗證

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

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

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

03安全需求管理

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

特色優(yōu)勢

01形式化驗證

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

02LSpec規(guī)范語言

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

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

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

成果應(yīng)用

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