王恪銘 ，王 霞 ，程 鵬 ，劉 寧 ，張傳東

（1.西南交通大學信息科學與技術學院，四川 成都 611756；2.西南交通大學系統(tǒng)可信性自動驗證國家地方聯合工程實驗室，四川 成都 610031；3.西南交通大學唐山研究生院，河北 唐山 063000；4.北京和利時系統(tǒng)工程有限公司，北京 100176）

車站聯鎖系統(tǒng)是典型的安全苛求系統(tǒng)，保障著車站內的行車效率與安全，該系統(tǒng)內在的行為缺陷會對車站的日常運營造成巨大的損失[1].此外，車站聯鎖系統(tǒng)由聯鎖表驅動，驗證數據的正確性對于該系統(tǒng)的安全運行也至關重要.

形式化方法是提高系統(tǒng)安全可靠性的一種有效方法，當系統(tǒng)的安全完整性等級達到SIL3級及以上時，IEC 61508[2]推薦使用該方法進行系統(tǒng)驗證.形式化方法在車站聯鎖系統(tǒng)中也有應用，如有：文獻[3]使用形式化建模工具UPPAAL建立了聯鎖系統(tǒng)的時間自動機模型，并對安全相關屬性進行了驗證；文獻[4]建立了滿足序列釋放特性的車站網絡聯鎖系統(tǒng)模型，基于有界模型檢驗及歸納推理方法，使用SMT（satisfiability modulo theories）求解器進行了驗證.

以上研究中都忽略了對聯鎖數據進行確認，近年來，基于數據視角的系統(tǒng)安全性逐漸被重視，如文獻[5]提出了一種用反例引導抽象精化范式的方法對車站聯鎖數據進行確認，文獻[6]中使用ProB證明器確認了聯鎖數據.

綜上所述，目前大多數聯鎖數據驗證研究使用的都是模型檢驗方法，針對特定對象構建專門的模型.這些方法忽略了不同車站聯鎖數據確認的通用性.且形式化驗證方法可分為模型檢驗與定理證明兩種，后者彌補了模型檢驗方法只能處理有限狀態(tài)空間的缺陷，Event-B語言是其中的典型代表，在該語言的支持平臺RODIN中，模型檢驗與定理證明兩種方法得到了有機結合[7].基于此，本文分析了聯鎖系統(tǒng)通用功能需求規(guī)范的形式化建模流程，使用Event-B語言描述，基于逐層精化策略建立了一個通用的聯鎖系統(tǒng)行為模型，并結合車站實例仿真、驗收測試，提出了車站聯鎖系統(tǒng)行為驗證與數據確認的形式化方法.

1 基于Event-B語言的形式化建模

Event-B是一種使用一階、命題邏輯與集合論作為建模符號，描述離散系統(tǒng)的建模語言[1].Event-B模型由兩部分組成[1,7]：場景文件（context）和機器文件（machine），其中場景文件定義了系統(tǒng)的靜態(tài)屬性，包括系統(tǒng)的基本組成對象以及運行時必須遵循的準則；機器文件定義了系統(tǒng)運行時的動態(tài)屬性，由變量（variable）、不變式（invariant，運行過程中應滿足的基本原則）、變體（variant）和事件（event）組成.

1.1 規(guī)范分析

建模之前需要進行規(guī)范分析.首先基于國標規(guī)范[8]，將通用聯鎖系統(tǒng)中的各類屬性按照要求分為環(huán)境類、功能類和安全類3類，其中環(huán)境類屬性被用來描述系統(tǒng)中建模的對象[1]，例如ENV_DG1：軌道區(qū)段分為道岔區(qū)段、無岔區(qū)段；功能屬性描述系統(tǒng)對象應當具備的基本功能以及其執(zhí)行條件，例如FUN_SIG1：信號機能正常顯示建立進路時應當顯示的燈色；安全類屬性描述運行過程中保障安全苛求標準應具備的條件，例如SAF_SIG2：如果區(qū)段故障占用在信號保持階段時發(fā)生，需要立即關閉信號機，但不能解鎖進路.

