基于時間自動機的列控系統等級轉換建模與驗證

董家希，劉珂帆，鄢春花，杜利芳，周家宇

（成都工業學院 汽車與交通學院，四川 成都）

引言

在列車運行過程中，需要十分嚴苛復雜的控制系統對于其安全穩定運行起到保障作用。等級轉換作為列控系統中的重要組成部分，每個環節的運作都必須得到嚴格的檢查和確認，方能順利推進。近年來，對于列控系統進行形式化建模，取得了豐碩的成果。其中，基于時間自動機原理的模型能夠將復雜抽象的列控系統等級轉換過程更加直觀、全面、清晰的呈現出來，因此在實時系統問題的研究中具備良好的表現[1]。

1 時間自動機模型

1.1 時間自動機理論

時間自動機(Timed Automata, TA)是一種面向實時系統進行建模和驗證分析的理論，為具有時間特征的系統的狀態轉換圖的描述提供了一種簡潔有效的方法[2]。

時間自動機系統將復雜的實時系統抽象為狀態和邊的轉換關系，并為其轉移條件提供了相應的時鐘約束，每個狀態改變都可以配合觸發啟動對應的時鐘計時模式，這個時鐘約束所對應的轉移條件在滿足時鐘約束的條件下才能夠執行。

時間約束的集合(X)的定義如下：

其中，X 表示時鐘變量，x 表示其中一個時鐘，時鐘解釋表示為時鐘集X 上的每一個時鐘賦予的一個實數值。

其中，T?R+，Tx為X 上所有時鐘解釋的集合。

在一個復雜的實時系統中，常常是由多個子系統構成的，他們之間相互獨立又彼此配合，頻繁進行子系統之間的信息交互，保證整個系統的協同合作，從而完成復雜實時系統對應的功能。因此我們可以用組成該系統的各個子系統的積來描述系統的功能，稱為時間自動機的積[3]。

設兩個時間自動機TA1=，TA2=，時鐘集合X1和X2不相交，則TA1和TA2的積記為TA1|| TA2。

1.2 UPPAAL 建模

UPPAAL 軟件采用圖形化的界面，主要由四個部分組成[4]。System Editor 是用于創建實時系統建模的工具。Simulator 是建模的初始步驟，它以圖形方式表示系統的邏輯關系。Verifier 則是實現系統功能仿真和時序仿真的關鍵工具。在設計階段Verifier 可以檢查所有可能的執行路徑，并在驗證之前對已有模型進行檢驗。Yggdrasil則用于測試用例的自動生成，可進行深度搜索，分析其測試用例覆蓋的運營場景，還可以根據所驗證性質進行測試用例的自動生成。UPPAAL 結構體系見圖1。

圖1 UPPAAL結構體系

TA 模型包括狀態、邊和約束條件三個元素。在TA模型中，兩個子系統之間的信息交互通過通道完成。UPPAAL 中所支持的BNF 語法主要有4 種表現方式[5]，其BNF 語句及含義見表1。

表1 BNF 語句及含義

2 等級轉換場景需求分析

2.1 等級轉換場景過程分析

當列車進行C2 到C3 等級轉換時，邊界上設置了應答器、轉換點以及司機確認區等，具體布置見圖2。

圖2 等級轉換邊界布置示意

2.2 建立等級轉換信息交互圖

將C2 至C3 列控系統等級轉換流程場景抽象描述為司機、應答器、車載設備和RBC 四個子系統之間的信息交互過程。它們通過傳輸包含不同指令的信息包來進行信息的傳遞。

對于根據需求規范歸納出來的C2 至C3 列控系統等級轉換流程的描述，繪制了C2 至C3 級列控系統等級轉換流程信息交互序列圖見圖3。

圖3 等級轉換流程信息交互序列圖

3 等級轉換場景建模與驗證

在構建模型時，我們將整個系統劃分為Train、Balise、RBC 和Driver 四個子系統，并分別構建這些子系統的UPPAAL 模型。

3.1 等級轉換場景建模

在等級轉換場景建模中，車載子系統是其中最復雜的部分。當列車通過等級轉換區域時，車載子系統根據列車實時狀態，頻繁地與應答器、RBC 以及司機界面進行信息傳遞，以確保等級轉換順利進行。等級轉換Train子系統模型見圖4。

應答器子系統作為車地信息交互的渠道，用于判斷列車位置，根據需求不同設置的相應功能的應答器，可以實現列車定位，為等級轉換提供位置信息。等級轉換Balise 子系統模型見圖5。

圖5 等級轉換Balise 子系統模型

RBC 根據收到信息生成控制命令，提供行車許可，保證列車運行安全性，模型見圖6。

圖6 等級轉換RBC 子系統模型

當接收到RBC 傳送的等級轉換命令后，車載設備就會向司機發送等級轉換確認請求，司機通過按壓按鈕對于等級轉換過程進行確認。這樣可以通過自動化操作和人工操作兩個方面來完整地驗證列控系統等級轉換的條件，實現雙保險。等級轉換Driver 子系統模型見圖7。

圖7 等級轉換Driver 子系統模型

3.2 等級轉換場景模型驗證

得到狀態轉移圖后，還需要運用UPPAAL 的驗證器對模型進行進一步的驗證，保證模型的正確性。利用形式化驗證的方法確保模型滿足系統的功能性需求和實時性需求，其流程見圖8。

圖8 基于UPPAAL的形式化驗證流程

功能性要求主要關注研究所建立的模型對于轉換流程的完整性。例如，確保系統能夠按照實際流程順利完成所需的步驟，防止系統出現死鎖，并確保執行操作能夠正常進行。同時，在設備正常運行的情況下，系統應能夠實現從C2 級到C3 級列控系統的等級轉換。當轉換條件不滿足時，系統應能夠保持C2 級列控系統的控車運行等。等級轉換功能性要求驗證運行結果見圖9。

圖9 等級轉換功能性要求驗證結果

實時性要求主要驗證系統的時間特性。等級轉換場景對時間的要求十分嚴格，因此，模型中狀態遷移的時間約束能否有效合理進行是模型建立成功與否的關鍵因素。等級轉換實時性要求驗證運行結果見圖10。

圖10 等級轉換實時性要求驗證結果

經過等級轉換過程中對每條性質的逐一驗證，得出的驗證結果發現每條性質均是可達的，說明系統可以滿足相應的性能和需求，證明所建立的時間自動機模型是安全可靠的。

4 結論

本文提出了一種基于模型對于復雜實時系統的研究方法，并對模型的準確性及完備性進行形式化驗證。首先，對于列控系統的等級轉換場景進行過程性分析和提取需求，梳理各子系統之間的信息交互流程。其次，基于時間自動機原理，借助UPPAAL 建模工具，建立四個子系統的狀態轉移圖模型。最后，對標列控系統規范要求，結合BNF 邏輯公式和系統驗證器，對于模型的實時性和功能性需求給出驗證，保證了此模型的準確性和可靠性。對于基于模型的研究問題具有一定的借鑒意義。