有色Petri網在平交道口安全性分析中的應用

孫 超，陳黎潔，宋鳳娟

（1.中國鐵道科學研究院集團有限公司 標準計量研究所，北京 100081；2.北京全路通信信號研究設計院集團有限公司，北京 100073）

隨著鐵路建設的發展以及道路交通工具數量的增長，平交道口（LC，Level crossing）存在很大的安全隱患[1]。平交道口一旦發生交通事故，不僅中斷鐵路運輸，阻塞道路交通，還會引起嚴重的人員傷亡和財產損失[2]。形式化方法可以通過具有明確數學定義的文法和語義方法或語言對LC的期望特性和行為進行精確、簡潔描述，得到其數學模型，通過計算方式對模型性質進行分析和驗證，能夠發現LC存在的風險，提高其安全性[3-4]。

相對于其他形式化語言，有色Petri網具有直觀的圖形表示和嚴密的數學基礎，在描述系統的分叉、同步和并行等行為、層次化建模及處理數據方面具有很大優勢[5]，因為基于模型的分析方法能夠直觀體現系統的行為[6]。同時，有色Petri網支撐時序邏輯語言ASK-CTL的運行，ASK-CTL時序邏輯是一種形式化語言，其主要作用是進行計算的邏輯推理，通過時序連接詞將時間建立成一系列“狀態”序列，通過搜索模型中是否具有用ASK-CTL描述的狀態來驗證模型代表的系統是否符合需求[7]。文章用有色Petri網分析平交道口的安全性：（1）運用有色Petri網工具對平交道口建立模型；（2）用ASK-CTL語言表示平交道口的安全需求；（3）通過模型檢驗的方法進行功能驗證。

1 有色Petri網方法

有色Petri網是在Petri網的基礎上加上模塊化的功能，使模型能夠分成不同的模塊，降低了每個模塊中模型的復雜程度，其相關的變量參數定義如下：

（1）元素的類型用Type表示，變量v的類型用Type(v)表示；

（2）變量集合V的綁定，即每個變量v∈V與一個具體元素b(v)∈Type(v)相關聯，元素b(v)是屬于Type(v)類型的。

1.1 有色Petri網語法

1.2 ASK-CTL語法

ASK-CTL公式由路徑量詞、時態運算符和性質描述符3部分構成。路徑量詞包括A（對于所有路徑）、E（存在某個路徑）；時態運算符包括 G（Global）、F（Future）、X（next）、U（Until）；性質描述符用來描述系統模型的性質或狀態，可以用a、b表示。

1.3 ASK-CTL語義

用S表示狀態，那么有

S|=EFb==>存在從狀態S出發的路徑滿足Si|=b,i≥0

S|=AFb==>對所有從狀態S出發的路徑滿足Si|=b,i≥0

S|=EGb==>存在從狀態S出發的路徑滿足ASi|=b,i≥0

S|=AGb==>對所有從狀態S出發的路徑滿足ASi|=b, i≥0

2 平交道口結構

本文選用單條軌道和雙向道路組成的平交道口作為分析對象，包含道路警報燈、護欄、信號機、傳感器、控制單元，如圖1所示[8-9]。

平交道口系統的工作流程為[10]：（1）當列車接近道口傳感器檢測到有列車接近平交道口時，傳感器將列車接近信息發送給控制單元；（2）控制單元向道路警報燈和護欄發出控制命令，道路警報燈閃爍，護欄落下，護欄向控制單元反饋護欄落下信息；（3）控制單元給軌旁信號機發送綠燈命令，將信號燈從紅色轉換為綠色，如果信號機未收到控制單元的綠燈命令，信號燈需保持紅色。如果列車接近，但信號燈仍然為紅色，列車必須停在信號機前。當列車到達平交道口并且被列車出清傳感器檢測到后，列車出清傳感器向控制單元反饋列車已出清信息；（4）控制單元向信號機發送紅燈命令，將信號燈置為紅色，同時向道路警報燈發送熄滅命令，向護欄發送抬升命令。

圖1 平交道口結構

3 平交道口有色Petri網模型

基于有色Petri網的模塊化功能，可以將平交道口的模型分為：軌道交通系統模型、道口控制系統模型和道路交通系統模型。CPN Tools是典型的有色Petri網建模工具，本文使用CPN Tools建立相關模型。

3.1 軌道交通系統有色Petri網模型

