基于Petri網(wǎng)的全自動無人駕駛列車停站場景形式化建模與驗證

王瑋琦，任晨宇，陳黎潔，侯卓璞

按照國際通行定義，城市軌道交通自動化等級（Grade of Automation，GoA）劃分為5個等級：GoA0～GoA4級。其中，最高等級GoA4級代表了技術(shù)發(fā)展的趨勢，被定義為全自動無人駕駛系統(tǒng)（Unattended Train Operation，UTO）。UTO系統(tǒng)運行時無需司機(jī)和乘務(wù)員參與，在控制中心的統(tǒng)一調(diào)度下實現(xiàn)列車喚醒和休眠、載客運行、洗車及出入停車場等全場景、全過程自動控制，有充分的設(shè)備冗余配置和完善的安全防護(hù)機(jī)制［1］，已成為未來軌道交通發(fā)展的必然趨勢。

全自動無人駕駛系統(tǒng)中，由自動控制系統(tǒng)替代司機(jī)和乘務(wù)員操作，降低了由于人為失誤導(dǎo)致發(fā)生事故的可能性，但是系統(tǒng)組件信息交互頻繁、時序特征復(fù)雜等特點也帶來新的安全風(fēng)險。一般先由生產(chǎn)廠家對全自動無人駕駛系統(tǒng)進(jìn)行安全驗證，在實驗室的仿真環(huán)境下測試相關(guān)功能，再在新建項目中進(jìn)行現(xiàn)場系統(tǒng)場景測試。然而，這種方式通常無法檢測出各個專業(yè)接口之間的潛在問題，在實際運營過程中才能發(fā)現(xiàn)一些具體問題［2］。因此，在全生命周期早期對系統(tǒng)中運營場景的實現(xiàn)流程進(jìn)行建模與驗證分析，對于全自動無人駕駛系統(tǒng)的項目實施和安全應(yīng)用至關(guān)重要。

作為一種基于數(shù)學(xué)和邏輯的系統(tǒng)化方法，形式化方法被廣泛應(yīng)用到軌道交通系統(tǒng)的建模與驗證研究中。文獻(xiàn)［3］采用STPA（系統(tǒng)理論過程分析方法）對全自動無人駕駛系統(tǒng)中的自動洗車功能進(jìn)行安全分析，辨識不安全控制行為并提出風(fēng)險規(guī)避措施。文獻(xiàn)［4］采用形式化建模工具UPPAAL對LKJ-15系統(tǒng)的模式轉(zhuǎn)換功能進(jìn)行建模并驗證其安全性。文獻(xiàn)［5］采用安全狀態(tài)機(jī)對自主化ATP的等級轉(zhuǎn)換功能進(jìn)行建模，并利用HAZOP（危險和可操作性分析）方法對其進(jìn)行安全驗證。

Petri網(wǎng)是由Carl Adam Petri提出的一種基于狀態(tài)的形式化建模方法，具有嚴(yán)格的數(shù)學(xué)定義和直觀的圖形表達(dá)，可以清晰地描述系統(tǒng)狀態(tài)的動態(tài)演變過程，被廣泛應(yīng)用于計算機(jī)和系統(tǒng)工程的建模與仿真驗證領(lǐng)域。文獻(xiàn)［6］基于觀察、定位、決策、行動（Observation、Orientation、Decision、Action，OODA）環(huán)理論分析無人多平臺作戰(zhàn)指揮流程，采用Petri網(wǎng)工具對OODA指揮控制進(jìn)行建模與驗證。文獻(xiàn)［7］基于城市軌道交通車載ATP子系統(tǒng)建立Petri網(wǎng)故障模型，并進(jìn)行危險源辨識與故障診斷。文獻(xiàn)［8］針對地鐵車輛子系統(tǒng)建立Petri網(wǎng)模型，研究其在運營過程中可能發(fā)生的安全事故。全自動無人駕駛系統(tǒng)的運營場景是在系統(tǒng)設(shè)計階段分析系統(tǒng)安全關(guān)鍵功能建立的應(yīng)用實例，Perri網(wǎng)在系統(tǒng)靜態(tài)結(jié)構(gòu)和動態(tài)行為的建模分析方面具有優(yōu)勢，因此本文以一個典型的全自動無人駕駛系統(tǒng)運營場景——列車自動停站場景為研究對象，利用Petri網(wǎng)理論對其進(jìn)行建模與驗證，為系統(tǒng)開發(fā)及安全分析提供理論支撐。

