高速鐵路CTC分界口臨時限速系統建模與驗證

趙榮亮，王長林

(西南交通大學 信息科學與技術學院，成都 610031)

臨時限速系統是高速鐵路列車控制（簡稱：列控）系統的重要組成部分，臨時限速的設置直接關系到列車的運行效率和運行安全。臨時限速分為突發限速和有計劃情況下的限速，僅在某段線路上一定的時間范圍內有效，其工作流程即擬定、設置、執行、取消等具有嚴格的時間約束特性，是典型的實時系統。根據列車的實際運行情況，臨時限速區段可能設置在調度集中系統調度臺分界處，此時，臨時限速系統與相鄰的調度臺之間都有信息交互，表現出的交互特性更加復雜。

形式化方法以數學為基礎，運用嚴格的方法和語義對系統特性或行為進行精確描述[1]，根據描述模型，可以最大限度地驗證系統的正確性。時間自動機是對自動機理論的擴展，不僅可用來描述系統的時間特性，還能很好的描述系統的交互特性。基于時間自動機理論的驗證工具UPPAAL為用戶提供了良好的建模仿真界面，并且能夠自動對系統的屬性進行驗證。

本文基于時間自動機理論，應用UPPAAL建模驗證工具，對CTC分界口臨時限速的工作流程及信息交互過程進行仿真建模，并對系統的安全性和受限活性進行驗證。

1 CTC分界口臨時限速場景分析

臨時限速系統的基本構成如圖1所示。

圖1 臨時限速系統構成

臨時限速的設置應滿足運輸安全，并要求靈活設置。當調度集中系統（CTC，Certralized Traffic Command System）分界口處由于施工、維修或自然災害等原因需要設置臨時限速時，臨時限速系統不僅要完成自身臨時限速的設置，還要與相鄰調度臺臨時限速設備之間進行信息交互。臨時限速在CTC分界口處的場景如圖2所示。

圖2 CTC分界口處臨時限速場景

其中，左側調度臺命名為A,右側調度臺命名為B，對應設備均通過在其后面加上相應的字母來區分。根據站場圖，標示出相鄰調度臺臨時限速命令的擬定范圍和限速數據的覆蓋區域，并標示出邊界TCC/RBC的單向臨時限速數據覆蓋區域（圖中范圍均為示意圖）。

根據圖2中的方向所示，臨時限速命令的擬定責任方遵循“以線路正方向，限速起點所在局”的歸屬原則。圖2中限速區1由CTC-A負責擬定，限速區2由CTC-B負責擬定，限速區1與限速區2均在兩側TSRS數據覆蓋范圍內，因此，TSRS-A數據覆蓋區內限速區1的限速信息要發送給TSRS-B，同時，TSRS-B臨時限速數據覆蓋區內限速區2的數據也要發送給TSRS-A，使雙方的限速命令同步，這樣才能形成正式的臨時限速命令。當出現通信中斷或其它原因照成命令狀態不一致，各TSRS請求刷新，進行命令狀態同步，同步原則以命令發起方為準。若同步失敗，則判斷為故障，跨界臨時限速設置不成功。各TSRS根據雙方的限速結果，生成最終的限速命令。

本論文主要對分界口臨時限速的擬定校驗、驗證、執行流程進行建模，由于臨時限速的取消流程與執行流程類似，不再詳細分析其工作過程。

1.1 分界口臨時限速命令擬定

調度臺CTC-A施工調度員負責提出跨界臨時限速命令的申請，與相鄰的調度臺CTC-B聯系確認后，擬定正式限速調度命令，下發給對應的TSRS-A進行有效性驗證，并將驗證結果傳遞給相鄰的TSRS-B，請求CTC-B的TSR校驗，綜合兩側的校驗結果，形成文本形式臨時限速調度命令，送至行調臺CTC-A、CTC-B，調度員確認后存入TSRS。

1.2 分界口臨時限速命令激活驗證