事件是系統(tǒng)功能在基于安全類屬性約束場景中的具體表現.在分析過程中，要得出各個功能對應的基本事件及其執(zhí)行條件，分解出復雜功能的初始化狀態(tài)、基本事件組成集合與執(zhí)行順序，并構建該功能的所有場景與安全性約束.以上過程中可使用STAMP（system-theoretic accident model and processes）等安全分析方法，并建議使用UML工具輔助構建可視化流程.且由于各屬性與事件流程的對應規(guī)范文本內容往往數倍于系統(tǒng)需求本身，管理難度加大，可使用相應的需求管理工具（如RODIN平臺中的ProR），以保持在修改過程中分析成果與后續(xù)模型的邏輯一致性.

1.2 初始模型

車站聯鎖系統(tǒng)主要是對進路流程進行控制，初始模型設計了進路的建立與解鎖.對應場景文件中定義了進路的抽象集合ROUTE；在機器文件中包含兩個事件：建立進路lock_route和解鎖進路release_route，且定義集合lockedRoute來表示已經建立的進路，r表示進路序號.本文研究的建模過程中，使用了RODIN平臺中的iUML-B插件，通過建立環(huán)境變量與事件流程UML圖（如圖1所示），直接生成場景文件與機器文件（如圖2所示），提高建模過程的準確性及自動化程度.

圖1 初始模型中事件的 UMLFig.1 UML diagram for event of initial model

圖2 初始模型中的機器文件Fig.2 Machine file in initial model

1.3 精化策略

精化策略是指在模型建立過程中，將復雜的系統(tǒng)功能進行層次分解的建模策略.即首先建立初始模型，在初始模型得到實現且通過證明后，后續(xù)模型擴展的場景文件與精化的機器文件可以繼承已被證明的定理、不變式，在此過程中逐步完善系統(tǒng)功能.本文的精化過程如表1所示.

表1 模型各層精化內容Tab.1 Refinement of the model

下文以第1層的Event-B精化模型為例，說明對象的引入與事件的添加過程.

1.3.1 第 1 層精化模型中的場景文件

定義軌道區(qū)段集合SECTION、列車的抽象集合TRAIN，EXTRA_TRACK、TRACK分別被定義為站外軌道區(qū)段、站內軌道區(qū)段，且EXTRA_TRACK?SECTION，TRACK?SECTION.站外軌道區(qū)段與站內軌道區(qū)段不能同時包含同一個軌道區(qū)段，即有如式（1）所示的公理定義.

用routeTrack表示每一條進路中含有的軌道區(qū)段.顯然，各個軌道區(qū)段可以屬于各個不同的進路，每一個進路區(qū)段也都可以包含有多條不同的軌道區(qū)段，因此routeTrack被定義為

設routeTrackNum為進路中各軌道區(qū)段的連接序號，屬于ROUTE與軌道區(qū)段有序集合TRACK的全函數，其中在軌道區(qū)段的有序集合中，使用了不同編號以表示各個軌道區(qū)段，軌道區(qū)段與編號的關系為單射函數；進路中的軌道區(qū)段數量用routeTrack-Count表示，屬于ROUTE和整數間的全函數.

用approachSection表示每條進路與其接近區(qū)段的映射關系：

1.3.2 第 1 層精化模型中的機器文件

由于加入了軌道區(qū)段，第1層精化模型中的機器文件新增了以下兩個變量：變量lockedTrack記錄鎖閉軌道區(qū)段的進路，以便在解鎖進路時對相應區(qū)段進行解鎖，因此lockedTrack為TRACK與ROUTE之間的二元關系.進路的狀態(tài)只有鎖閉或解鎖狀態(tài)兩類，故將lockedTrack定義為TRACK到ROUTE的部分函數關系；變量train_Pos用于記錄站內站外所有列車的位置信息，因此有

本層模型中共有11個事件，以圖3中的事件train_into_route為例說明如下：