1 列車自動停站場景

列車自動停站屬于正線運營場景，是全自動無人駕駛系統(tǒng)的關(guān)鍵運營場景之一。全自動無人駕駛系統(tǒng)的運營場景與傳統(tǒng)CBTC系統(tǒng)的不同之處在于：傳統(tǒng)CBTC系統(tǒng)中，列車停站過程中由駕駛員或站務(wù)人員確認(rèn)車門是否滿足關(guān)閉條件，列車客室車門的開啟/關(guān)閉由駕駛員通過按下開門或關(guān)門按鈕執(zhí)行；全自動無人駕駛系統(tǒng)沒有司機(jī)的參與，完全依賴系統(tǒng)實現(xiàn)該功能。

列車進(jìn)站場景結(jié)束之后進(jìn)入列車停站場景，當(dāng)列車進(jìn)站對標(biāo)停車后，停站倒計時開始。此時站臺上的乘客處于站臺門之外等候上車，車內(nèi)乘客在車門處等候下車。車載控制器（Vehicle On-board Controller，VOBC）生成允許開門指令并向車輛發(fā)送門控命令，車門控制單元執(zhí)行開門命令開啟車門并將車門開啟狀態(tài)信息反饋給VOBC。與此同時，VOBC向計算機(jī)聯(lián)鎖（Computer Interlocking，CI）發(fā)送允許開門指令，CI將開門指令發(fā)送給站臺門系統(tǒng)，站臺門門控單元解鎖并開啟站臺門，CI將站臺門狀態(tài)信息反饋給VOBC。當(dāng)車門和站臺門分別開啟后，乘客開始上下車。站臺門與客室車門的障礙物檢測裝置開始工作，并將站臺門與車門狀態(tài)實時反饋給VOBC。在時刻表規(guī)定的停站時間結(jié)束時，且站臺門與車門處無異常狀態(tài)，VOBC即生成關(guān)門指令，車門和站臺門關(guān)閉過程與前文所述開門指令的傳輸流程一致。當(dāng)VOBC收到車門和站臺門關(guān)閉且鎖閉、列車與站臺門間無異物的狀態(tài)反饋信息后，允許列車啟動出發(fā)［9］。至此列車停站場景結(jié)束，進(jìn)入列車離站場景。全自動無人駕駛系統(tǒng)列車停站運營場景事件順序見圖1。

圖1 全自動無人駕駛系統(tǒng)列車停站場景事件順序

由圖1可知，全自動無人駕駛系統(tǒng)中的列車停站運營場景由以下子場景按順序組成：列車進(jìn)站停車、開啟車門與站臺門、乘客上下車、關(guān)閉車門與站臺門、列車啟動離站。各子場景中涉及對象主要包括VOBC、CI、列車客室車門、站臺門和乘客，各對象的狀態(tài)隨著子場景的改變而發(fā)生變化，各子場景中各對象的狀態(tài)見表1。

表1 列車停站場景各參與對象在不同階段的狀態(tài)

2 基于Petri網(wǎng)的運營場景建模與分析

2.1 Petri網(wǎng)基本要素及運行規(guī)則

