形式化方法應用于計算機聯鎖軟件的安全驗證研究

羅 娟，王燕芩

（卡斯柯信號有限公司，上海 200071）

形式化方法應用于計算機聯鎖軟件的安全驗證研究

羅 娟，王燕芩

（卡斯柯信號有限公司，上海 200071）

鐵路信號系統中的聯鎖系統對安全性要求極高，僅通過普通的功能測試無法保障其安全性。采用形式化驗證的方式可以驗證聯鎖系統的應用邏輯與安全需求的一致性。將通用安全需求結合具體的站場圖進行實例化，得到具體的安全需求后輸入帶歸納功能的布爾可滿足問題（SAT）約束求解器進行驗證，通過覆蓋所有的實例、所有周期以及每個周期所有的狀態空間，保證了驗證方法的完備性。

計算機聯鎖；安全需求；通用應用；形式化驗證

聯鎖系統是涉及到生命財產安全的高安全性系統，其安全性除了體現在冗余結構的系統硬件上，還應考慮系統軟件的安全性。軟件的安全性需通過系統邏輯設計與安全需求的一致性和特殊的安全防護措施保證。在安全需求實現時，若存在系統需求描述不準確，則會造成需求設計實現不準確，這一系列因為人為失誤可能導致最終的系統功能失效，威脅行車安全。為了確保系統需求的正確實現，本文提出形式化方法對既有聯鎖系統應用進行安全驗證，確保系統實現與安全需求要求的一致性。聯鎖系統是鐵路信號系統中的安全相關的重要系統，根據EN50128的要求，聯鎖系統的安全性需達到SIL4的安全等級，因此對其進行安全驗證十分必要。

1 研究背景

對于安全相關的系統，在正常功能性需求外，含大量安全需求。其中，功能需求描述了系統正常的功能總會在未來某個正確的時刻發生，而安全需求則描述了導致系統危險的情況不會發生[1]。傳統的開發、設計和測試的方法不能保證系統所有安全需求均被正確實現。目前，系統的功能需求主要通過測試的方法進行驗證，而安全需求則主要通過危險分析（HA，Hazard Analysis）及創建危害日志的方法，分析和記錄系統可能出現的危險。采用傳統的開發、測試和驗證主要存在以下幾個方面的缺點：

（1）使用自然語言描述需求，需求內容不夠明確，容易產生二義性，設計和測試階段均可能會出現因為對需求理解的偏差而造成設計錯誤或測試錯誤的情況；

（2）傳統的測試采用人工設計測試用例的方式，對于某一個功能的所有場景可能無法考慮全面，從而導致測試用例設計不完整；

（3）傳統的測試過程無法覆蓋系統在某個測試場景下所有的狀態空間，導致系統運行過程中發生的危害并不能通過測試發現；

（4）對于安全需求的驗證目前主要是通過追蹤需求、設計、實現中的對應關系進行，大多僅停留在文檔的層面，無法保證軟件的實現完全滿足安全需求。而且多采用人工分析的方式，效率較低，需要投入較多的人力資源。

2 形式化方法簡介

2.1 形式化方法

形式化方法[2]是建立在嚴格數學基礎上、具有精確數學語義的開發方法，能夠除去用自然語言描述而造成的需求、屬性方面的模糊定義。該方法需要對被驗證對象進行形式化建模，也就是將一般的需求定義抽象成數學模型，將待測系統抽象成可被證明的數學模型。

形式化方法可分為形式化規范描述和形式化驗證兩大類：（1）形式化規范描述使用具有嚴格數學定義的語法和語義的規范語言來描述系統。被描述的系統特性包括行為特性、時間特性、性能特性和內部結構等。采用形式化語言將非形式化的（Informal）需求進行形式化（Formal）描述，從系統設計的開始階段就努力降低系統的故障率，可以節省大量后期調試、修改成本。（2）形式化驗證是通過數學證明的方式，自動化的驗證系統在一定的前提條件下滿足各種靜態和動態性質。

2.2 形式化驗證主要技術

形式化驗證的主要技術包括模型檢驗和定理證明：（1）模型檢驗是一種基于有限狀態模型并檢驗該模型的期望特性的技術。它對模型的狀態空間進行遍歷搜索，以確認該系統模型是否具有某些性質。（2）定理證明則是選定一個數學邏輯體系，用體系中的公式描述系統和系統性質。依據該體系中的公理和定理，推導系統性質的描述公式。

定理證明因其在驗證過程中需要人工交互而導致自動化程度不高，相比于定理證明，以模型檢驗的方法則可以對系統變量進行全狀態空間的檢驗和證明，在提升系統狀態覆蓋完備性同時，提高了驗證的自動化程度。

