基于形式化方法的道口控制系統(tǒng)規(guī)范建模與驗證

王恪銘 ，王 崢

（1.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院，四川 成都 611756；2.西南交通大學(xué)系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室，四川 成都 610031）

道路與鐵路的平面交匯形成了鐵路道口，目前鐵路道口數(shù)量多，且由于公路方向上的行人、車輛與列車通行存在矛盾的客觀性，使得鐵路道口隱藏著潛在的事故風(fēng)險.近年來我國鐵路道口平交改立交取得了成效，但數(shù)量依然龐大，僅正線上全國鐵路的道口就有數(shù)千處（2013年底為7 519 處）[1].最新調(diào)查數(shù)據(jù)顯示：歐盟28 國中有114 580 道口，平均每10 km的線路上就有5 處道口（2014年）[2]；2015年中道口事故占全部鐵道事故的比例約為25.9%（469/1 808），道口事故造成的受傷人員比例為38.6%（264/684），死亡人員占比為30.7%（296/963）[3].可見，改善鐵路道口的安全狀況對于減少人員傷亡與財產(chǎn)損失，提高行車效率有著重要意義.

近年來道口安全研究引起了學(xué)者們的重視，影響道口安全的因素中，除了涉及行人、車輛、環(huán)境、道口特性等之外，還包含道口管理及其安全防護裝置等因素[4].目前在相關(guān)道口控制系統(tǒng)的研究中，主要體現(xiàn)在對不同種類道口設(shè)備的可靠性分析[5]，增加傳感器、視頻分析等新道口裝置的研究[6-7].

道口控制系統(tǒng)的研發(fā)是基于設(shè)計規(guī)范進(jìn)行的，使用形式化方法可以檢查系統(tǒng)規(guī)范，完善設(shè)計模型，且可大幅減少后續(xù)測試階段發(fā)現(xiàn)的錯誤，顯著提升工程質(zhì)量與開發(fā)效率[8].當(dāng)系統(tǒng)的安全完整性水平（safety integrity level，SIL）要求達(dá)到3 級及以上時，IEC61508 標(biāo)準(zhǔn)強烈建議使用形式化方法對系統(tǒng)進(jìn)行驗證[9].不同于具體功能算法測試后所得的指標(biāo)比較[10]，形式化方法強調(diào)對系統(tǒng)設(shè)計中邏輯流程的驗證[8].以上研究中，都忽略了道口規(guī)范可能存在缺陷及規(guī)范理解不全面對系統(tǒng)可靠性的影響；文獻(xiàn)[5]使用了Petri 網(wǎng)、文獻(xiàn)[6]使用了UPPAAL 時間自動機的形式化分析方法，但這些形式化方法缺少定理證明的能力，通過驗證的模型不能直接用于生成系統(tǒng)的初始代碼.

道口控制系統(tǒng)作為一類安全苛求系統(tǒng)，任何潛在的系統(tǒng)缺陷都可能會給道口運營安全帶來巨大風(fēng)險.據(jù)統(tǒng)計顯示，系統(tǒng)中1/3 左右的禍根都是在需求分析階段埋下的，但其糾正成本要占整體糾正費用的70%以上[11].因此，在設(shè)計研發(fā)階段檢查規(guī)范缺陷，對于保證系統(tǒng)功能的安全性、可靠性和完備性尤為重要.本文基于道口管理規(guī)范，分析得出道口管理的場景、功能、安全屬性，建立事件邏輯流程，使用形式化方法及逐層精化策略建立了包含道口控制系統(tǒng)主要功能的系統(tǒng)原型，并基于Event-B 語言描述了系統(tǒng)驗證特性，通過證明過程，檢查了系統(tǒng)的安全與時間特性，完善了功能模型，通過系統(tǒng)設(shè)計原型的建立過程 ，揭示了目前管理規(guī)范中的不足，改進(jìn)了系統(tǒng)設(shè)計并進(jìn)行了驗證確認(rèn)，得出了對系統(tǒng)的功能規(guī)范進(jìn)行建模與驗證的形式化流程與方法.

1 功能規(guī)范分析

本文研究的是一個安裝有自動防護裝置的道口控制系統(tǒng)（有人值守），道口公路方向有可升降的欄門（或欄桿），系統(tǒng)示意如圖1所示.道口來車方向設(shè)置有兩個接近區(qū)段，列車駛向道口前在點A（接近點）與點C（逼近點）處發(fā)送預(yù)警信息.根據(jù)規(guī)范要求，A的位置應(yīng)設(shè)置在接近通知時間不小于40 s 處（即列車從該處到達(dá)道口的時間，上限為90 s，按列車通過最大時速120 km/h 計算），C距離道口不小于列車的最大制動距離，并考慮適當(dāng)?shù)陌踩哂?其中T1為列車從A至C的時間、T2為列車從C至道口的時間.