圖3 精化模型一中 train_into_route 事件Fig.3 Event of train_into_route in refined model 1

該事件用于實現車輛由站外區(qū)段駛入站內，精化擴展了初始模型中的事件release_route，事件release_route中對站內區(qū)段鎖閉集合lockedRoute進行過定義.當進路r建立（grd1），且進路r的站外起始區(qū)段（比如第1離去區(qū)段）有車占用時（grd2），滿足觸發(fā)事件train_into_route執(zhí)行的條件，車輛可以由這些區(qū)段駛入站內.該事件執(zhí)行后，進路r釋放（act1），且站外區(qū)段恢復空閑，同時車輛當前位置由站外區(qū)段更新為該進路的第1個站內區(qū)段，原站外區(qū)段恢復空閑（act2）.該事件在之后各層中還將得到精化，如增加車輛初始位置限制，區(qū)分列車與調車進路等.

在事件train_into_route執(zhí)行后，將觸發(fā)執(zhí)行車輛前行事件train_move，并正常解鎖（分段解鎖）道岔、站內區(qū)段，直至車輛到達進路r的最末區(qū)段，則進路r執(zhí)行結束.此時進路r雖被釋放，但不滿足重新建立的條件，如該進路最末區(qū)段仍被占用，進路r仍為非空閑狀態(tài).最終功能實現可見該模型精化后的最后一層機器文件M6[9-10].

2 系統(tǒng)屬性驗證

2.1 驗證屬性的Event-B描述

在場景文件中，集合或常量之間的屬性定義為公理（axiom）.基于第1層精化模型中的場景文件，兩條屬性被定義成如下公理：

1）在任意進路，關系集合routeTrack對應的軌道區(qū)段，也會存在于routeTrackNum定義域所包含的軌道區(qū)段之中.其Event-B描述對應如下：

式中：符號?為蘊含操作符；dom(?)為定義域操作；?為值域限制操作[7].

2）routeTrack與routeTrackNum不等價.在調車進路當中，如果無岔區(qū)段或到發(fā)線股道是最末端的軌道區(qū)段，則在聯鎖檢查中不需要考慮該區(qū)段.routeTrack中定義的關系集合數量與routeTrackNum定義的關系集合數量有差異.即

式中：card(?)為笛卡爾積操作[7].

不變式表示系統(tǒng)的事件在執(zhí)行過程中應遵守的屬性，需保證其在模型執(zhí)行的過程中始終為真.以精化模型1的機器文件為例，其中兩條安全屬性被表達成如下不變式：

1）任意兩條敵對進路r1、r2不能同時被鎖閉，如式（8）.

式中：conflictRoute為敵對進路集合.

2）一個軌道區(qū)段最多能被一條進路鎖閉，如式（9）.

2.2 證明義務的證明

場景文件中的公理會產生證明義務，對其定義的合理性進行檢查，機器文件中的不變式通過對相關事件生成證明義務的形式，實現對事件邏輯狀態(tài)的檢查.

以下是通過添加公理完善模型，使得證明義務得到證明通過的例子.

如對第4層模型中的rotate_switch_complete_2/inv1/INV證明義務進行證明時，加入公理

式中：routeSwitchPos為建立進路r中道岔sw應被鎖閉的正確位置；dw為定位；fw為反位.

然后證明義務更新后未通過.分析過程如下：

在場景文件C4中，將routeSwitchPos定義為

式中：SWITCH為道岔的集合；道岔狀態(tài)SWITCH_POS={dw,fw,null}，null表示道岔處于四開狀態(tài).

可 見routeSwitchPos(r→ sw)的 值 可 能 是 null，故以上目標不能得到證明.在C4文件中添加公理，如式（12）.

式中：r_otherSwitchPos為與routeSwitchPos關聯的雙動道岔另一端的狀態(tài).

之后將式（12）添加作為該證明義務的假設，該證明義務得以成立.