經(jīng)典Petri網(wǎng)是一個由節(jié)點和連接弧所組成的有向二分圖。一個Petri網(wǎng)結(jié)構(gòu)由4個基本元素組成：庫所（place）、變遷（transition）、有向?。╝rc）和令牌（token）。其中，庫所和變遷是Petri網(wǎng)的2個節(jié)點類型，庫所表示被建模的系統(tǒng)狀態(tài)，變遷表示在系統(tǒng)中發(fā)生的事件；有向弧連接庫所和變遷，表示兩者之間的順序關(guān)系，2個同類型的節(jié)點之間不能連接；令牌是分布在庫所中的動態(tài)對象，可以從一個庫所轉(zhuǎn)移到另一個庫所，根據(jù)觸發(fā)規(guī)則轉(zhuǎn)移，代表系統(tǒng)狀態(tài)的演化，反映系統(tǒng)運行的全部過程。

在Petri網(wǎng)中，變遷的使能（enabling）表示該變遷代表的事件，在滿足前提條件時發(fā)生。用變遷的輸入庫所（由指向變遷的弧所連接的庫所）表示該事件發(fā)生所需要的前提局部狀態(tài)，如果一個變遷的每個輸入庫所都擁有令牌，則該變遷即為被允許（enabled）。一個變遷被允許時，該變遷將被觸發(fā)（fire）。

2.2 模型建立

對全自動無人駕駛系統(tǒng)運營場景進(jìn)行Petri網(wǎng)建模的流程如下。

Step 1清晰刻畫需要建模的運營場景，即確定場景中事件發(fā)生的時序邏輯及狀態(tài)變化。

Step 2在分析系統(tǒng)運營場景的基礎(chǔ)上進(jìn)行對象狀態(tài)集辨識，提取出場景中的參與對象，將運營場景分成若干順序子場景，分析各子場景中參與對象的狀態(tài)變化及時序邏輯。

Step 3根據(jù)所提取對象的狀態(tài)集和事件確定Petri網(wǎng)中對應(yīng)庫所和變遷的物理含義，嚴(yán)格定義其模型語義，根據(jù)事件時序邏輯選擇相應(yīng)的基本結(jié)構(gòu)，建立對應(yīng)運營場景的Petri網(wǎng)模型。

在對列車自動停站場景建模時，利用庫所表示列車停站過程中各參與對象在不同階段的狀態(tài)；利用變遷表示列車停站過程中觸發(fā)不同狀態(tài)的事件；利用有向弧連接庫所和變遷來表示狀態(tài)時序及事件觸發(fā)邏輯順序。根據(jù)場景描述分析設(shè)計Petri模型的庫所集合P為P=｛P0，P1，P2，…，P14｝，變遷集合T為T=｛T0，T1，T2，…，T10｝。列車停站場景Petri網(wǎng)模型中庫所集和變遷集標(biāo)識及對應(yīng)含義見表2。

表2 列車停站場景各庫所、變遷的編號及對應(yīng)含義

根據(jù)各參與對象狀態(tài)與庫所的對應(yīng)關(guān)系、觸發(fā)事件與變遷的對應(yīng)關(guān)系，以及列車停站場景流程邏輯時序，基于開源Petri網(wǎng)建模軟件PIPE［10］，建立的全自動無人駕駛列車停站場景Petri網(wǎng)模型見圖2。

圖2 全自動無人駕駛列車停站場景Petri網(wǎng)模型

圖2中，元素、符號及物理含義見表3；有向弧上的數(shù)字為權(quán)重，每條弧的權(quán)重相同，為默認(rèn)值1［11］；庫所P0、P1、P2、P3分別為列車從進(jìn)站、站臺停車、準(zhǔn)備出站到啟動離站這一過程的狀態(tài)變化；變遷T0、T1分別為列車對標(biāo)停車后停站計時開始和停站計時結(jié)束2個事件；車門控制子場景發(fā)生在列車停站過程中，從列車對標(biāo)停車后開始，到列車停站計時結(jié)束后車門與站臺門關(guān)閉為止，中間伴隨著乘客上下車子場景，當(dāng)車門與站臺門均關(guān)閉后，列車啟動離站，并在區(qū)間運行直至接近下一車站，這2個事件分別為變遷T2和T3。

