基于形式化方法的道口控制系統規范建模與驗證

王恪銘 ，王 崢

（1.西南交通大學信息科學與技術學院，四川 成都 611756；2.西南交通大學系統可信性自動驗證國家地方聯合工程實驗室，四川 成都 610031）

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

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

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

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

1 功能規范分析

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

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

對道口控制系統的驗證需要確認系統在通用標準及管理規范的約束下能否正確運行.首先需要深入解讀道口規范的文本內容，析取各個功能事件的邏輯流程，分析得出系統的環境屬性、功能屬性、安全屬性，構建好形式化描述的對象.

1.1 事件流程

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

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

1.2 屬性提取

分析道口設計規范，將其中的屬性要求分為環境類、功能類和安全類共3 類.環境類屬性（ENV）用于描述系統中建模對象的性質，功能屬性（FUN）描述系統應當具備的基本功能，安全類屬性（SAF）描述系統在運行過程中應具備的安全條件.

提取出環境類屬性如下：

ENV1：道口門欄的狀態包括升起中、開啟、下降中、關閉.

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

ENV3：列車在道口附近的狀態包括到達接近點A、到達逼近點C、離去.

ENV4：道口信號燈的狀態包括紅燈、紅閃、白燈.

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

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

FUN1：控制器通過升起、下降命令控制欄門的狀態轉換：開啟→下降中→關閉→升起中→開啟.

FUN2：列車到達接近點A、到達逼近點C及離開道口時，應給出相應信號.

FUN3：列車到達接近點A時，發出接近信號，道口信號燈轉變成紅燈并進行道口出清作業，之后欄門下降，道口關閉.

FUN4：列車到達逼近點C時，發出逼近信號，道口信號燈紅閃，列車經過T2時間后將通過道口.

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

安全類屬性有：

SAF1：當列車即將通過道口時，道口應該關閉.

SAF2：當列車離去時，道口才可重新開放.

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

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

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

2.1 初始模型

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

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

欄門狀態（Gate_State）集合：初始化（Initia）、開啟中（Opening）、已開啟（Opened）、關閉中（Closing）、已關閉（Closed）；

初始模型的機器文件中包含4 個事件：欄門下降（GateGoDown）、欄門關閉（Gate_Close）、欄門打開（Gate_GoUp）、欄門開放（Gate_Open），且定義變量Gate_Information、Controller_Ctrl分別表示欄門、控制器的狀態變化.如圖4所示，建模中通過UML圖的形式直觀反映欄門的狀態變遷，并用此圖自動生成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 精化策略

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

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

3 系統特性驗證

3.1 系統驗證特性的Event-B 描述

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

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

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

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

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

基于FUN3 的屬性需求，得出INV3，以驗證控制器發出欄門下降指令后，欄門應在指定時間內關閉.

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

基于SAF1 的屬性需求，得出INV5，以驗證當列車逼近道口時，道口應該關閉.

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

基于FUN5 的屬性需求，得出INV7，以驗證控制器發出欄門開啟指令后，欄門應在指定時間內開放.

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

3.2 證明義務的證明

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

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

圖7 添加事件的防衛條件Fig.7 Additional guards of event

（2）在列車逼近（Train_Close）事件中，需要增加防衛條件：Gate_In formation=Closed，以保證INV6對應產生的證明義務得以通過.

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

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

圖8 精化過程中的證明義務統計Fig.8 Statistics of proof obligation in the refinement processes

4 道口控制系統的完善

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

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

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

除添加道口狀態檢查、信息發送、道口狀態判斷、列車制動等事件外，增加了列車接近（Train_Approach）、列車逼近（Train_Close）事件的防衛條件，添加了驗證特性INV8，以約束當道口狀況異常時，應發出警告信號，提示正在接近的列車進行制動，如圖10所示.圖中，變量道口狀態Crossing_Infor的取值有：正常（Normal）、異常（Abnormal）；變量列車命令TrainOrder的取值有：制動（Normal）、繼續前行（KeepGoing）.

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

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

5 結 論

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

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

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

（3）研究得出目前規范中存在列車駛入道口時不能確保系統安全狀態的缺陷.形式化建模與驗證方法有助于發現并糾正系統規范中潛在的設計漏洞，減少因規范理解不當造成的建模缺陷，驗證后的模型可以作為系統設計原型，成為編碼階段工作的依據，且后續基于設計原型使用代碼生成技術可以提高編碼階段的自動化程度，以減少測試階段的成本投入.