圖1 鐵路道口控制系統(tǒng)示意Fig.1 Schematic diagram of control system for railway level crossings

對道口控制系統(tǒng)的驗證需要確認(rèn)系統(tǒng)在通用標(biāo)準(zhǔn)及管理規(guī)范的約束下能否正確運行.首先需要深入解讀道口規(guī)范的文本內(nèi)容，析取各個功能事件的邏輯流程，分析得出系統(tǒng)的環(huán)境屬性、功能屬性、安全屬性，構(gòu)建好形式化描述的對象.

1.1 事件流程

基于平交鐵路道口的管理規(guī)范，歸納得出道口控制系統(tǒng)的基本需求為：列車、道路上的行人與車輛可以分別安全地通過道口[12-13].具體的實現(xiàn)規(guī)范為：避免鐵路上列車與道路上行人、車輛交通的沖突，即當(dāng)列車即將通過前，行人與車輛應(yīng)當(dāng)出清，欄門及時關(guān)閉；列車駛離道口后，欄門及時開放，道路上的行人與車輛可以安全通過.析取出相應(yīng)的流程如下：當(dāng)系統(tǒng)檢測到列車已到達(dá)接近點A，給出接近報警信號，同時信號燈轉(zhuǎn)變成紅燈并進(jìn)行道口出清作業(yè)，之后發(fā)出欄門下降命令，道口關(guān)閉；當(dāng)列車到達(dá)接近點C時，給出列車逼近報警信號，信號燈紅閃；當(dāng)列車駛離道口時，道口欄門升起，信號燈亮白燈，道口再次開放.流程如圖2所示.

圖2 道口控制系統(tǒng)中的事件流程Fig.2 Events flows of control system for railway level crossings

1.2 屬性提取

分析道口設(shè)計規(guī)范，將其中的屬性要求分為環(huán)境類、功能類和安全類共3 類.環(huán)境類屬性（ENV）用于描述系統(tǒng)中建模對象的性質(zhì)，功能屬性（FUN）描述系統(tǒng)應(yīng)當(dāng)具備的基本功能，安全類屬性（SAF）描述系統(tǒng)在運行過程中應(yīng)具備的安全條件.

提取出環(huán)境類屬性如下：

ENV1：道口門欄的狀態(tài)包括升起中、開啟、下降中、關(guān)閉.

ENV2：控制器對欄門的控制命令包括升起、下降.

ENV3：列車在道口附近的狀態(tài)包括到達(dá)接近點A、到達(dá)逼近點C、離去.

ENV4：道口信號燈的狀態(tài)包括紅燈、紅閃、白燈.

ENV5：控制器對信號燈的控制命令包括紅燈亮、紅燈閃、白燈亮.

結(jié)合事件的流程分析，功能類屬性有：

FUN1：控制器通過升起、下降命令控制欄門的狀態(tài)轉(zhuǎn)換：開啟→下降中→關(guān)閉→升起中→開啟.

FUN2：列車到達(dá)接近點A、到達(dá)逼近點C及離開道口時，應(yīng)給出相應(yīng)信號.

FUN3：列車到達(dá)接近點A時，發(fā)出接近信號，道口信號燈轉(zhuǎn)變成紅燈并進(jìn)行道口出清作業(yè)，之后欄門下降，道口關(guān)閉.

FUN4：列車到達(dá)逼近點C時，發(fā)出逼近信號，道口信號燈紅閃，列車經(jīng)過T2時間后將通過道口.

FUN5：當(dāng)列車駛離道口時，道口欄門準(zhǔn)備升起，延時一段時間后道口再次開放，信號燈亮白燈.

安全類屬性有：

SAF1：當(dāng)列車即將通過道口時，道口應(yīng)該關(guān)閉.

SAF2：當(dāng)列車離去時，道口才可重新開放.

2 基于Event-B 方法的形式化建模