表3 Petri網(wǎng)元素、符號及物理含義

2.3 模型分析

由圖2可知，當(dāng)列車處于停車狀態(tài)時，進(jìn)入車門控制子場景，車載設(shè)備分別發(fā)送客室車門和站臺門開門指令，分別由庫所P4和P5表示。此處采用Petri網(wǎng)基本結(jié)構(gòu)中的并發(fā)結(jié)構(gòu)，即庫所P0擁有令牌，通過T0觸發(fā)后，P4和P5都擁有了令牌，描述車門與站臺門開啟的并發(fā)過程，同時庫所P1獲得令牌，列車處于停站狀態(tài)?？褪臆囬T和站臺門的開門動作分別由變遷T4和T5表示，此時客室車門與站臺門處于開啟狀態(tài)，分別由庫所P6和P7表示。當(dāng)車門與站臺門都處于開啟狀態(tài)時，乘客開始上下車。變遷T6為車廂里和站臺上的乘客開始向車門處移動，此處采用Petri網(wǎng)基本結(jié)構(gòu)中的同步結(jié)構(gòu)，即只有當(dāng)庫所P6和P7都具有令牌時，變遷T6才能被觸發(fā)。庫所P8、P9、P10為站臺門和車門開啟后乘客上下車子場景中的3個狀態(tài)，即車門開啟后的乘客狀態(tài)、乘客乘降狀態(tài)和上下車過程結(jié)束后的乘客狀態(tài)。

為了更清晰地將乘客上下車過程中的庫所與變遷關(guān)聯(lián)起來，將乘客上車與下車動作轉(zhuǎn)換為上下車乘客進(jìn)入門之間與離開門之間的2種動作，分別由變遷T6和T7表示，描述乘客上下車過程的庫所與變遷示意見圖3。此處采用Petri網(wǎng)基本結(jié)構(gòu)中的順序結(jié)構(gòu)，即變遷T6觸發(fā)后，庫所P8擁有令牌，按乘客上下車時序邏輯觸發(fā)變遷T7，使庫所P9擁有令牌并保持，直到車門與站臺門關(guān)閉。列車停站時間結(jié)束時，觸發(fā)變遷T1，此時車載設(shè)備發(fā)送車門和站臺門關(guān)閉指令，分別由庫所P11和P12表示，此處采取的結(jié)構(gòu)與車門開啟過程相同，即變遷T1觸發(fā)后，庫所P11、P12、P2同時擁有令牌。客室車門及站臺門關(guān)閉動作由變遷T9與T10表示，車門與站臺門關(guān)閉后的狀態(tài)由庫所P13和P14表示。庫所P9、P13、P14同時獲得令牌后，變遷T8被觸發(fā)，即乘客停止上下車動作，庫所P10獲得令牌，表示上下車場景結(jié)束后的乘客狀態(tài)。當(dāng)庫所P2、P10同時擁有令牌后，變遷T2被觸發(fā)，即當(dāng)車門與站臺門關(guān)閉后，乘客結(jié)束上下車，允許列車啟動離站。庫所P3獲得令牌表示列車出站狀態(tài)，觸發(fā)變遷T3后，庫所P0重新獲得令牌，開始新一輪的列車停站場景。

圖3 乘客上下車場景庫所與變遷示意

綜上，列車自動停站場景Petri網(wǎng)模型由順序、并發(fā)和同步3種基本結(jié)構(gòu)組成。其中，順序結(jié)構(gòu)描述列車停站、列車運行、乘客上下車和車門控制等子場景；同步結(jié)構(gòu)描述變遷的觸發(fā)條件，例如車門和站臺門都開啟后乘客才可以上下車，車門與站臺門關(guān)閉后意味著乘客停止上下車；并發(fā)結(jié)構(gòu)描述場景狀態(tài)的并發(fā)特點，例如停站倒計時開始后車載設(shè)備同時發(fā)送客室車門和站臺門開門指令，同時列車處于停站狀態(tài)；列車啟動后，停站場景結(jié)束，列車在區(qū)間運行并接近站臺，進(jìn)入下一個停站場景。

