劉 征,武曉春

(蘭州交通大學自動化與電氣工程學院,蘭州 730070)

隨著軟件技術的不斷發(fā)展，人們對于軟件的正確性與安全性的要求也在不斷提高，在許多領域中提出需使用安全苛求系統(tǒng)作為安全的保障[1]。在國際電工委員會提出的IEC61508標準中指出：當系統(tǒng)的安全完善度等級為4級(SIL4)時，強烈推薦使用形式化證明的方法對系統(tǒng)進行建模與驗證[2]。然而形式化語言難以理解，隨著軟件系統(tǒng)變得越來越龐大、越來越復雜，直接使用形式化方法對系統(tǒng)需求規(guī)范進行建模，對形式化相關理論知識的要求也變得越來越高[3]。

計算機聯(lián)鎖技術作為控制鐵路運輸?shù)闹匾踩Ｕ霞夹g，在各個車站已被廣泛應用。其中，聯(lián)鎖程序的設計是鐵路建設中至關重要的一個環(huán)節(jié)。計算機聯(lián)鎖系統(tǒng)是典型的SIL4級系統(tǒng)，其系統(tǒng)需求規(guī)范中的任何缺陷都有可能導致安全事故的發(fā)生。隨著站場規(guī)模的擴大，其聯(lián)鎖系統(tǒng)也會越來越復雜，對聯(lián)鎖系統(tǒng)規(guī)范進行嚴格的驗證，對保證安全苛求系統(tǒng)安全高效運行具有重要的意義[4-6]。

UML統(tǒng)一建模語言易于表達，描述直觀，在現(xiàn)今的面向對象建模領域中被廣泛應用。文獻[7]提出一種基于UML的聯(lián)鎖進路控制過程的半形式化模型。該模型有利于加強開發(fā)人員對系統(tǒng)的理解。但UML本身作為一種半形式化的建模語言，不能提供嚴格的自動分析和驗證方法[8-9]。

由美國Carnegie Mellon大學和Trento大學聯(lián)合開發(fā)的符號模型檢驗器NuSMV是一種高效的形式化驗證工具。它基于二叉判決樹對系統(tǒng)是否滿足CTL(Computation Tree Logic，計算樹邏輯)進行判斷，緩解了模型檢測中出現(xiàn)的狀態(tài)爆炸的問題[10]。并且它可以驗證系統(tǒng)性質，若一個性質不滿足可給出其不滿足的原因。NuSMV工具已經成功應用于多個領域進行安全分析[10-17]。文獻[10]提出將聯(lián)鎖關系用SMV語言進行表達，并通過CTL驗證語句分析聯(lián)鎖關系的正確性，但由于直接通過SMV形式化語言建模難度較大，僅搭建了基礎的模型，并驗證了幾條簡單聯(lián)鎖關系；文獻[11]采用UML狀態(tài)圖對聯(lián)鎖邏輯進行建模，并通過Petri網(wǎng)對其進行形式化驗證，由于僅使用了UML狀態(tài)圖進行分析，模型的信息量不足，且需人工對模型進行轉換；文獻[12]利用抽象狀態(tài)機與NuSMV結合對聯(lián)鎖邏輯進行建模與驗證，但并沒有應用于具體聯(lián)鎖系統(tǒng)模型；文獻[17]利用Event-B方法與多智能體系統(tǒng)(MAS)結合，通過細化形式化模型對聯(lián)鎖系統(tǒng)進行形式化建模并驗證，但細化過程復雜，即使非常小的車站其生成的模型也很冗長?？梢姡瑐鹘y(tǒng)的形式化模型驗證方法要求使用者掌握特定的形式化規(guī)范語言和時態(tài)邏輯的相關知識，使用難度較大，且無法做到自動生成具體聯(lián)鎖系統(tǒng)的形式化模型。