Event-B 是一種描述離散系統(tǒng)的建模語言，使用一階邏輯、命題邏輯與集合論作為建模符號，在其支持平臺Rodin 中，模型檢驗與定理證明兩種形式化方法得到了結(jié)合應(yīng)用.Event-B 模型由兩部分組成：場景文件（Context）和機器文件（Machine），其中場景文件定義了系統(tǒng)的靜態(tài)屬性，包括系統(tǒng)的基本組成對象以及運行時必須遵循的準(zhǔn)則，場景文件由載體集合（Carrier Set，系統(tǒng)實際對象的抽象集合）、常量（Constant，系統(tǒng)中的固定對象）、公理（Axiom，系統(tǒng)中的普遍原則或先驗的通用準(zhǔn)則）組成[14-15].

機器文件定義了系統(tǒng)運行時的動態(tài)屬性，由變量（Variable）、不變式（Invariant，系統(tǒng)動態(tài)運行過程中應(yīng)滿足的基本原則）、變體（Variant）和事件（Event）.事件包含事件參數(shù)（Event Parameter）、等價關(guān)系（Witness）、防衛(wèi)條件（guard）、動作（action）等組成.事件定義了系統(tǒng)狀態(tài)之間的遷移，模型執(zhí)行時最先觸發(fā)初始化事件（INITIALISATION）.

2.1 初始模型

在各事件的流程分析之后，可結(jié)合各類屬性的約束，建立系統(tǒng)事件流程的UML 圖，然后使用iUML-B插件，轉(zhuǎn)化得到可擴充的驗證模型原型，以提高建模過程的自動化程度.初始模型是對系統(tǒng)進(jìn)行建模和驗證的起點，底層模型會影響整個模型結(jié)構(gòu)的簡潔性及后續(xù)精化的便捷程度.道口控制系統(tǒng)的核心功能是根據(jù)列車接近情況對道口欄門進(jìn)行控制，故初始模型僅設(shè)計了欄門的開啟與關(guān)閉過程.因此場景文件中的數(shù)據(jù)類型有（文件定義如圖3所示）：

門控命令（Controller_Order）集合：初始化（Null_C）、開啟（GoUp）、關(guān)閉（GoDown）；

欄門狀態(tài)（Gate_State）集合：初始化（Initia）、開啟中（Opening）、已開啟（Opened）、關(guān)閉中（Closing）、已關(guān)閉（Closed）；

初始模型的機器文件中包含4 個事件：欄門下降（GateGoDown）、欄門關(guān)閉（Gate_Close）、欄門打開（Gate_GoUp）、欄門開放（Gate_Open），且定義變量Gate_Information、Controller_Ctrl分別表示欄門、控制器的狀態(tài)變化.如圖4所示，建模中通過UML圖的形式直觀反映欄門的狀態(tài)變遷，并用此圖自動生成Event-B 語句.列出部分機器文件如圖5所示.

圖3 初始模型中的場景文件Fig.3 Context file in the initial model

圖4 初始模型中的UML 圖Fig.4 UML diagram in the initial model

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

2.2 精化策略

在初始模型得到實現(xiàn)且通過證明之后進(jìn)行精化，逐步添加與完善模型的系統(tǒng)功能，形成新的場景文件與機器文件，繼承已被證明的定理、不變式成果.精化策略降低了系統(tǒng)的建模難度，保證了各級底層模型的正確性.精化過程如表1所示，各層UML圖、文件見參考文獻(xiàn)[16].

表1 模型精化過程Tab.1 Refinement processes of the model

3 系統(tǒng)特性驗證

3.1 系統(tǒng)驗證特性的Event-B 描述

為體現(xiàn)系統(tǒng)運行過程中安全類屬性的重要性，將該屬性強制進(jìn)行特性驗證.以不變式（INV1～I(xiàn)NV7）表達(dá)待驗證的特性，即要讓這些屬性成立，則需保證對應(yīng)的不變式在執(zhí)行過程中始終保持為真.由于該系統(tǒng)的實時性要求非常高，因此同時對功能類屬性中的時間性約束進(jìn)行驗證.定義一個計時事件Tick_Tock表示系統(tǒng)時鐘，其它有時間特性的事件通過記錄各運行階段的系統(tǒng)當(dāng)前時間，表達(dá)出時間特性要求[17].對各條驗證特性進(jìn)行Event-B描述，如圖6所示.

圖6 基于特性的不變式驗證Fig.6 Property-based invariants verification

圖6中，列車當(dāng)前狀態(tài)變量Train_Information的取值有：接近（Approach）、逼近（Closing）、離去（Exit）；Time為系統(tǒng)當(dāng)前時間；Time_Approach_GateClosing為關(guān)閉道口時行人與車輛必需的出清時間；T_TrainApproach為列車發(fā)出接近信號的時刻；Time_Closing為門欄下降過程中的最大持續(xù)時間；T_ClosingStart為欄門下降命令下達(dá)時刻；T_TrainClose為列車發(fā)出逼近信號的時刻；Time_Closing_Coming為列車逼近至列車駛離道口過程中的最高持續(xù)時間T2；T_OpeningStart為開啟命令下達(dá)時刻；Time_Opening為欄門開啟過程中的最大持續(xù)時間.