法國巴黎地鐵14號線的自動駕駛系統就是用形式化方法開發并驗證的，1998年投入運行，至今未發現任何缺陷。法國戴高樂機場用于接送乘客無人駕駛線路也應用形式化方法對系統安全性進行了驗證。

3 聯鎖系統軟件的形式化驗證

隨著鐵路信號控制系統的復雜性在不斷地增加，世界各大業主和信號廠商也越來越重視形式化方法的應用：（1）形式化驗證方法從系統的安全需求出發，通過模型檢驗，證明系統的安全需求已經實現且系統功能滿足安全需求的要求，驗證系統安全性確實滿足既定要求；（2）通過驗證，檢驗系統在安全實現上的缺陷，做到查漏補缺，能夠早發現，早解決，為系統的安全提供安全保障；（3）形式化驗證在系統的全狀態空間的搜索過程中，能夠完整檢驗系統在任意狀態可能潛在的風險問題，增強產品信心。

將安全需求的形式化驗證方法應用于聯鎖系統，需要考慮在實際控制應用過程中的特殊性。聯鎖系統軟件內部邏輯主要是布爾邏輯，從狀態空間的角度出發，對其進行模型檢驗更為可行。對于聯鎖系統而言，危及行車安全的風險主要有列車或車列迎面沖撞、側面沖撞、追尾沖撞、錯道、擠岔和掉道等。對于一個完善的聯鎖系統，除了要通過測試說明各項功能需求被正確無誤的實現，還必須要驗證導致上述各種危險的事件不可能發生。采用歸納驗證和模型檢驗相結合的形式化驗證方法用于確保系統的輸出確實無法導致危險事件發生。其中，通過模型檢驗可以覆蓋每一個周期的所有狀態空間，而通過歸納驗證，則可以覆蓋所有的周期。

3.1 驗證流程

本文所描述的是通過開發通用的形式化安全需求，結合具體站型對實例化后的既有聯鎖應用進行形式化驗證的過程。其中，所涉及到的聯鎖系統邏輯的通用應用和特定應用都是以布爾表達式進行描述。對聯鎖系統特定應用進行形式化驗證的過程如圖1所示，主要包括：（1）聯鎖系統安全需求通用建模及針對特定應用的配置，即圖中兩個虛線框內的部分。這兩部分完成后，就可以直接輸入到實例化工具中，將通用安全性質實例化為針對特定站場的特定安全性質；（2）將特定安全性質輸入到帶有歸納證明功能的模型檢驗的驗證器中進行形式化驗證，得到最終的結果，并通過對最終結果的分析確定系統是否滿足相關的安全性質。其中，針對安全需求通用建模，主要是建立聯鎖信號設備的邏輯模型，用以描述聯鎖功能上的邏輯關系，同時，設計形式化安全需求與應用的接口，以實現后續安全需求實例化。

圖1 聯鎖軟件形式化驗證流程

3.2 安全需求形式化描述

為了能夠實現安全需求的形式化驗證，要求驗證輸入的需求必須以形式化方式進行描述。用于安全需求形式化描述的語言很多，本文提出了一種基于面向對象技術和一階謂詞邏輯[3]的形式化語言。

面向對象的技術可以很好地對驗證系統的各功能模塊及控制對象進行建模，而一階謂詞邏輯能夠清楚地描述各個控制對象之間的聯鎖關系，且能夠通過實例化和變換轉變為析取范式，便于驗證器進行驗證。該語言由基本的邏輯操作符（如and,or,not,=＞）、量詞（如ALL,EXIT）組成，具有面向對象的繼承、方法重載等特性。基本的操作元素是對象，每個對象屬于一個類，類包括屬性、函數、等式等字段。例如，對于安全需求“進路開放，則進路上的區段空閑”而言，對該條安全需求采用形式化方式描述后即為：

"ALL rt(rt.route_clear =＞ ALL seg(rt.segment(seg) =＞seg.vacant))",(PO1)

其中，rt,seg分別為事先定義的控制對象的應用實例，route_clear,segment，vacant是控制對象需實現的功能函數。

3.3 安全需求實例化

本文所述的聯鎖系統形式化驗證的應用是對具體的聯鎖應用邏輯進行形式化驗證，而上述形式化安全需求是從通用角度進行描述的，因此，為了能夠進行最終的驗證工作，還需要對安全需求進行實例化。從通用的安全需求轉換為針對具體某個站的安全需求的過程稱為安全需求實例化。安全需求實例化實際就是將每條形式化安全需求中的對象實例化為站場上對應的設備，而功能函數則通過函數描述的關系最終轉換為每個設備對應的參數。從數學層面來看，整個實例化的過程就是在類實例化和函數映射的基礎上移除全稱量詞和存在量詞的過程。由于這一過程完全可以通過面向對象技術結合相應的數學原理實現，因此這一過程可以由工具自動完成。

