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

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

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

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

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

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

1 列車自動停站場景

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

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

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

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

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

2 基于Petri網的運營場景建模與分析

2.1 Petri網基本要素及運行規則

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

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

2.2 模型建立

對全自動無人駕駛系統運營場景進行Petri網建模的流程如下。

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

Step 2在分析系統運營場景的基礎上進行對象狀態集辨識，提取出場景中的參與對象，將運營場景分成若干順序子場景，分析各子場景中參與對象的狀態變化及時序邏輯。

Step 3根據所提取對象的狀態集和事件確定Petri網中對應庫所和變遷的物理含義，嚴格定義其模型語義，根據事件時序邏輯選擇相應的基本結構，建立對應運營場景的Petri網模型。

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

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

根據各參與對象狀態與庫所的對應關系、觸發事件與變遷的對應關系，以及列車停站場景流程邏輯時序，基于開源Petri網建模軟件PIPE［10］，建立的全自動無人駕駛列車停站場景Petri網模型見圖2。

圖2 全自動無人駕駛列車停站場景Petri網模型

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

表3 Petri網元素、符號及物理含義

2.3 模型分析

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

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

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

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

3 模型驗證與優化

本文應用Petri網建模軟件PIPE對所建模型進行驗證，并考慮場景中可能出現的異常情況，對模型進行優化。

3.1 模型驗證

評價Petri網的可用性指標一般包括可達性、有界性、安全性及活性。

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

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

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

圖4 Petri網模型狀態空間可達圖

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

圖5 模型不變量分析結果

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

圖6 模型狀態空間分析結果

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

3.2 模型優化

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

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

圖7 優化后的列車停站場景Petri網模型

4 結束語

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