行業背景

在現代公共交通體系中，軌道交通系統具有不可替代的突出地位。隨著車站信號設備數量越來越龐大、車站作業任務越來越復雜，如何保證列車安全、快速、高效的運行，是擺在相關技術人員面前的一個突出問題。計算機聯鎖系統是鐵路及城市軌道交通信號系統中極重要的子系統，是一種典型的基于數據驅動的安全苛求系統，開發過程中需要對系統行為進行驗證并確認數據的安全性，數據不僅關系著計算機聯鎖功能的正確實現，更關系到整個信號系統的安全完整性等級。傳統的聯鎖系統開發、設計和測試，只能從功能上保證其邏輯的正確性，而無法保證其安全需求完全得到滿足。通過形式化方法保障安全需求完全滿足，才是提高聯鎖系統安全性的關鍵。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個實例，利用該工具已實現對試點站的聯鎖系統形式化驗證。