孫 超，陳黎潔，宋鳳娟

（1.中國(guó)鐵道科學(xué)研究院集團(tuán)有限公司 標(biāo)準(zhǔn)計(jì)量研究所，北京 100081；2.北京全路通信信號(hào)研究設(shè)計(jì)院集團(tuán)有限公司，北京 100073）

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

相對(duì)于其他形式化語(yǔ)言，有色Petri網(wǎng)具有直觀的圖形表示和嚴(yán)密的數(shù)學(xué)基礎(chǔ)，在描述系統(tǒng)的分叉、同步和并行等行為、層次化建模及處理數(shù)據(jù)方面具有很大優(yōu)勢(shì)[5]，因?yàn)榛谀Ｐ偷姆治龇椒軌蛑庇^體現(xiàn)系統(tǒng)的行為[6]。同時(shí)，有色Petri網(wǎng)支撐時(shí)序邏輯語(yǔ)言ASK-CTL的運(yùn)行，ASK-CTL時(shí)序邏輯是一種形式化語(yǔ)言，其主要作用是進(jìn)行計(jì)算的邏輯推理，通過(guò)時(shí)序連接詞將時(shí)間建立成一系列“狀態(tài)”序列，通過(guò)搜索模型中是否具有用ASK-CTL描述的狀態(tài)來(lái)驗(yàn)證模型代表的系統(tǒng)是否符合需求[7]。文章用有色Petri網(wǎng)分析平交道口的安全性：（1）運(yùn)用有色Petri網(wǎng)工具對(duì)平交道口建立模型；（2）用ASK-CTL語(yǔ)言表示平交道口的安全需求；（3）通過(guò)模型檢驗(yàn)的方法進(jìn)行功能驗(yàn)證。

1 有色Petri網(wǎng)方法

有色Petri網(wǎng)是在Petri網(wǎng)的基礎(chǔ)上加上模塊化的功能，使模型能夠分成不同的模塊，降低了每個(gè)模塊中模型的復(fù)雜程度，其相關(guān)的變量參數(shù)定義如下：

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

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

1.1 有色Petri網(wǎng)語(yǔ)法

1.2 ASK-CTL語(yǔ)法

ASK-CTL公式由路徑量詞、時(shí)態(tài)運(yùn)算符和性質(zhì)描述符3部分構(gòu)成。路徑量詞包括A（對(duì)于所有路徑）、E（存在某個(gè)路徑）；時(shí)態(tài)運(yùn)算符包括 G（Global）、F（Future）、X（next）、U（Until）；性質(zhì)描述符用來(lái)描述系統(tǒng)模型的性質(zhì)或狀態(tài)，可以用a、b表示。

1.3 ASK-CTL語(yǔ)義

用S表示狀態(tài)，那么有

S|=EFb==>存在從狀態(tài)S出發(fā)的路徑滿足Si|=b,i≥0

S|=AFb==>對(duì)所有從狀態(tài)S出發(fā)的路徑滿足Si|=b,i≥0

S|=EGb==>存在從狀態(tài)S出發(fā)的路徑滿足ASi|=b,i≥0

S|=AGb==>對(duì)所有從狀態(tài)S出發(fā)的路徑滿足ASi|=b, i≥0

2 平交道口結(jié)構(gòu)

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

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

圖1 平交道口結(jié)構(gòu)

3 平交道口有色Petri網(wǎng)模型

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

3.1 軌道交通系統(tǒng)有色Petri網(wǎng)模型

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

3.2 道口控制系統(tǒng)有色Petri網(wǎng)模型

道口控制系統(tǒng)的工作流程為：檢測(cè)到有列車接近平交道口時(shí)，道路警報(bào)燈閃爍4 s，然后信號(hào)燈變成紅色，護(hù)欄落下。直到檢測(cè)到列車已出清平交道口，信號(hào)燈由紅色變成綠色，同時(shí)護(hù)欄升起。道口控制系統(tǒng)具備“關(guān)閉”和“開(kāi)啟”兩種狀態(tài)，一旦信號(hào)燈為紅色，平交道口對(duì)道路交通系統(tǒng)就是關(guān)閉的，同理，一旦列車出清平交道口并且信號(hào)燈變成綠色以后護(hù)欄完全升起，平交道口對(duì)道路交通系統(tǒng)就是開(kāi)啟的。

圖2 軌道交通系統(tǒng)模型