本次建立的模型各層文件共計生成了710條證明義務，通過完善模型中的形式表達，結合手動交互式證明策略，最后所有生成的證明義務都證明通過，統(tǒng)計情況如表2所示.

表2 模型證明義務的證明情況統(tǒng)計Tab.2 Proving statistics of model proof obligations 條

從需求文本到形式化模型的邏輯轉換跨度較大，且系統(tǒng)規(guī)范也可能存在漏洞.所以，證明義務的證明過程是完善系統(tǒng)的設計規(guī)范、修正系統(tǒng)屬性及形式化模型中潛在缺陷的重要手段[1].

3 數據確認及功能仿真與測試

3.1 基于公理驗證的數據確認

以上各類證明義務全部通過，保證了聯鎖系統(tǒng)功能的可達性與安全性.若要保證實際車站聯鎖系統(tǒng)的可靠性還需要滿足：1）公理的正確性驗證.證明義務的證明過程默認公理的正確性，且將其作為證明條件；2）實際車站中聯鎖數據的安全性確認.聯鎖數據在人工編制過程中可能會發(fā)生錯誤.

文中設計了如圖4所示的技術路線來進行公理驗證及數據確認，即基于原模型1，建立一個僅有靜態(tài)場景文件的新模型2，將所有場景文件進行實例化，即基于具體車站實例數據，對場景文件中的各常量進行賦值，且將除數據定義外的各屬性公理設定為定理.該定理在系統(tǒng)中均可以自動生成相應的證明義務，通過證明來保證各公理的正確性.

圖4 數據確認的技術方案Fig.4 Technical solution for data validation

本文實例選用的是圖5所示的典型三股道車站，編制了對應的聯鎖表（只列出發(fā)車進路6條操作，另有接車進路6條未列出）如表3所示[9].

表3 舉例車站聯鎖表Tab.3 Interlocking table of the example station

圖5 舉例車站平面布置Fig.5 Layout of an example railway station

證明過程中，C1場景文件中定理routeTrackNum∈ROUTE→(TRACKZ ) 對應的證明義務未被證明通過，其中ROUTE=1，2，···，12，TRACK={IG，IIG，IIIG，1/3DG，2/4DG}，routeTrackNum已被實例化為各條進路中各軌道區(qū)段的連接序號.分析得出原因為：此定理為多級函數關系，對應狀態(tài)空間過大，超出了證明器的最大內存容量占用限制.本文設計了一種等價狀態(tài)的證明方法如下：

1）定義 4 條公理：ROUTE1={1,2,3}，ROUTE2={4,5,6}，···，ROUTE4={10,11,12}，代替ROUTE=1,2,···,12，同時定義公理：

2）實例化routeTrackNum1，routeTrackNum2，···，routeTrackNum4 為進 路ROUTE1，ROUTE2，···，ROUTE4對應的區(qū)段，代替routeTrackNum的實例化數據，同時定義公理：

3）新定義 4 條定理

routeTrackNum1∈ROUTE1→(TRACKZ )，routeTrackNum2∈ROUTE2→(TRACKZ )，··，routeTrackNum4∈ROUTE4→(TRACKZ )，同時增加1條檢查定理，檢查routeTrackNum1，route-TrackNum2，···，routeTrackNum4 的定義域相互之間不出現重疊；

4）通過證明3）中5個較小狀態(tài)空間的定理，并將證明通過的定理做為原定理證明中的前提條件，從而實現了對原定理的證明.

上述內容列在文件C1_1中，更改后驗證結果如表4所示，可見在文件C1_1中，新增的5條定理和原定理共產生的6條證明義務全部可以證明通過.

表4 公理驗證結果Tab.4 Verification of axioms 條

表4中的結果顯示，由上述車站編制的聯鎖數據達到了模型2中所有定理的要求，從而確認了聯鎖數據，且證明了原模型中公理的正確性.在模型2中已證明所舉例車站聯鎖數據滿足原模型中所有公理約束.新建一個模型3，其場景文件從模型2擴展而來，其機器文件由原模型中繼承而來.對模型3進行死鎖及是否存在違反不變式的情況進行檢驗，結果顯示，模型無死鎖且不存在違反不變式的情況.