綜上所述，由于計算機聯(lián)鎖系統(tǒng)對安全的高要求，需在系統(tǒng)開發(fā)初期對其需求進行形式化建模，而直接采用形式化語言描述一個復雜系統(tǒng)，對于缺乏形式化方法專業(yè)知識的聯(lián)鎖軟件開發(fā)人員而言難度較大且容易出錯。為了降低對系統(tǒng)形式化建模與驗證的難度與減少人工建模時可能出現(xiàn)的錯誤，本文提出了一種UML與NuSMV相結合的形式化模型檢驗方法。通過簡單易懂與通用性強的UML對系統(tǒng)需求進行建模，再與高效的形式化驗證工具NuSMV結合，從而間接地完成對聯(lián)鎖系統(tǒng)的形式化建模與驗證。

1 計算機聯(lián)鎖系統(tǒng)UML模型的建立

1.1 系統(tǒng)需求分析

鐵路車站的計算機聯(lián)鎖系統(tǒng)是一種典型的安全苛求系統(tǒng)，其主要的功能是將車站中的軌道電路、道岔、信號機通過聯(lián)鎖運算聯(lián)系控制，實現(xiàn)控制列車的進路建立與解鎖，保證列車的安全高效運行。以一個標準站場的接車進路的建立過程為例進行分析[4]，如圖1所示，建立X→SIII的接車進路模型，通過對該模型進行建模與驗證，對本文提出的方法進行闡述。

當操作員在監(jiān)控機按順序按下X與SⅢ的按鈕后，建立X→SⅢ接車進路的命令被發(fā)送至聯(lián)鎖機。聯(lián)鎖機首先會檢查聯(lián)鎖表，如表1所示，并根據(jù)聯(lián)鎖表對該條進路上相關設備的狀態(tài)信息進行檢查。接下來聯(lián)鎖機檢查三大聯(lián)鎖條件，即依次檢查軌道區(qū)段是否空閑，道岔位置是否正確且鎖閉，敵對信號是否建立，若符合進路建立的條件，則進路鎖閉，信號開放。

圖1 標準站場進路示意

方向進路進路方式按下按鈕確定運行方向道岔信號機名稱顯示表示器道岔敵對信號軌道區(qū)段迎面進路列車調車其他聯(lián)鎖進路號碼列車進路北京方面接車至Ⅲ股道1XLA、SⅢLA(23/25)XUU5/7、1/3、9/11、13/15、17/19、(23/25)D3、D7、D9、D13、SⅢDIAG、5DG、3DG、9-15DG、17-23DG、25DG、<21>21DG、IIIGIIIGIIIG16

利用UML對計算機聯(lián)鎖系統(tǒng)的進路建立環(huán)節(jié)進行建模。將不同類型的聯(lián)鎖設備看作UML中的類，將聯(lián)鎖設備的靜態(tài)與動態(tài)數(shù)據(jù)通過類圖來表示；對于每個設備模塊建立相應的狀態(tài)圖，用于描述各個設備在進路建立階段不同的狀態(tài)；建立聯(lián)鎖系統(tǒng)的順序圖，用于描述進路建立過程中各個模塊之間的信息交互。

1.2 聯(lián)鎖系統(tǒng)UML類圖的建立

UML的類圖用于對系統(tǒng)的各種概念進行建模，屬于對系統(tǒng)的靜態(tài)結構進行描述的視圖。如圖2所示。

圖2 聯(lián)鎖系統(tǒng)UML模型類圖

根據(jù)系統(tǒng)的需求，建立軌道區(qū)段(Section)、道岔(Switch)與信號機(Signal)的設備類，其中信號機類分為列車信號機(TrainSignal)與調車信號機(ShuntingSignal)，并根據(jù)聯(lián)鎖表的概念建立進路(Route)類，其中每個類中包含了對該設備的操作函數(shù)，表2列舉了這些操作函數(shù)的定義。并根據(jù)聯(lián)鎖表上對應的設備，建立與該條進路相關的信號機、道岔與軌道區(qū)段設備的實例模塊。

表2 類圖中操作函數(shù)定義

1.3 UML狀態(tài)圖的建立

與類圖相對應的，系統(tǒng)中每個類的動態(tài)行為由UML的狀態(tài)圖進行描述。它重點描述的是一個實體如何根據(jù)當前所處的狀態(tài)對接收到的事件與防護條件做出反應。根據(jù)聯(lián)鎖進路建立過程中各個設備類狀態(tài)的變化所建立的狀態(tài)如圖3所示。在進路建立時，每種狀態(tài)轉移的防護條件需根據(jù)相關的聯(lián)鎖關系詳細列出。