圖3表示道口控制系統(tǒng)的模型。初始情況下，平交道口對(duì)道路交通系統(tǒng)是開(kāi)啟的，這用庫(kù)所“LCOpenToRoadTraffic”中包含一個(gè)令牌來(lái)表示。變遷“close”的觸發(fā)代表信號(hào)燈變成紅色并且護(hù)欄落下，其符號(hào)@+4代表該動(dòng)作有4 s的延時(shí)，即列車接近平交道口時(shí)道路警報(bào)燈閃爍4 s以后。庫(kù)所“LCCloseToRoadTraffic”代表平交道口處于關(guān)閉狀態(tài)，庫(kù)所“open”代表因?yàn)樾盘?hào)燈變成綠色并且護(hù)欄升起，平交道口重新開(kāi)啟。

圖3 道口控制系統(tǒng)模型

3.3 道路交通系統(tǒng)有色Petri網(wǎng)模型

在平交道口的出清區(qū)道路交通存在擁堵和無(wú)擁堵兩種情況，而存在擁堵時(shí)，道路交通存在安全導(dǎo)向和風(fēng)險(xiǎn)導(dǎo)向兩種情況，因此，道路交通系統(tǒng)的模型可以進(jìn)一步劃分為無(wú)擁堵時(shí)的道路交通系統(tǒng)模型、汽車駛?cè)肫浇坏揽谀Ｐ汀⒂袚矶聲r(shí)道路交通系統(tǒng)的風(fēng)險(xiǎn)導(dǎo)向模型、有擁堵時(shí)道路交通系統(tǒng)的安全導(dǎo)向模型，如圖4所示。表1總結(jié)了圖4中各變遷代表的含義。

表1 道路交通系統(tǒng)模型中各變遷的含義

3.3.1 無(wú)擁堵時(shí)道路交通系統(tǒng)模型

無(wú)擁堵時(shí)的道路交通系統(tǒng)模型如圖4a所示。庫(kù)所“VehicleApproachingLC”表示在汽車靠近平交道口的出清區(qū)沒(méi)有交通擁堵。用M（“”）表示庫(kù)所中存在的令牌數(shù)量，無(wú)交通擁堵情況下，出清區(qū)最多只能同時(shí)存在兩輛汽車，那么M（“VehiclesInCZ”）+ M（“AnotherVehiclesInCZ”）= M（“VehiclesStillInCZ”）+ M（“AnotherVehiclesStillInCZ”）= 1,即 庫(kù) 所“VehiclesInCZ”和庫(kù)所“AnotherVehiclesInCZ”中的令牌總數(shù)為1，同理，庫(kù)所“VehiclesStillInCZ”和庫(kù)所“AnotherVehiclesStillInCZ”中的令牌總數(shù)也為1。兩輛汽車依次通過(guò)道口區(qū)的場(chǎng)景可以由庫(kù)所“VehiclesInCZ”、庫(kù)所“VehiclesStillInCZ”，以及變遷“Entry to CZ without jam”、變遷“begin exit”、變遷“l(fā)eave CZ and enter EZ”共同描述。變遷“Entry to CZ without jam”表示汽車進(jìn)入道口區(qū)，變遷“begin exit”表示開(kāi)始離開(kāi)道口區(qū)，變遷“l(fā)eave CZ and enter EZ”表示完全離開(kāi)道口區(qū)并進(jìn)入出清區(qū)。

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

3.3.2 汽車駛?cè)肫浇坏揽谀Ｐ?/p>

汽車駛?cè)肫浇坏揽诘哪Ｐ腿鐖D4b所示。變遷“Vehicle at entry under traffic jam situation”觸發(fā)的條件之一是圖4a模型中庫(kù)所“RemainingCapacity”的令牌數(shù)為3，即出清區(qū)汽車數(shù)量到達(dá)最大容量，發(fā)生擁堵。此時(shí)可能發(fā)生兩種情況：（1）汽車?yán)^續(xù)駛?cè)氲揽趨^(qū)，觸發(fā)圖4c中模型的變遷“risk”；（2）汽車等在平交道口的入口直到出清區(qū)的汽車離開(kāi)，觸發(fā)圖4d中模型的變遷“safe”。

3.3.3 有擁堵時(shí)道路交通系統(tǒng)風(fēng)險(xiǎn)導(dǎo)向模型

有擁堵時(shí)道路交通系統(tǒng)的風(fēng)險(xiǎn)導(dǎo)向模型如圖4c所示。此時(shí)出清區(qū)已經(jīng)發(fā)生擁堵，汽車?yán)^續(xù)駛?cè)氲揽趨^(qū)是存在一定風(fēng)險(xiǎn)的。變遷“risk”的觸發(fā)表明汽車駛?cè)氲揽趨^(qū)。

3.3.4 有擁堵時(shí)道路交通系統(tǒng)安全導(dǎo)向模型