3.4 安全需求與通用應用接口

由于是對既有聯鎖應用進行形式化驗證，而聯鎖系統邏輯并非用上文提出的形式化語言進行設計和描述，因此，從形式化語言到聯鎖通用應用邏輯之間必須建立映射關系，以支持安全需求的實例化。

安全需求與通用應用接口主要包括以下工作：站場信號設備面向對象建模、站場平面圖信息讀取、信號設備模型與站場圖和通用應用的映射。

3.4.1 站場信號設備面向對象建模

結合聯鎖系統功能，在建模時，通用設備對象的分類采用面向對象的方式，因此，需要對信號設備分類，主要包括：進路、信號機、道岔、軌道區段，上述這些設備均可作為父類。如進路又包括列車進路、調車進路、非進路等。信號機根據不同的作用可分為：列車信號機、調車信號機和列車兼調車信號機。列車信號機主要是用來作為列車進路的始端或終端，調車信號機可以作為調車進路的始端和終端，而列車兼調車信號機，既可以作為列車進路的始終端，又可作為調車進路的始終端，但同一時間只能作為一種進路的始端或終端。上述給出的是基本的信號設備分類，考慮復雜的情況時還可以進一步擴展。對于每一個類，需要設計相應的參數、函數和等式。參數是可以直接從站場圖中獲得的信息，如信號設備之間的位置關系等；函數是信號設備的狀態或功能描述，如信號機的開放或關閉狀態；等式與函數很類似，但是與周期相關，即等式左邊計算得到的值都是下一周期的值，需要使用本周期的值進行計算。另外，由于進路是由信號機、道岔和軌道電路組成，因此，還需要設計進路和其他3種設備之間的關系。圖2所示為信號設備的面向對象的關系圖。

圖2 信號設備面向對象建模示意圖

3.4.2 站場平面圖信息讀取

站場平面圖信息的讀取是為了提取出信號設備的屬性以及各信號設備之間的拓撲關系，并將相關的信息傳給對象結構中的函數和參數。站場平面圖的描述一般采用結構化的文件進行，內部包括各種數據結構。本文描述的是以XML格式的站場圖的信息提取。XML中包含的信號設備相關的字段主要有：SIGNAL,TRACK,SWITCH,ROUTE等，當然還包括一些零散的按鈕和表示燈，在此就不進行介紹。表1以道岔為例，給出了其在站場描述文件中對應的各種字段。

表1 道岔屬性表

3.4.3 信號設備模型與站場圖和通用應用的映射

為了對信號設備以及安全需求進行實例化，需要建立信號設備模型到站場圖和通用應用之間的映射關系，這里的映射關系包括兩層：（1）信號設備模型到站場圖的映射，進行該映射可以將站場圖上的具體的信號設備與信號設備類聯系起來，得到信號設備實例以及每個實例對應的拓撲關系相關的參數值。以信號機為例，根據type確定信號機父類，根據subtype確定子類，這樣就可以產生一個信號機實例，再根據其他字段，可得到實例中相關參數的取值。（2）信號設備類中的函數、變量到通用應用邏輯中實際變量之間的映射，如對于軌道區段， TRACK類會有一個vacant的函數，用來表示區段的占用或空閑狀態，那么在通用應用邏輯中會有一個相同含義的變量，如：用布爾變量DGJ表示區段占用（DGJ=0）或空閑（DGJ=1）。表2列出了一些主要的函數映射關系。

表2 主要信號設備類函數與聯鎖應用邏輯變量映射表

4 形式化驗證實現

在聯鎖系統中，信號開放必須檢查其內方軌道區段處于空閑狀態[4]。由此出發，建立驗證該安全需求的通用應用，即：若進路始端信號開放，則進路內方所有區段應空閑。在描述安全需求的通用驗證模型外，必須結合特定的站型對通用模型進行實例化，以檢驗建立的通用模型滿足安全需求，達到對安全需求驗證的目的。

對上述安全需求進行形式化描述后得到：

"ALL rt(rt.route_clear=＞ ALL seg(rt.segment(seg) =＞seg.vacant))"，

其中，rt表示進路變量，seg表示區段，rt.segment(seg)表示區段seg是進路rt的內方區段，seg.vacant表示區段seg處于空閑狀態，route_clear表示進路進路始端信號開放，但由于一個信號可能會是多條進路的始端信號，因此，將需求細化為“進路內方道岔位置正確，始端信號開放，則進路內方區段空閑”，將route_clear進一步定義為：

"route_clear (ROUTE rt) :=

EXISTsi(rt.start_signal(si) and si.permissive and ALL sw(rt.switches(sw) =＞sw.in_required_pos(rt)))"