臨時限速服務器TSRS-A實時檢查存儲的臨時限速調度命令開始執行的時間，在計劃開始執行前30 min向原擬定方提示激活存儲的相應臨時限速命令，并且每間隔10 min提示一次，直到確認或超出命令結束時間。TSRS-A激活提示檢驗通過后請求TSRS-B激活提示并檢驗（除時間信息處，其它條件均滿足即可）。激活成功后由TSRS-A下達驗證，并分發給相關TCC/RBC進行驗證，同時請求TSRS-B分發并進行驗證。

1.3 分界口臨時限速命令執行

臨時限速服務器TSRS-A設置提示成功，請求TSRS-B設置提示，TSRS-A綜合設置提示結果，提示調度員下達執行。TSRS-A分發限速命令至相關的TCC/RBC及TSRS-B執行，TSRS-A在請求鄰站執行結果的同時，告知本地執行的中間結果，綜合執行的結果并送行調臺顯示。

2 系統建模仿真

2.1 時間自動機

時間自動機使用時鐘變量表示時間，用一個約束條件來注釋狀態轉換圖，這個與時間有關的約束條件決定了狀態轉換的發生時機[2]。對于一個時鐘變量的有窮集合X，時鐘約束的集合φ(X)的形式語法為：φ：x≤c|c≤x|x

時間自動機A是一個六元組（∑, S, S0, X, I,E），其中：∑ 是一個有窮標記集合，S是一個有限狀態集合， S0∈S是開始狀態集合，X是一個有限時鐘集合，I是一個映射，為每個位置s指定φ(X)中的一些時鐘約束，E?S×∑×2X×φ(X)×S是轉換集合，一個轉換（s, s', a, λ, φ)表示在符號a下從位置s到位置s'的一條邊，φ是X上的一個時鐘約束，指定什么時候轉換發生，集合λ?X指這次轉換中被復位的時鐘。時間自動機的語義由一個與它相關的狀態轉換SA來定義，SA的一個狀態是一個偶對（s, v），s是A的一個位置，v是X的一個時鐘約束[3]。

2.2 基于時間自動機模型

根據分界口臨時限速系統的工作流程，利用UPPAAL建模仿真工具建立時間自動機模型。分界口臨時限速信息交互通過4個活動對象來完成，即CTC-A、TSRS-A、TSRS-B 、CTC-B，構造出每個對象的時間自動機模型，通過自動機網絡描述整個系統。構造出時間自動機依次記作 TACTC–A、TATSRS–A、TATSRS–B、TACTC–B，如圖3所示。

圖3 時間自動機模型

圖3中，各位置之間通過同步通道實現轉換的同步發生，其中，“！”結尾的標記表示發出此信號時轉換發生，“？”結尾的標記表示接收到此信號時轉換發生[4]。標有 C 的圓圈為堅定位置[5]，可以凍結時間即下一個轉換必須無延遲的離開。規定模型中位置的命名規則：各設備模型中以“P_”開頭表示限速命令擬定(prepare)過程,以“E_”開頭表示TSRS中限速命令的執行下達（execute）過程，以“S_”開頭表示限速命令的設置（set）過程。模型中的主要位置如表1所示。

表1 模型中的主要位置

模型中的主要通道如表2所示。

TA=TACTC–A||TATSRS–A||TACTC–B||TATSRS–B

整個時間自動機網絡使用全局變量進行通信，用來保證系統邏輯功能的準確性。整型變量如confirmFlag、promptFlag、exeFlag分別用于控制確認、提示、執行結果，取值為1表示成功，0表示失敗，以此來達到模型邏輯的準確性。應用時鐘變量進行精確的時鐘控制，設置時鐘集合 X={T0, T1, T2}，其中，T0用來控制分界口臨時限速命令激活驗證提示時間，T1、T2用來描述相應的TSRS與TCC/RBC的通信時間。模型中T_reaction、T_timeout分別表示TSRS與TCC/RBC通信的響應時間和中斷時間，由于本文主要對分界口臨時限速系統信息交互進行建模，側重于跨界限速，因此沒有列出TCC/RBC的時間自動機模型，但在TSRS-A的模型中描述出了其與TCC/RBC的通信過程，同時，詳細對調度臺A限速命令的擬定、驗證、下達過程進行建模，與調度臺B有關的模型描述了輔助完成調度臺A限速命令下達的過程，其與調度臺A相似的工作過程，在模型中均省略。