INV1 體現(xiàn)了FUN3 的約束，以驗證列車接近信號發(fā)出后，在必要的出清理時間之內(nèi)，道口仍需要保持開放.

結(jié)合FUN2 與SAF1 的屬性需求，得出INV2，以驗證在列車接近信號發(fā)出后，經(jīng)過一定時間的行駛，列車發(fā)出逼近信號.這段時間包括道口出清時間與門欄關(guān)閉時間，即T1.

基于FUN3 的屬性需求，得出INV3，以驗證控制器發(fā)出欄門下降指令后，欄門應(yīng)在指定時間內(nèi)關(guān)閉.

INV4 表達(dá)出了FUN4 的屬性需求，以驗證在列車逼近信號發(fā)出后，經(jīng)過一定時間的行駛，列車通過道口.

基于SAF1 的屬性需求，得出INV5，以驗證當(dāng)列車逼近道口時，道口應(yīng)該關(guān)閉.

INV6 體現(xiàn)了SAF2 的屬性需求，以約束在列車駛離道口之后，道口才可開放，即欄門升起之前，需要判斷道口狀態(tài)，并同時得到欄門升起命令.

基于FUN5 的屬性需求，得出INV7，以驗證控制器發(fā)出欄門開啟指令后，欄門應(yīng)在指定時間內(nèi)開放.

規(guī)范中的環(huán)境類屬性全部定義在模型的Context文件中，功能類屬性在Machine 文件中描述成了各個事件，結(jié)合以上不變式對應(yīng)的安全屬性與時間特性要求，設(shè)計需求規(guī)范在模型中已經(jīng)得到了全部覆蓋.

3.2 證明義務(wù)的證明

在Rodin 中，不變式對事件會產(chǎn)生相應(yīng)的證明義務(wù)（proof obligations）.由于規(guī)范文本到邏輯事件的跨度非常大，在對系統(tǒng)進(jìn)行形式化描述時，難免會遺漏某些關(guān)鍵的約束信息.在對證明義務(wù)進(jìn)行證明時，這些建模缺陷會被顯現(xiàn)出來.證明義務(wù)的交互式修改證明過程對于開發(fā)者深入理解規(guī)范，完善規(guī)范屬性與模型至關(guān)重要.舉例如下：

（1）系統(tǒng)時鐘（Tick_Tock）是一個計數(shù)事件，需要添加有時間特性約束的響應(yīng)，作為時鐘計數(shù)的防衛(wèi)條件，如圖7中的guard1、guard2，以加強事件防衛(wèi)條件的完備性，從而確保INV1、INV4 產(chǎn)生的證明義務(wù)得以通過.

圖7 添加事件的防衛(wèi)條件Fig.7 Additional guards of event

（2）在列車逼近（Train_Close）事件中，需要增加防衛(wèi)條件：Gate_In formation=Closed，以保證INV6對應(yīng)產(chǎn)生的證明義務(wù)得以通過.

（3）在欄門開放（Gate_Open）事件中，需要增加防衛(wèi)條件：Train_In formation=Exit.雖然欄門打開（Gate_GoUp）事件中判斷了列車狀態(tài)（Train_Inforamtion），但由于在欄門開放（Gate_Open）事件中，欄門狀態(tài)Gate_Information要轉(zhuǎn)換成Opened，為了不與INV1 產(chǎn)生的證明義務(wù)相沖突，此處仍需要增加對列車狀態(tài)的檢查，以限定事件的狀態(tài)空間.

證明義務(wù)統(tǒng)計如圖8所示，圖中，C1～C4 表示模型中的各層場景文件，M1_Control_Gate～M4_Control_Gate_Train_Signalling_Time 表示模型中的各層機器文件.以第4 層的機器文件為例，共計生成57 條證明義務(wù)，其中自動證明通過52 條義務(wù)，結(jié)合人工修改完善模型證明5 條，所有證明義務(wù)全部證明通過.

圖8 精化過程中的證明義務(wù)統(tǒng)計Fig.8 Statistics of proof obligation in the refinement processes

4 道口控制系統(tǒng)的完善