模型中的所有公理均是開發(fā)者根據對需求的分析后而形式化設定的，在分析的過程中可能會存在錯誤的邏輯描述，或各公理之間可能存在矛盾.數據的可靠性是計算機聯鎖系統(tǒng)功能實現的基礎.本文研究中通過基于公理驗證的數據確認方法，檢查并確認了公理與數據的正確性.

3.2 驗收測試與仿真實驗

由于向不同領域的專家解釋形式化模型的屬性時存在困難，且非形式化研究人員很難確認模型事件的正確性，因此通過驗收測試與仿真實驗的方式，以說明驗證后的模型所能實現的功能.

Cucumber for Event-B[11]允許在 Event-B 模型中建立 Gherkin 場景（Gherkin scenarios），可以被用來編碼和執(zhí)行驗收測試.根據所建立模型3，建立一個應用Cucumber測試車站聯鎖進路場景的例子，如圖6所示.其中：route_delay_L為列車進路解鎖長延時事件，train_come_L為列車進站事件，train_move_L為列車在進路內行駛事件，train_leave_L為列車離去事件，switch_delay_2為雙動道岔轉動計時事件；train、train_Pos、train_type分別為列車、列車位置、列車類型，e_t為進站列車所接近的區(qū)段，L為列車類型集合.

圖6 測試場景的步驟定義Fig.6 Plain step definitions oftest scenario

基于驗證后的模型3，使用BMotionWeb插件工具制作一個典型實際車站的執(zhí)行場景，可仿真不同變量與參數下的模型響應結果，用以對聯鎖表的數據進行功能確認.其中仿真場景中的燈色、道岔、列車的狀態(tài)直接與模型中的變量相關聯.圖7中為演示聯鎖表中第10條即股道Ⅰ至發(fā)車進路S建立的場景，其中發(fā)車信號機XI顯示為綠色燈光，在仿真執(zhí)行過程中，車輛、色燈、道岔、進路與區(qū)段的狀態(tài)變化都與設計規(guī)范相符.

圖7 仿真測試舉例Fig.7 Example of simulation testing

按照圖5中車站對應的聯鎖表，在驗收測試與可視化仿真環(huán)境中逐條建立和解鎖進路，系統(tǒng)功能均可正常實現.上述過程對形式化模型進行了功能化的描述，同時還對模型的正確性做出檢查，即通過仿真實驗和驗收測試，可以檢測用戶場景的集合，為系統(tǒng)行為的可達性提供了明確的說明，可進一步檢查模型功能是否正確，與系統(tǒng)設計規(guī)范是否一致.

4 結 論

本文建立了基于規(guī)范分析得出通用系統(tǒng)形式化描述的過程，提出了一種對系統(tǒng)行為進行驗證的方法.基于規(guī)范分析得出系統(tǒng)設計的環(huán)境屬性、功能屬性、安全屬性與各事件流程，輔助使用UML工具建立初始模型的場景文件與機器文件，描述了各屬性與事件流程；對本層的證明義務進行定理證明，基于精化策略，建立了后續(xù)各層模型.通過驗證各層模型的系統(tǒng)屬性，完善了通用功能模型.基于一個實例車站的聯鎖數據對系統(tǒng)中公理的正確性進行驗證，并通過檢驗是否存在死鎖與違反不變式的情況，進一步確認了模型的可靠性.

文中提出了基于通用形式化模型對系統(tǒng)數據進行確認的方法，即將聯鎖數據注入驗證后的模型中，可以有效地進行聯鎖數據的驗證；并通過功能仿真與驗收測試技術，直觀地展現模型的功能特性，可進一步驗證系統(tǒng)行為，并同時對聯鎖數據的正確性進行了檢驗.

備注：本文相關的模型文件可在文獻[10]的鏈接中下載.