聯(lián)鎖系統(tǒng)UML模型的建立與形式化驗(yàn)證

劉 征,武曉春

(蘭州交通大學(xué)自動(dòng)化與電氣工程學(xué)院,蘭州 730070)

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

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

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

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

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

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

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

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

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

圖1 標(biāo)準(zhǔn)站場(chǎng)進(jìn)路示意

方向進(jìn)路進(jìn)路方式按下按鈕確定運(yùn)行方向道岔信號(hào)機(jī)名稱顯示表示器道岔敵對(duì)信號(hào)軌道區(qū)段迎面進(jìn)路列車調(diào)車其他聯(lián)鎖進(jìn)路號(hào)碼列車進(jì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對(duì)計(jì)算機(jī)聯(lián)鎖系統(tǒng)的進(jìn)路建立環(huán)節(jié)進(jìn)行建模。將不同類型的聯(lián)鎖設(shè)備看作UML中的類，將聯(lián)鎖設(shè)備的靜態(tài)與動(dòng)態(tài)數(shù)據(jù)通過類圖來表示；對(duì)于每個(gè)設(shè)備模塊建立相應(yīng)的狀態(tài)圖，用于描述各個(gè)設(shè)備在進(jìn)路建立階段不同的狀態(tài)；建立聯(lián)鎖系統(tǒng)的順序圖，用于描述進(jìn)路建立過程中各個(gè)模塊之間的信息交互。

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

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

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

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

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

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

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

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

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

1.4 UML順序圖的建立

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

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

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

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

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

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

2.1 UML與NuSMV模型間的映射

一個(gè)標(biāo)準(zhǔn)的NuSMV程序模板如圖6所示。

圖6 NuSMV程序模板

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

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

圖7 道岔模型片段的對(duì)比

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

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

①所以首先對(duì)道岔、軌道區(qū)段、信號(hào)機(jī)、進(jìn)路設(shè)備類依次進(jìn)行轉(zhuǎn)換，它們的NuSMV模塊名需要保持與原類名相同。

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

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

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

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

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

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

next(status):=

case

status=轉(zhuǎn)移之前的狀態(tài)&防護(hù)條件1&防護(hù)條件2…:{目標(biāo)狀態(tài)};

1:status;

esac

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

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

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

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

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

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

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

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

圖8 模型轉(zhuǎn)換程序的工作流程

3 NuSMV模型的形式化驗(yàn)證

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

3.1 NuSMV模型的驗(yàn)證語句

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

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

SPEC EF(x.status=doubleYellow)

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

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

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

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

(3)安全性：指系統(tǒng)不發(fā)生某件“不期望”的事件的屬性。同樣以1號(hào)道岔為例，在道岔鎖閉狀態(tài)進(jìn)行道岔定位與反位的轉(zhuǎn)換操作是不應(yīng)該出現(xiàn)的，將其表示為驗(yà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))表示存在一個(gè)狀態(tài)a，它的下一個(gè)狀態(tài)可以是b，在其之前加上“非”的符號(hào)即表示不存在這樣的狀態(tài)轉(zhuǎn)移。

同理，若排列接車進(jìn)路X→SⅢ時(shí)，敵對(duì)信號(hào)SⅢD已開放，則該條進(jìn)路不應(yīng)該開放，可表示為如下語句：

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

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

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

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

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

3.2 驗(yàn)證結(jié)果

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

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

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

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

圖10 加入錯(cuò)誤的聯(lián)鎖NuSMV模型驗(yàn)證結(jié)果片段

4 結(jié)語

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

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

(3)使用NuSMV符號(hào)模型驗(yàn)證工具對(duì)該模型進(jìn)行驗(yàn)證，證實(shí)了該聯(lián)鎖模型的正確性。

(4)通過間接建立形式化模型的方法，減少了聯(lián)鎖軟件開發(fā)人員對(duì)形式化相關(guān)知識(shí)的高要求，降低了對(duì)聯(lián)鎖系統(tǒng)進(jìn)行形式化建模與驗(yàn)證的難度，并且通過模型轉(zhuǎn)換程序?qū)崿F(xiàn)自動(dòng)生成模型，能夠避免人工建模可能出現(xiàn)的錯(cuò)誤，為計(jì)算機(jī)聯(lián)鎖系統(tǒng)的形式化建模與驗(yàn)證提供一種新思路。

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

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

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

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

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

[4] 王瑞峰.鐵路信號(hào)運(yùn)營基礎(chǔ)[M].北京：中國鐵道出版社，2008：91-101

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

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

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

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

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

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

[11] 薛豐，楊揚(yáng)，謝林.基于UML建模的計(jì)算機(jī)聯(lián)鎖進(jìn)路模塊Petri網(wǎng)驗(yàn)證[J].鐵路計(jì)算機(jī)應(yīng)用，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] 朱利魯，李智.問題框架中問題領(lǐng)域因果行為的形式化驗(yàn)證[J].計(jì)算機(jī)科學(xué)，2015，42(12):136-142.

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

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