圖3 聯(lián)鎖系統(tǒng)設備狀態(tài)

如圖3(a)中道岔定位與反位轉換的條件是其處于解鎖狀態(tài)(switch.unlocked=1)；道岔鎖閉的條件是正在排列進路(route.status=presetting)且道岔位置正確(rightposition=1)；圖3(b)中軌道區(qū)段的狀態(tài)變化只與是否有車占用有關(train=0/1)；圖3(c)與圖3(d)中信號機開放的條件是進路已鎖閉(route.status=locking)，道岔處于正確的位置(switch.rightposition=1)且鎖閉(switch.unlocked=0)，敵對信號未建立(signal.status=red|blue)；而圖3(e)中進路鎖閉的條件是相關軌道區(qū)段空閑(section.status=clear)，道岔處于正確的位置且鎖閉，敵對信號未建立。

1.4 UML順序圖的建立

UML順序圖用于表現(xiàn)一個用例中各個元素間的交互，重點強調事件順序。

聯(lián)鎖系統(tǒng)進路建立過程的順序如圖4所示。在進路建立的過程中，聯(lián)鎖系統(tǒng)首先根據(jù)聯(lián)鎖表對該條進路相關的軌道區(qū)段、道岔、信號機設備進行狀態(tài)采集，若道岔位置不正確則將其轉換至正確位置并鎖閉，并根據(jù)采集到的設備的狀態(tài)信息進行聯(lián)鎖運算，從而控制進路的開放。

圖4 聯(lián)鎖系統(tǒng)進路建立順序

2 聯(lián)鎖UML模型到NuSMV模型的轉換

若要使用工具對聯(lián)鎖系統(tǒng)模型進行驗證，需要將其轉換為形式化描述語言。對聯(lián)鎖UML模型進行形式化驗證的系統(tǒng)框圖如圖5所示。

圖5 聯(lián)鎖UML模型形式化驗證系統(tǒng)

2.1 UML與NuSMV模型間的映射

一個標準的NuSMV程序模板如圖6所示。

圖6 NuSMV程序模板

在一個NuSMV程序中包含一個main模塊和若干個子模塊。main模塊中通常描述系統(tǒng)各個元素間的交互，子模塊用于描述系統(tǒng)的各個部分的功能。其中每個模塊中均包含如下幾個部分：VAR部分負責聲明變量；DEFINE部分為簡寫字段，用于定義宏來使程序語句更加簡潔；ASSIGN部分負責為變量賦值，可描述狀態(tài)的初值與變化；SPEC部分只存在于main模塊中，其包含驗證語句，通過CTL表達式對模型進行驗證。

以第一章中道岔模型為例，圖7(a)為對這兩種模型片段的對比，可見在UML模型片段中，該模塊的名稱、初始狀態(tài)、狀態(tài)遷移等信息都能夠完整地提取出來。

圖7 道岔模型片段的對比

UML與NuSMV模型間的映射規(guī)則如下。

(1)對于類圖的轉換，通過對UML與NuSMV這兩種模型的比較可發(fā)現(xiàn)，UML中的類的定義與NuSMV程序中的子模塊定義非常類似，都是對系統(tǒng)進行模塊化描述。

①所以首先對道岔、軌道區(qū)段、信號機、進路設備類依次進行轉換，它們的NuSMV模塊名需要保持與原類名相同。

②由于各個設備模塊之間存在著聯(lián)鎖關系，所以每個模塊需要以其他模塊的狀態(tài)作為自身的輸入?yún)?shù)。如圖7中道岔的狀態(tài)受到它所在的進路與軌道區(qū)段的制約。

③UML類中的變量應在NuSMV中的VAR字段中聲明。在道岔模型中設布爾變量rightposition用來表示道岔是否處于正確位置。

④在NuSMV中的ASSIGN部分需要將擁有初值的變量以init(var)語句進行賦值。由于在初始狀態(tài)時相關進路信息未知，所以在道岔模型中無法判斷是否處于正確位置，故設rightposition=0的初始值。

