基于車車通信的列控系統移動授權功能建模與驗證

陳 燕

（福州職業技術學院交通工程系，福建 福州 350000）

1 基于車車通信的移動授權功能

1.1 基于車車通信的列控系統

列控系統，即列車控制系統，是保證列車安全、高效、舒適運行的關鍵系統之一。基于車車通信的列控系統主要實現動車組與動車組之間的直接信息傳輸，包括速度、位置、列車識別等，正因為如此，列車可直接進行移動授權計算而無需軌旁設備計算后轉發，避免了傳統列控系統中需要通過軌旁設備實現信息傳輸的局限性，提高了信息傳輸的效率和可靠性[1]。車車通信列控系統還可以實現動車組之間的協同控制，提高列車的運行效率和安全性。同時，由于移動授權計算功能由車載設備完成，地面設備得到簡化，系統復雜度和運維成本降低[2]。

1.2 移動授權生成功能

移動授權（Mobile Authority，MA）是列車運行的前提，它決定了列車的限速及終點信息。傳統列控系統的移動授權計算由軌旁區域控制器ZC 來完成，一個ZC 管轄范圍內可能存在多輛列車同時運行，一旦故障，將導致大量列車延誤[3]。而基于車車通信的列控系統中移動授權的計算以車載移動授權模塊為主，以智能列車監控系統、對象控制器等其他子系統為輔來完成計算[4]。移動授權的目標點可能是信號機、道岔等靜態障礙物，也可能是前方運行車輛等動態障礙物，同時計算過程還需考慮線路條件以及臨時限速信息，所以列車需要與地面設備通信獲取這些靜態障礙物、線路條件等信息，同時還要不斷與前行列車進行通信獲取動態障礙物信息。

2 形式化建模

2.1 形式化建模理論

形式化建模理論是一種數學建模方法，用于描述和模擬現實世界中的各種現象和過程。它基于數學符號系統，使用形式化語言來描述模型，并使用計算機程序來驗證模型的正確性和可靠性。形式化建模理論的主要目的是提供一種精確、一致和可靠的方式來描述和模擬現實世界中的系統，協助排查系統中可能存在的漏洞，提升系統運行的穩定性。

形式化建模理論包括三個主要組成部分：模型、解釋和驗證。模型描述系統或過程的本質特征和行為。解釋模型并回答模型所描述的問題。驗證檢查模型的正確性和可靠性。

列控系統是對于安全性能有著近乎苛刻的要求，車車通信的應用提升了車載設備的復雜度，原有模塊在功能和信息交互上也有了變化，以前車車尾為終點的移動授權計算模式需要高頻次的進行實時移動授權計算以保證列車運行效率和安全性能，針對基于車車通信列控系統的實時性、連續性的特點，選擇有色Petri 網理論為基礎，遵循分層建模的原則建立模型。

2.2 有色Petri 網理論

有色Petri 網理論在普通Petri 網的庫所和變遷的基礎上，引入了顏色（有色）的概念，用于描述和研究復雜系統的動態行為。庫所的顏色表示系統的屬性，變遷的顏色表示系統可以執行的操作。有色Petri網理論的優勢在于它可以更準確地描述具有多個屬性的系統，包括系統的演化、系統的穩定性、系統的控制等問題。

CPN Tools 工具是針對Petri 進行模型設計、功能驗證的工具，可實現模型的可視化，提供系統的可達性、有界性、活性、回歸性和公平性的狀態空間分析報告，發現模型中的漏洞，從而改進完善模型。

3 移動授權計算模型的驗證分析

3.1 車載移動授權生成流程

列車運行前，先根據預先下載的電子地圖規劃運行路徑，然后與對象控制器通信，遍歷目標路徑上的虛擬信號及道岔信息，若信號開放、道岔位置正確、路徑范圍無站臺、并且已識別出唯一前車并建立通信，那么列車就以前車車尾為終點障礙物，否則就以不符條件的設備為終點障礙物[5]。接下來以本車車尾為起點，再結合線路的臨時限速信息計算移動授權。在運行過程中還需不斷與智能列車監控系統、對象控制器以及前車進行通信，獲取線路條件、道岔位置、前車運行狀態等信息，不斷計算新的移動授權，保證列車運行在最優的狀態[6]。

3.2 頂層模型建立