有擁堵時(shí)道路交通系統(tǒng)的風(fēng)險(xiǎn)導(dǎo)向模型如圖4d所示。變遷“Safe entry to CZ”的觸發(fā)條件之一是庫(kù)所“Counter”中的令牌數(shù)小于3，即只要出清區(qū)的汽車數(shù)量不小于3，就沒(méi)有汽車駛?cè)氲揽趨^(qū)。

圖4 道路交通系統(tǒng)模型

3.4 整體模型

有色Petri網(wǎng)能夠通過(guò)模塊化的方法根據(jù)平交道口的功能將其模型分解成不同的模塊，為了體現(xiàn)各模塊之間的關(guān)聯(lián)性，本節(jié)描述圖4各模型之間的關(guān)系。

3.4.1 軌道交通系統(tǒng)和道口控制系統(tǒng)之間的關(guān)聯(lián)

一旦檢測(cè)到列車接近平交道口，平交道口對(duì)道路交通系統(tǒng)關(guān)閉，該狀態(tài)用圖2模型中的庫(kù)所“LCCloseToRoad”表示，同理，一旦列車離開(kāi)道口區(qū)，平交道口對(duì)道路系統(tǒng)開(kāi)啟，該狀態(tài)用圖2模型中的庫(kù)所“LCReopenToTrafficFlow”表示。這兩個(gè)庫(kù)所是圖3中模型的變遷“close”和變遷“open”的觸發(fā)條件。

3.4.2 道口控制系統(tǒng)和道路交通系統(tǒng)之間的關(guān)聯(lián)

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

4 平交道口模型分析與驗(yàn)證

模型檢驗(yàn)是關(guān)于系統(tǒng)屬性驗(yàn)證的算法和方法，基本思想是用狀態(tài)遷移系統(tǒng)列舉系統(tǒng)存在的所有狀態(tài)，用時(shí)序邏輯公式描述系統(tǒng)的目標(biāo)狀態(tài)，通過(guò)狀態(tài)空間查詢的方法查找列舉的系統(tǒng)狀態(tài)中是否存在符合目標(biāo)的狀態(tài)。CPN Tools除了能夠建立模型，還為時(shí)序邏輯公式ASK-CTL的運(yùn)行提供了環(huán)境，本章使用CPN Tools對(duì)平交道口的模型進(jìn)行檢驗(yàn)。

4.1 安全性分析算法

系統(tǒng)安全性的定義為：系統(tǒng)不期望的狀態(tài)永遠(yuǎn)不會(huì)發(fā)生，對(duì)應(yīng)到模型中則是通過(guò)所有路徑都能達(dá)到安全的狀態(tài)。本文平交道口的安全性分析算法如表2所示。

表2 安全性分析算法

4.2 安全性分析過(guò)程及結(jié)果

根據(jù)表2的算法，表3給出了對(duì)平交道口安全性分析的過(guò)程及結(jié)果。

4.3 到達(dá)非安全狀態(tài)的路徑查找

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

表3 平交道口安全性分析結(jié)果

表4 到達(dá)非安全狀態(tài)的路徑查找算法及路徑

從到達(dá)非安全狀態(tài)的路徑中可以看出，是因?yàn)榈缆方煌ㄏ到y(tǒng)風(fēng)險(xiǎn)導(dǎo)向模型中變遷“risk”的觸發(fā)導(dǎo)致代表汽車的令牌未進(jìn)入道路交通系統(tǒng)安全導(dǎo)向模型中，引起了非安全狀態(tài)的出現(xiàn)。這是因?yàn)樵谄浇坏揽诘某銮鍏^(qū)汽車數(shù)量已經(jīng)達(dá)到最大容量時(shí)，汽車司機(jī)可能會(huì)等到出清區(qū)的汽車數(shù)量減少時(shí)再駛?cè)肫浇坏揽?，也可能?huì)直接駛?cè)肫浇坏揽凇?/p>

5 結(jié)束語(yǔ)

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

本文將有色Petri網(wǎng)用于平交道口的安全分析中，相對(duì)于已往對(duì)平交道口安全性分析方法上研究的不足，該方法不僅能夠描述平交道口的功能特征和動(dòng)態(tài)行為，還能夠?qū)δ苓M(jìn)行驗(yàn)證。利用有色Petri網(wǎng)對(duì)平交道口進(jìn)行了形式化描述，針對(duì)平交道口中的軌道交通系統(tǒng)、道口控制系統(tǒng)和道路交通系統(tǒng)進(jìn)行了建模，最后應(yīng)用有色Petri網(wǎng)環(huán)境下的模型檢驗(yàn)工具ASK-CTL進(jìn)行了功能驗(yàn)證，驗(yàn)證結(jié)論表明了平交道口模型功能的正確性以及方法的可行性。