(2)在UML模型中狀態(tài)圖依附于類圖，所以在轉換狀態(tài)圖時應將狀態(tài)圖內容轉換至與類圖相同的模塊中，用于描述模塊的動態(tài)行為。在該模塊的VAR部分應聲明其所有可能所處的狀態(tài)，因此需添加一個枚舉型的變量status用來枚舉出其所有狀態(tài)。根據(jù)圖3(a)可知道岔的基本狀態(tài)為normal與reverse兩種。

①UML中的狀態(tài)圖與NuSMV中的ASSIGN部分都有描述模塊狀態(tài)轉移的功能，在該模塊的ASSIGN部分應使用init(status)語句對模塊的初始狀態(tài)進行定義。

②使用next(status)語句描述狀態(tài)的轉換，需將轉換前的狀態(tài)與防護條件列出，使用case語句進行分支判斷，其格式為：

next(status):=

case

status=轉移之前的狀態(tài)&防護條件1&防護條件2…:{目標狀態(tài)};

1:status;

esac

其中1：status代表若無符合的轉移條件，則保持原狀態(tài)不變。根據(jù)狀態(tài)圖中的防護條件，得到道岔定位與反位轉換的條件是其處于解鎖狀態(tài)(unlocked=1)，道岔鎖閉的條件是正在排列進路(route.status=presetting)且道岔位置正確(rightposition=1)。

③一個模塊中可能會存在著復合狀態(tài)的情況，如“與”狀態(tài)(并發(fā)狀態(tài))和“或”狀態(tài)(互斥狀態(tài))。如圖3(a)中道岔的狀態(tài)圖所示，可見其根狀態(tài)有unlocked與locked兩種，只有在unlocked狀態(tài)下才可進行定位normal與反位reverse兩種子狀態(tài)的轉換。這種復合狀態(tài)需將其分層展開，由根狀體到子狀態(tài)逐級進行轉換。在模型轉換時首先將根狀態(tài)以布爾變量進行描述，在道岔例子中應對應根狀態(tài)建立兩個量:locked，unlocked并賦予它們初始值，接下來將其加入到子狀態(tài)遷移的防護條件中。

(3)對于UML順序圖，由于其描述的是模塊之間信息的交互，為描述系統(tǒng)整體行為的視圖，所以應該對應地將其內容轉換至main模塊中去。

①由于描述的是異步系統(tǒng)，在NuSMV模型的main模塊中的VAR部分定義process進程函數(shù)，以順序圖為依據(jù)依次運行系統(tǒng)中的各模塊，完成系統(tǒng)的交互框架。

②將實例化的設備名作為process函數(shù)的對象名，其設備類型作為函數(shù)名，若存在傳遞參數(shù)則將之添加為process函數(shù)的參數(shù)。

2.2 聯(lián)鎖UML模型到NuSMV模型轉換的實現(xiàn)

為了實現(xiàn)模型的自動轉換，首先需要將UML模型完整地輸出為可讀取的格式?，F(xiàn)有的方法主要是將UML模型以XML格式進行輸出[3，15]，該方法得到的模型代碼的冗余信息較多，不利于提取信息。通過美國I-Logix公司開發(fā)的Rhapsody軟件中的模型驅動技術，可以實現(xiàn)將上文中建立好的聯(lián)鎖UML模型輸出為可運行的C++代碼，再將其根據(jù)上一節(jié)提出的轉換規(guī)則轉換為NuSMV程序模型文件，使用該方法輸出的模型文件與軟件的源代碼接近，且冗余信息少，有利于通過編程對其進行轉換。

本文在C#環(huán)境下編寫了將UML模型的C++代碼轉換為NuSMV模型的轉換程序。模型轉換程序的工作流程如圖8所示。

圖8 模型轉換程序的工作流程

3 NuSMV模型的形式化驗證

NuSMV模型驗證器使用CTL公式對系統(tǒng)所擁有的屬性進行驗證。若系統(tǒng)滿足該條屬性，則驗證語句的結果為True；若不滿足，驗證程序會返回False并列出不滿足的原因。