圖2是平交道口的軌道交通系統模型。這里考慮客運和貨運兩種列車類型，變遷“Passenger train”和變遷“Freight train”的觸發分別代表兩種車型的選擇。參考經驗數據，客運列車出現的概率為0.8，貨運列車出現的概率為0.2，庫所“Train Approaching LC”中包含1到10之間隨機分布的變量，用令牌E表示，當變量大于2時，表明以0.8的概率觸發變遷“Passenger train”。同理，變量不大于2時，表明以0.2的概率觸發變遷“Freight train”。

3.2 道口控制系統有色Petri網模型

道口控制系統的工作流程為：檢測到有列車接近平交道口時，道路警報燈閃爍4 s，然后信號燈變成紅色，護欄落下。直到檢測到列車已出清平交道口，信號燈由紅色變成綠色，同時護欄升起。道口控制系統具備“關閉”和“開啟”兩種狀態，一旦信號燈為紅色，平交道口對道路交通系統就是關閉的，同理，一旦列車出清平交道口并且信號燈變成綠色以后護欄完全升起，平交道口對道路交通系統就是開啟的。

圖2 軌道交通系統模型

圖3表示道口控制系統的模型。初始情況下，平交道口對道路交通系統是開啟的，這用庫所“LCOpenToRoadTraffic”中包含一個令牌來表示。變遷“close”的觸發代表信號燈變成紅色并且護欄落下，其符號@+4代表該動作有4 s的延時，即列車接近平交道口時道路警報燈閃爍4 s以后。庫所“LCCloseToRoadTraffic”代表平交道口處于關閉狀態，庫所“open”代表因為信號燈變成綠色并且護欄升起，平交道口重新開啟。

圖3 道口控制系統模型

3.3 道路交通系統有色Petri網模型

在平交道口的出清區道路交通存在擁堵和無擁堵兩種情況，而存在擁堵時，道路交通存在安全導向和風險導向兩種情況，因此，道路交通系統的模型可以進一步劃分為無擁堵時的道路交通系統模型、汽車駛入平交道口模型、有擁堵時道路交通系統的風險導向模型、有擁堵時道路交通系統的安全導向模型，如圖4所示。表1總結了圖4中各變遷代表的含義。

表1 道路交通系統模型中各變遷的含義

3.3.1 無擁堵時道路交通系統模型

無擁堵時的道路交通系統模型如圖4a所示。庫所“VehicleApproachingLC”表示在汽車靠近平交道口的出清區沒有交通擁堵。用M（“”）表示庫所中存在的令牌數量，無交通擁堵情況下，出清區最多只能同時存在兩輛汽車，那么M（“VehiclesInCZ”）+ M（“AnotherVehiclesInCZ”）= M（“VehiclesStillInCZ”）+ M（“AnotherVehiclesStillInCZ”）= 1,即 庫 所“VehiclesInCZ”和庫所“AnotherVehiclesInCZ”中的令牌總數為1，同理，庫所“VehiclesStillInCZ”和庫所“AnotherVehiclesStillInCZ”中的令牌總數也為1。兩輛汽車依次通過道口區的場景可以由庫所“VehiclesInCZ”、庫所“VehiclesStillInCZ”，以及變遷“Entry to CZ without jam”、變遷“begin exit”、變遷“leave CZ and enter EZ”共同描述。變遷“Entry to CZ without jam”表示汽車進入道口區，變遷“begin exit”表示開始離開道口區，變遷“leave CZ and enter EZ”表示完全離開道口區并進入出清區。

圖4a中模型從變遷“leave CZ and enter EZ”開始往下的部分表示出清區的汽車的行為。庫所“RemainingCapacity”表示出清區汽車的最大容量，本文假設出清區汽車的最大容量為3，庫所“Counter”表示出清區剩余的汽車數量，那么有M（“Counter”）+ M（“Vehicle1RemainEZ”）+ M（“Vehicle2RemainEZ”）+ M（“Vehicle3RemainEZ”）= 3。庫所“Counter”中的令牌數量到達3，變遷“Entry to CZ without jam”不能再觸發，表示出清區汽車數量一旦到達其最大容量，汽車不再進入道口區。因此，一旦變遷“Entry to CZ without jam”觸發，表明平交道口的汽車不會引起擁堵。

3.3.2 汽車駛入平交道口模型

汽車駛入平交道口的模型如圖4b所示。變遷“Vehicle at entry under traffic jam situation”觸發的條件之一是圖4a模型中庫所“RemainingCapacity”的令牌數為3，即出清區汽車數量到達最大容量，發生擁堵。此時可能發生兩種情況：（1）汽車繼續駛入道口區，觸發圖4c中模型的變遷“risk”；（2）汽車等在平交道口的入口直到出清區的汽車離開，觸發圖4d中模型的變遷“safe”。