3 模型驗證與優(yōu)化

本文應(yīng)用Petri網(wǎng)建模軟件PIPE對所建模型進(jìn)行驗證，并考慮場景中可能出現(xiàn)的異常情況，對模型進(jìn)行優(yōu)化。

3.1 模型驗證

評價Petri網(wǎng)的可用性指標(biāo)一般包括可達(dá)性、有界性、安全性及活性。

定義一個庫所集P，p∈P在一個Petri網(wǎng)的每一個庫所p中令牌數(shù)量不超過一個有限正整數(shù)k，庫所與其所包含的令牌數(shù)的映射函數(shù)為M（p）。當(dāng)M（p）≤k，則判定該庫所是有界的，k為該庫所的界。當(dāng)k=1時，則稱該庫所是安全的。如果Petri網(wǎng)中每個庫所都有界，則該Petri網(wǎng)有界，當(dāng)Petri網(wǎng)的界為1時，則稱該Petri網(wǎng)是安全的［12］。

定義一個變遷集T，對于Petri網(wǎng)中的任意變遷t?T，若存在某個變遷序列覆蓋該變遷，即該變遷是被允許的，則稱該變遷是活的。若一個Petri網(wǎng)所有變遷是活的，則該Petri網(wǎng)具有活性，與之相反的現(xiàn)象則稱為死鎖。

首先，利用PIPE軟件中的可達(dá)圖模塊自動生成上述Petri模型狀態(tài)空間可達(dá)圖，見圖4。圖4中，節(jié)點S為模型的可達(dá)標(biāo)識集，即系統(tǒng)從初始狀態(tài)經(jīng)過一系列變遷的觸發(fā)和令牌的轉(zhuǎn)移達(dá)到最終狀態(tài)的全部狀態(tài)集合?？蛇_(dá)標(biāo)識由具有令牌的庫所構(gòu)成，初始標(biāo)識S0=｛P0｝，終止標(biāo)識S32=｛P3｝?？蛇_(dá)標(biāo)識之間由帶約束的有向弧連接，約束為觸發(fā)的變遷，例如初始標(biāo)識S0經(jīng)過變遷T0到達(dá)標(biāo)識S1。模型覆蓋所有變遷，不存在死鎖，因此所建模型具有活性。從圖4可以看出，系統(tǒng)模型在不同子場景中至少存在1條可達(dá)路徑，保證能夠成功執(zhí)行模型中的各項功能，模型從起始節(jié)點到終止節(jié)點存在可達(dá)路徑，因此所建Petri網(wǎng)模型具有可達(dá)性。

圖4 Petri網(wǎng)模型狀態(tài)空間可達(dá)圖

其次，利用PIPE軟件不變量分析模塊（Invariant Analysis）得出所建模型的變遷不變量（T-invariants）、庫所不變量（P-invariants）及不變量方程。模型不變量分析結(jié)果見圖5。由圖5可見，所建Petri網(wǎng)中有1個變遷不變量和5個庫所不變量。對于變遷不變量，分析模塊給出的結(jié)論是：該網(wǎng)絡(luò)被確定的T-invariants覆蓋，因此它可能是有界和活的。對于庫所不變量，分析模塊給出的結(jié)論是：該網(wǎng)絡(luò)被確定的P-invariants覆蓋，因此它是有界的。

圖5 模型不變量分析結(jié)果