3.1 NuSMV模型的驗證語句

對于計算機聯(lián)鎖系統(tǒng)，需要進行驗證的屬性主要是關于聯(lián)鎖邏輯的正確性，即系統(tǒng)是否能根據(jù)聯(lián)鎖表實現(xiàn)道岔、信號機、軌道區(qū)段與進路之間聯(lián)鎖的功能。以X→SⅢ接車進路為例，需要驗證的性質可分為如下幾類。

(1)可達性：指系統(tǒng)能夠從某一狀態(tài)到達目標狀態(tài)，滿足該性質表示系統(tǒng)中沒有永遠也無法達到的狀態(tài)。例如如下語句：

SPEC EF(x.status=doubleYellow)

其中EF(a)表示存在一條路徑使公式a最終成立，即代表接車進路X→SⅢ存在最終開放的可能性。

(2)互斥性：指系統(tǒng)不能同時處于某幾個狀態(tài)中。以1號道岔為例，它處于定位的同時不能處于反位，該屬性可表示為：

SPEC ! EF(Sw1.status=normal & Sw1.status=reverse)

其中! EF(a & b)的含義是不存在一個未來狀態(tài)滿足a與b同時成立。

(3)安全性：指系統(tǒng)不發(fā)生某件“不期望”的事件的屬性。同樣以1號道岔為例，在道岔鎖閉狀態(tài)進行道岔定位與反位的轉換操作是不應該出現(xiàn)的，將其表示為驗證語句為：

SPEC ! EF((Sw1.locked=1 & Sw1.status=normal) & EX(Sw1.status=reverse))

SPEC ! EF((Sw1.locked=1 & Sw1.status=reverse) & EX(Sw1.status=normal))

EF(a & EX(b))表示存在一個狀態(tài)a，它的下一個狀態(tài)可以是b，在其之前加上“非”的符號即表示不存在這樣的狀態(tài)轉移。

同理，若排列接車進路X→SⅢ時，敵對信號SⅢD已開放，則該條進路不應該開放，可表示為如下語句：

SPEC AG !(x.status=doubleYellow & SiiiD.status!=red)

其中AG !(a & b)的含義是在所有節(jié)點都不存在a與b同時成立的情況。

(4)活性屬性：指的是系統(tǒng)“期望”發(fā)生的事件的屬性。例如“接車進路X→SⅢ選排完成時相應的信號X機會開放”可以表示為如下語句：

SPEC EG(X_Siii.status=locking-> AF(x.status=doubleYellow))

其中AF(b)代表公式b最終會成立，而由于進路選排完成后也有可能取消進路，所以寫為EG(a-> AF(b))，即公式a成立，存在一條路徑使得公式b最終成立。

3.2 驗證結果

根據(jù)表1中的聯(lián)鎖關系，可得一條進路建立過程中需要驗證的聯(lián)鎖相關屬性：通過安全性驗證三大聯(lián)鎖條件是否滿足與所有道岔在鎖閉時不可進行轉換的性質；通過互斥性驗證雙動道岔中(包括交叉渡線與帶動道岔)相關道岔位置的正確性；通過可達性與活性驗證該條進路開放的可能性。

最終得到的驗證結果片段如圖9所示?？梢?，驗證語句的結果均為true，從而可證明聯(lián)鎖模型正確。

圖9 聯(lián)鎖NuSMV模型驗證的結果片段

通過驗證的結果可分析出計算機聯(lián)鎖模型中的出錯的環(huán)節(jié)。為了體現(xiàn)本文所提出的方法驗證模型內部錯誤的能力，首先在聯(lián)鎖UML模型中將道岔轉動的防護條件Sw1.unlocked=1刪除，即表示1號道岔在鎖閉的情況下也會進行定反位的轉換。然后重新將其轉換為NuSMV模型并進行驗證。在圖10中可見驗證1號道岔的安全性的語句結果為false與舉出的反例，從而可以得出UML模型該處存在問題。

圖10 加入錯誤的聯(lián)鎖NuSMV模型驗證結果片段

4 結語