其中，si表示信號機，rt.start_signal(si)表示信號機si是進路rt的起始信號機，si.permissive表示信號機si為允許狀態，sw表示道岔，rt.switches(sw)表示道岔sw是進路rt內方的道岔，sw.in_required_ pos(rt)表示道岔sw當前所處的位置和進路rt要求的位置一致。

如圖3所示：（1）進站信號機X的防護進路有3條，X-S1，X-SII，X-S3，對應的進路就會被實例化為上述3條；（2）根據站場圖中的拓撲關系去實例化這3條進路的起始信號機、內方的道岔和區段；（3）當無論當前建立的進路是這3條進路中的哪一條時，驗證結果均滿足安全需求，才能夠得到對于X信號機而言，滿足“信號開放，進路內區段空閑”的安全性質。

圖3 簡單站場圖示例

根據上述的站場圖以及相關的映射關系進行實例化后共可以得到24條具體的安全需求并且全部通過驗證。

實例化后進行安全驗證主要是使用了帶有歸納功能的布爾可滿足問題（SAT）約束求解器進行模型檢驗。其中，SAT約束求解器的基本原理可以參見[5～8]。而歸納功能是針對聯鎖系統不同的周期而言的，SAT約束求解器只能針對一個周期進行求解，如果要求在任何周期都滿足，那么就需要結合歸納法：（1）檢查在初始周期是否滿足相關的性質；（2）假設某一個周期K，系統滿足相關的性質，進而去證明K+1個周期時，相關的性質也能夠得到滿足，那么就可以得到系統在任何時候都滿足對應的性質。

5 結束語

聯鎖系統是安全相關的系統，其安全性僅僅通過測試無法保障，通過形式化驗證的方式，可以遍歷環境模型約束下每條安全需求每個周期的所有狀態空間，而由于聯鎖系統軟件邏輯結構比較簡單，狀態空間大小適中，對驗證器的要求并不高，因此可以很好地進行形式化驗證。本文所應用的方法可以在不開發形式化的通用應用模型的前提下，進行安全需求的驗證，只需要開發通用應用模型與安全需求之間的接口即可，適用于對既有的聯鎖應用進行驗證，可以作為聯鎖應用開發過程中的安全補強，增加對特定聯鎖應用安全性的信心。而且不需要從需求階段就建立形式化模型，應用難度遠小于一般的形式化方法。從驗證的結果可以看到，通過對安全需求建模，對其進行實例化，再使用帶歸納法的SAT約束求解器對實例化后的安全需求進行驗證，可以很好地發現應用邏輯中不滿足安全需求的地方，從而實現安全驗證的目的。本文中所介紹的方法已經在相關實驗項目中應用，使用真實的站型驗證了其可行性。

[1]Nicolas Halbwachs,FabienneLagnier,Christophe Ratel.Programming and Verifying Real-TimeSystems by Means of the SynchronousData-Flow Language LUSTR[J].IEEE Transactions of Software Engineering,1992,18(9):785-793.

[2]古天龍.軟件開發的形式化方法[M].北京：高等教育出版社，2005：15-22.

[3]石純一，王家廞.數理邏輯與集合論[M].北京：清華大學出版社，2000：54-111.

[4]何文卿.6502電氣集中電路[M].北京：中國鐵道出版社，2007：112-132.

[5]童湖東，寧 濱，王海峰.基于Event-B的聯鎖進路控制建模驗證方法研究[J].鐵路計算機應用，2013，22（6）：57-61.

[6]季曉慧，張 健.約束問題求解[J].自動化學報，2007，33（2）：125-131.

[7]Y Vizel，G Weissenbacher，S Malik.Boolean Satisfiability Solvers and Their Applications in Model Checking[J].Proceedings of the IEEE,2015 (11):1-15.

[8]J Marques-Silva.Model checking with Boolean Satisfability[J].Journal of Algorithms,2008,63(1-3):3-16.

責任編輯 王 浩

Formal method applied to safety verifcation for computer interlocking software

LUO Juan,WANG Yanqin
( CASCO Signal Ltd., Shanghai 200071,China)

The Interlocking System is a safety critical system.Its safety cannot be guaranteed only by testing.Formal verifcation can be used to verify the consistency between the applied logic and the safety requirements of the System.In this article,the general safety requirements were instantiated with the specifc station layout.Then the specifc safety requirements were verifed through inputting them to the SAT induction constraint solver.The completeness of the method was guaranteed by covering all the instances,all the cycles and all the state space of each cycle.

computer based interlocking;safety requirement;general application;formal verifcation

U284.3∶TP39

A

1005-8451（2016）11-0053-05

2016-06-06

羅 娟，助理工程師；王燕芩，工程師。