根據(jù)Petri網(wǎng)中的5個庫所不變量，仿真模塊給出對應(yīng)的5個庫所不變量方程。圖5中｛M（Px），x=0，1，2，…，14｝為庫所與其所包含的令牌數(shù)的映射函數(shù)。由庫所不變量方程可知，Petri網(wǎng)的界為1，根據(jù)Petri網(wǎng)的有界性和安全性定義可知，所建Petri網(wǎng)是有界和安全的。圖6所示的由PIPE軟件狀態(tài)分析模塊（State Space Analysis）得出的結(jié)論為模型有界、安全、無死鎖，同時也驗證了上述分析結(jié)果。

圖6 模型狀態(tài)空間分析結(jié)果

綜上，由仿真驗證和狀態(tài)空間分析結(jié)果可知，根據(jù)場景需求和對象狀態(tài)辨識所建立的全自動無人駕駛系統(tǒng)列車停站運營場景Petri網(wǎng)模型具有可達(dá)性、活性、安全性和有界性，驗證了所建模型的有效性和可用性。

3.2 模型優(yōu)化

上述模型只考慮了各設(shè)備正常運行時的狀態(tài)轉(zhuǎn)換，未考慮異常情況的處理與建模分析。在城軌車門控制系統(tǒng)中，原則上要求車門和站臺門同時開啟或關(guān)閉。當(dāng)處于交通高峰期時，車站內(nèi)乘客較多，開門時，若車門早于站臺門開啟，或關(guān)門時，站臺門早于車門關(guān)閉，乘客在上下車過程中，就可能因為擁擠而處于站臺門與車門的縫隙中，存在安全隱患。本文針對這類異常情況對上述列車停站模型進(jìn)行優(yōu)化。

由于站臺門和車門的開門響應(yīng)時間不同，在實際運行中，目前通過設(shè)定車門與站臺門延時時間差來確保車門不應(yīng)比站臺門先開啟，站臺門不應(yīng)比車門先關(guān)閉［13］。根據(jù)該思想，優(yōu)化后的模型見圖7。本模型中不考慮設(shè)定站臺門與車門延時時間差，僅考慮開關(guān)時序邏輯。為了避免出現(xiàn)車門比站臺門先開啟或站臺門比車門先關(guān)閉的異常情況，本模型中引入庫所P15和P16，利用Petri網(wǎng)的并發(fā)與同步結(jié)構(gòu)優(yōu)化車門與站臺門的開關(guān)時序。在變遷T4和T5之間加入庫所P15，表示站臺門打開且車門關(guān)閉的瞬時狀態(tài)，P4和P5同時擁有令牌后，T5先被觸發(fā)，P15和P7獲得令牌，只有當(dāng)P15和P4同時擁有令牌時，T4才被觸發(fā)，實現(xiàn)變遷T5的觸發(fā)優(yōu)先權(quán)。同理在變遷T9和T10之間加入庫所P16，表示車門關(guān)閉且站臺門打開的瞬時狀態(tài)，實現(xiàn)變遷T9的觸發(fā)優(yōu)先權(quán)。利用PIPE軟件中的狀態(tài)空間分析模塊對優(yōu)化后的模型分析可得，該模型有界、安全、無死鎖。

圖7 優(yōu)化后的列車停站場景Petri網(wǎng)模型

4 結(jié)束語

通過分析全自動無人駕駛系統(tǒng)列車停站運營場景，基于Petri網(wǎng)理論定義了場景狀態(tài)的時序和事件觸發(fā)的邏輯順序與庫所集、變遷集的對應(yīng)關(guān)系，建立了列車停站場景的Petri網(wǎng)模型；利用仿真軟件分析與驗證了所建模型的有效性及可用性，并針對可能出現(xiàn)的車門/站臺門開關(guān)時序異常情況對模型進(jìn)行優(yōu)化。后續(xù)研究可利用有色Petri網(wǎng)、時間Petri網(wǎng)等高級Petri網(wǎng)理論對該模型進(jìn)行擴(kuò)展，并對其他運營場景建模并驗證，為全自動無人駕駛系統(tǒng)的安全分析和應(yīng)用提供理論支撐。