(1)本文以一個簡單的聯(lián)鎖進路作為實例，對該條進路的建立過程進行了分析，并建立了計算機聯(lián)鎖系統(tǒng)中該過程對應的UML類圖、狀態(tài)圖、順序圖模型。

(2)分析了UML與NuSMV模型的映射關系，并通過在C#環(huán)境下編寫的模型轉換程序，將UML模型轉化為NuSMV形式化模型。

(3)使用NuSMV符號模型驗證工具對該模型進行驗證，證實了該聯(lián)鎖模型的正確性。

(4)通過間接建立形式化模型的方法，減少了聯(lián)鎖軟件開發(fā)人員對形式化相關知識的高要求，降低了對聯(lián)鎖系統(tǒng)進行形式化建模與驗證的難度，并且通過模型轉換程序實現(xiàn)自動生成模型，能夠避免人工建?？赡艹霈F(xiàn)的錯誤，為計算機聯(lián)鎖系統(tǒng)的形式化建模與驗證提供一種新思路。

(5)在驗證語句輸入過程中，每條聯(lián)鎖關系都需要人工將其轉化為CTL表達式，對于大型站場重復工作量較大，在今后研究的過程中可以開發(fā)根據(jù)聯(lián)鎖表自動生成CTL驗證語句的方法。

(6)后續(xù)工作中將對測試用例的相關內容進行研究，實現(xiàn)自動生成測試用例，對計算機聯(lián)鎖系統(tǒng)的需求完成更全面的驗證。

[1] 吳曉丹，寧濱.基于UML的建模及模型檢驗研究[J].現(xiàn)代電子技術，2011，34(6):50-54.

[2] 劉金濤，唐濤，徐田華，趙林.基于UML的CTCS-3級列控系統(tǒng)需求規(guī)范形式化驗證方法[J].中國鐵道科學，2011，32(3):93-99.

[3] 劉心鈺.基于UML的系統(tǒng)需求形式化分析方法[D].北京：北京交通大學，2015.

[4] 王瑞峰.鐵路信號運營基礎[M].北京：中國鐵道出版社，2008：91-101

[5] 高雪娟.基于UML的計算機聯(lián)鎖軟件測試用例生成方法的研究[D].蘭州：蘭州交通大學，2014.

[6] 趙志熙.計算機聯(lián)鎖系統(tǒng)技術[M].北京：中國鐵道出版社，1999：132-135.

[7] 李穎.基于UML的車站信號軟件建模[D].北京：北京交通大學，2008.

[8] 單黎君，朱鴻.UML的形式化描述語義[J].計算機工程與科學，2010，32(3):96-103.

[9] 韓德帥，楊啟亮，邢建春.一種軟件自適應UML建模及其形式化驗證方法[J].軟件學報，2015，26(4):730-746.

[10] 燕飛，唐濤.計算機聯(lián)鎖控制邏輯的模型檢驗方法[J].鐵道通信信號，2009，45(5):26-29.

[11] 薛豐，楊揚，謝林.基于UML建模的計算機聯(lián)鎖進路模塊Petri網(wǎng)驗證[J].鐵路計算機應用，2017(4):10-14.

[12] A MIRABADI， M B YAZDI. Automatic generation and verification of railway interlocking control tables using FSM and NuSMV[J]. International Journal for Engineering Modelling，2008，21(4):57-63.

[13] P JAMES, F MOLLER， H N NGUYEN， et al. Techniques for modelling and verifying railway interlockings[J]. International Journal on Software Tools for Technology Transfer， 2014，16(6):685-711.

[14] D ZARMIRAL，C RANCEL. Comparing model checkers for timed UML activity diagrams[J]. Science of Computer Programming， 2015，111(2):277-299.

[15] 朱利魯，李智.問題框架中問題領域因果行為的形式化驗證[J].計算機科學，2015，42(12):136-142.

[16] 何洋，洪玫，祁琳瑩，等.基于模型檢測工具NuSMV的功能測試用例生成方法[J].計算機應用，2015，35(S2):155-159.

[17] 胡曉輝，韓佳芮.車站聯(lián)鎖進路控制邏輯的形式化方法[J].計算機工程與應用，2016(17):229-234.