3 系統模型驗證

根據CTC分界口臨時限速系統約束提出的系統功能和性能要求，利用UPPAAL工具分別對其進行驗證，從而說明系統的安全性和受限活性。

系統的安全性用于描述系統不一定發生的事情，指“壞的事情永遠都不會發生”，其驗證可以歸結為時間自動機的可達性分析；系統的受限活性用于說明系統必定會發生某些事情，指“好的事情終究會發生”[5]，可以由時間自動機位置的不變式和轉換的約束條件來保證。

系統的功能和性能要求如下：

（1）功能屬性要求：a.CTC應能擬定、設置、取消臨時限速命令；b.TSRS保證限速命令先驗證后執行；c.TSRS-A激活提示成功的同時請求相鄰TSRS-B激活提示；d.TSRS-A能分發臨時限速命令到相應的TCC/RBC執行同時請求TSRS-B分發執行； e.各設備均應對接收到的限速信息進行有效性驗證。

（2）性能屬性要求：a.TSRS-A通信響應間隔在T_reaction內完成；b.在T_timeout時間內TSRS-A通信未完成， 則視為通信中斷。

UPPAAL為驗證提供了一種BNF（Bac-kus Naur Form）語法：

Prop:= A[]φ|E<>φ|E[]φ|A<> →ψ其中φ,ψ為所驗證的系統性質的邏輯表達式；字符A、E用來量化路徑即時間自動機描述的一個轉換，A表示給定的性質對于所有路徑均滿足，E表示至少有一條路徑滿足性質，[]、<>用來量化路徑上的狀態，[]表示路徑上的所有狀態均滿足給定的性質，<>表示路徑上至少有一個狀態滿足給定的性質。

應用BNF語言在UPPAAL驗證器中對以上列出的性質進行驗證。

把上述驗證語句輸入UPPAAL驗證器中，逐條驗證每條性質。

在驗證器中，性質列表中每條性質后面的灰色圓形標志變成綠色表示驗證通過，驗證的進度與結果一欄中進一步表明列表中所列的性質均滿足，即CTC分界口臨時限速時間自動機網絡 能滿足系統的這些性質。通過驗證說明模型是安全可靠的，系統滿足邏輯和時間上的要求。

4 結束語

本文在分析CTC調度臺分界口處臨時限速工作流程的基礎上，以其安全性和受限活性為驗證目標，建立整個系統交互的時間自動機網絡模型，作為驗證的基礎。根據CTC分界口臨時限速系統約束提出功能和性能等系統性質，利用UPPAAL驗證工具，驗證了各條性質均得到滿足，從而說明了系統的安全性和受限活性，為系統的設計和開發提供了一定的依據。

[1]古天龍.軟件開發的形式化方法[M].北京:高等教育出版社，2005：5-67.

[2]吳永剛，陸慧娟.基于時間自動機的實時系統建模及驗證[J].計算機時代，20116（1）：2-3.

[3]劉傳會，張廣泉.一種基于時間自動機網絡的實時系統形式化驗證方法[J].蘇州大學學報，2008，24（1）：35-40.

[4]袁 磊，王俊峰.CTCS-3級列控系統臨時限速建模與驗證[J].西南交通大學學報，2013，48（4）：710-712.

[5]OLDEROGER, DIERKSH. Real-time systems[M].London:Cambridge University Press，2008: 137-146．

[6]康仁偉.基于時間自動機的CTCS-3級列控系統建模方法與驗證研究[D].北京:北京交通大學， 2013：40-53.