3.3.3 有擁堵時道路交通系統風險導向模型

有擁堵時道路交通系統的風險導向模型如圖4c所示。此時出清區已經發生擁堵，汽車繼續駛入道口區是存在一定風險的。變遷“risk”的觸發表明汽車駛入道口區。

3.3.4 有擁堵時道路交通系統安全導向模型

有擁堵時道路交通系統的風險導向模型如圖4d所示。變遷“Safe entry to CZ”的觸發條件之一是庫所“Counter”中的令牌數小于3，即只要出清區的汽車數量不小于3，就沒有汽車駛入道口區。

圖4 道路交通系統模型

3.4 整體模型

有色Petri網能夠通過模塊化的方法根據平交道口的功能將其模型分解成不同的模塊，為了體現各模塊之間的關聯性，本節描述圖4各模型之間的關系。

3.4.1 軌道交通系統和道口控制系統之間的關聯

一旦檢測到列車接近平交道口，平交道口對道路交通系統關閉，該狀態用圖2模型中的庫所“LCCloseToRoad”表示，同理，一旦列車離開道口區，平交道口對道路系統開啟，該狀態用圖2模型中的庫所“LCReopenToTrafficFlow”表示。這兩個庫所是圖3中模型的變遷“close”和變遷“open”的觸發條件。

3.4.2 道口控制系統和道路交通系統之間的關聯

道口控制系統的任務是允許或禁止汽車通過平交道口，因此圖4a模型中的變遷“Entry to CZ without jam”、圖4b中模型的變遷“Vehicle at entry under traffic jam situation”、圖4c中模型的變遷“Risky entry to CZ”、圖4d中模型的變遷“Safe entry to CZ”的觸發條件之一是圖3中模型的庫所“LCCloseToRoadTraffic”沒有令牌。

4 平交道口模型分析與驗證

模型檢驗是關于系統屬性驗證的算法和方法，基本思想是用狀態遷移系統列舉系統存在的所有狀態，用時序邏輯公式描述系統的目標狀態，通過狀態空間查詢的方法查找列舉的系統狀態中是否存在符合目標的狀態。CPN Tools除了能夠建立模型，還為時序邏輯公式ASK-CTL的運行提供了環境，本章使用CPN Tools對平交道口的模型進行檢驗。

4.1 安全性分析算法

系統安全性的定義為：系統不期望的狀態永遠不會發生，對應到模型中則是通過所有路徑都能達到安全的狀態。本文平交道口的安全性分析算法如表2所示。

表2 安全性分析算法

4.2 安全性分析過程及結果

根據表2的算法，表3給出了對平交道口安全性分析的過程及結果。

4.3 到達非安全狀態的路徑查找

從分析結果看出不是所有路徑都能到達安全狀態，即代表汽車的令牌可能不在道路交通系統安全導向模型中，存在非安全狀態，那么就要查找到達非安全狀態的路徑。查找到達非安全狀態路徑的算法及路徑如表4所示。

表3 平交道口安全性分析結果

表4 到達非安全狀態的路徑查找算法及路徑

從到達非安全狀態的路徑中可以看出，是因為道路交通系統風險導向模型中變遷“risk”的觸發導致代表汽車的令牌未進入道路交通系統安全導向模型中，引起了非安全狀態的出現。這是因為在平交道口的出清區汽車數量已經達到最大容量時，汽車司機可能會等到出清區的汽車數量減少時再駛入平交道口，也可能會直接駛入平交道口。

5 結束語

鐵路的建設發展進入一個全新的階段，無論是列車的速度、密度還是列車的載重都比以前有了極大的提高，與此同時，公路運輸量也在不斷提高，道路交通工具數量大幅增長。這樣的交通現狀加上有待提高的人口素質，導致平交道口存在很大的安全隱患。因此，平交道口的安全性是當前交通運輸行業亟需重視的問題。

本文將有色Petri網用于平交道口的安全分析中，相對于已往對平交道口安全性分析方法上研究的不足，該方法不僅能夠描述平交道口的功能特征和動態行為，還能夠對功能進行驗證。利用有色Petri網對平交道口進行了形式化描述，針對平交道口中的軌道交通系統、道口控制系統和道路交通系統進行了建模，最后應用有色Petri網環境下的模型檢驗工具ASK-CTL進行了功能驗證，驗證結論表明了平交道口模型功能的正確性以及方法的可行性。