根據車載移動授權生成流程建立其頂層模型如圖1 所示，該模型包含靜態障礙物信息處理（Static）和動態障礙物信息處理（Dynamic）2 個變遷，包含車載移動授權模塊（V_MA）、靜態障礙物判斷結果（Static_Result）、終點為靜態障礙物的MA（S_MA）和終點為動態障礙物的MA（D_MA）共4 個庫所，用STRING定義顏色集info。

圖1 移動授權計算頂層模型圖

3.3 子模型建立

根據終點障礙物類型可將模型分為靜態障礙物處理模型和動態障礙物處理模型。

靜態障礙物處理模型用來模擬列車運行路徑終點為靜態障礙物的情況，其處理模型如圖2 所示，總共包括從對象控制器獲取路徑上的靜態障礙物信息（Static）、判斷路徑上的虛擬信號狀態（XH_State）、判斷道岔狀態（DC_State）等3 個變遷，包括開始計算移動授權（V_MA）、判斷信號狀態（XH_Judge）、信號判斷結果（XH_Result）、判斷道岔位置（DC_Positon）、判斷道岔狀態（DC_Judge）、靜態障礙物判斷結果（Static_Result）等6 個庫所。

圖2 靜態障礙物處理模型

列車開始計算移動授權時，首先通過對象控制器遍歷路徑上的虛擬信號狀態，并將結果存放在Signal中，如果信號未開放，那么列車就以虛擬信號位置為終點計算移動授權，如果信號開放，則繼續遍歷道岔狀態，如果道岔位置正確，再根據前車位置計算移動授權，如果道岔位置不正確且無法轉換，則以道岔位置為終點生成移動授權，最終將最新的移動授權存放在Static_Result 中。

動態障礙物處理模型用來模擬列車運行路徑終點為唯一前行列車的情況，其處理模型如圖3 所示，總共包括從對象控制器獲取路徑上的動態障礙物信息（Train_State）等2 個變遷，包括通過靜態障礙物處理模型計算得到的靜態障礙物判斷結果（Static_Result）、根據靜態障礙物生成的移動授權（S_MA）、繼續進行其他信息的判定（Msg_Judge）、前車信息（V_Ahead）、移動授權計算結果（D_MA）等6 個庫所。

圖3 動態障礙物處理模型

如果規劃路徑上存在未開放的信號或者位置不正確且無法轉換的道岔，則以S_MA 中存放的靜態障礙物信息為終點生成移動授權，如果信號和道岔位置均滿足條件，則以唯一前車位置為終點計算移動授權，如果不存在前車，則以列車運行目標為終點生成移動授權。

3.4 移動授權計算模型驗證與分析

3.4.1 模型邏輯功能驗證

根據圖1 的移動授權計算模型圖，庫所VOMA為其初始狀態，當托肯為1`（“MA”）時，列車開始計算進入移動授權計算流程。可能出現虛擬信號未開放、道岔位置不正確等情況，此時應以未開放信號或者錯誤位置道岔為終點計算靜態移動授權（Dev_MA），列車在運行過程中可能存在沒有前車的情況，此時應以列車運行目標位置為終點計算移動授權，進而由車載ATP 生成位置速度曲線控制列車安全運行。如表1 所示，功能正常與功能特殊情況都可實現。

表1 移動授權模塊功能驗證

3.4.2 模型狀態空間分析

由圖4（a）為移動授權生成模型部分狀態空間報告，可以看到State Space 與Scc Graph 中的節點和弧的數量一致，系統所有節點可達。

圖4 移動授權生成模型報告

圖4（b）為移動授權生成模型系統有界性報告，可以看到模型中僅存在1 個Upper 和Lower 均為0的庫所，這是因為該庫所存放由靜態障礙物生成的移動授權，模型中默認初始狀態是虛擬信號機都開放，道岔位置正確且鎖閉，因此出現這種情況，整個系統模型有界。

圖4（c）為移動授權生成模型性質報告，可以看到 Dead Transition Instances、Live Transition Instances、Fairness Properties 都為None，表示沒有重復的流程，滿足公平性的要求。通知可以看到Dead markings 顯示節點6 為死節點，因為節點6 是模型的最后一個節點，所以符合實際情況，模型具有活性。

4 結語

采用有色Petri 理論對基于車車通信的移動授權計算流程，根據分層建模的思想，建立了移動授權計算的Petri 模型，并完成了模型的空間、有界性及性質報告，得出了該模型滿足可達性、有界性、公平性、活性的要求，該模型在基于車車通信的列控系統中合理且有效，實現系統功能并能滿足系統的安全性需求。