在列車逼近（Train_Close）事件中，假設(shè)了列車可以獲取道口欄門狀態(tài).而目前的道口控制系統(tǒng)沒有這一功能，接近列車司機需要與道口管理員進(jìn)行語音通話確認(rèn)，無法做到實時性，且響應(yīng)過程較長，存在列車未知欄門狀態(tài)就已闖入道口的隱患.另外，根據(jù)研究過程中的事故調(diào)研分析，欄門關(guān)閉并不能等價于道口出清，現(xiàn)實中仍存在人車滯留在道口內(nèi)且欄門已經(jīng)閉關(guān)的可能性.

因此，安全屬性SAF1 不能滿足需求中列車安全通過道口的要求，也不能保證規(guī)范中的道口出清的要求，需要將其修改為：當(dāng)列車即將通過道口時，道口應(yīng)該關(guān)閉且道口出清；否則列車應(yīng)采取制動措施.可見圖2流程中缺少對道口異常狀態(tài)的處理，對應(yīng)管理規(guī)范中也缺少對異常狀態(tài)處理流程的明確界定，導(dǎo)致系統(tǒng)缺乏穩(wěn)健性（robustness）.在第四層模型中增加了對道口狀態(tài)的監(jiān)督及異常狀態(tài)處理，流程如圖9所示.

圖9 道口異常處理流程Fig.9 Exception-handling process of the railway level crossings

除添加道口狀態(tài)檢查、信息發(fā)送、道口狀態(tài)判斷、列車制動等事件外，增加了列車接近（Train_Approach）、列車逼近（Train_Close）事件的防衛(wèi)條件，添加了驗證特性INV8，以約束當(dāng)?shù)揽跔顩r異常時，應(yīng)發(fā)出警告信號，提示正在接近的列車進(jìn)行制動，如圖10所示.圖中，變量道口狀態(tài)Crossing_Infor的取值有：正常（Normal）、異常（Abnormal）；變量列車命令TrainOrder的取值有：制動（Normal）、繼續(xù)前行（KeepGoing）.

圖10 新增對應(yīng)的異常處理流程不變式驗證Fig.10 Additional invariants verification of exceptionhandling process

之后對模型不變式的沖突性與死鎖進(jìn)行了檢驗，全部通過驗證，該結(jié)果進(jìn)一步確認(rèn)了系統(tǒng)原型的正確性.可見，雖然在證明過程可以修正并減少需求分析與建模過程中的缺陷，但如果需求分析過程不完善，證明通過的模型也有可能包含缺陷.因此系統(tǒng)設(shè)計人員需要通過分析、建模與驗證過程，加深對系統(tǒng)設(shè)計需求及規(guī)范的理解，以提高模型的完備性與可靠性.本文相關(guān)的所有文件與模型可見參考文獻(xiàn)[16].

5 結(jié) 論

系統(tǒng)功能規(guī)范是系統(tǒng)設(shè)計實現(xiàn)的依據(jù)，任何潛在的規(guī)范缺陷或解讀錯誤都可能會給系統(tǒng)運營安全帶來巨大風(fēng)險.本文以道口管理規(guī)范為例，基于Event-B方法建立了道口控制系統(tǒng)的設(shè)計原型，并進(jìn)行了形式化驗證，得出主要結(jié)論如下：

（1）基于管理規(guī)范對系統(tǒng)屬性及事件流程的分類分析方法、通過UML 圖自動生成驗證模型文件的技術(shù)及精化建模的策略，有助于清晰、準(zhǔn)確地描述系統(tǒng)的特性，提高驗證模型的層次性；

（2）通過證明義務(wù)的交互式修改證明過程，可以幫助開發(fā)者深入理解規(guī)范，發(fā)現(xiàn)規(guī)范文本自身以及跨度到邏輯表達(dá)過程中，造成的假設(shè)、約束信息遺漏或錯誤，從而可以修改規(guī)范與建模缺陷，完善規(guī)范屬性在驗證模型的表達(dá)；

（3）研究得出目前規(guī)范中存在列車駛?cè)氲揽跁r不能確保系統(tǒng)安全狀態(tài)的缺陷.形式化建模與驗證方法有助于發(fā)現(xiàn)并糾正系統(tǒng)規(guī)范中潛在的設(shè)計漏洞，減少因規(guī)范理解不當(dāng)造成的建模缺陷，驗證后的模型可以作為系統(tǒng)設(shè)計原型，成為編碼階段工作的依據(jù)，且后續(xù)基于設(shè)計原型使用代碼生成技術(shù)可以提高編碼階段的自動化程度，以減少測試階段的成本投入.