基于時間自動機的CBI道岔轉換時間建模與驗證

石 佳

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

基于時間自動機的CBI道岔轉換時間建模與驗證

石 佳

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

針對CBTC計算機聯鎖安全性十分重要的問題，介紹時間自動機理論，分析CBTC計算機聯鎖系統的結構和與傳統聯鎖系統的區別，以CBTC聯鎖系統的道岔轉換功能為例，采用UPPAAL建立了道岔轉換模型，分析模型的安全需求。表明了在聯鎖系統開發過程中采用基于時間自動機建模與驗證的方法的可行性和有效性。

時間自動機；計算機聯鎖；建模；驗證

基于通信的列車控制（CBTC，Communication Based Train Control）系統是城市軌道交通系統的發展方向。CBTC通過連續、大容量的通信方式實現車—地雙向數據通信，采用了高精度列車定位技術，具有安全性高、線路利用率高、自動化程度高、工程建設周期短、系統靈活性和兼容性強等優點。計算機聯鎖（CBI， Computer Based Interlocking）系統是CBTC的核心子系統之一，是典型的安全苛求系統（Safety Critical System）。CBI是一個實時控制系統，邏輯復雜，對實時性要求高，失效后可能危及行車安全，軟件安全性需要經過嚴格的驗證[1]。

形式化方法具有語義清晰、語法準確、描述準確規范、表達無二義性的優點，是保證系統安全性、可靠性的重要途徑。為滿足實時系統的建模和驗證需要，Alur和Dill對形式化的自動機理論進行了擴展，提出了時間自動機（TA，Timed Automata）。利用TA對實時系統進行建模、分析，能夠保證實時系統具有較高的安全性和可靠性。本文分析了時間自動機理論，并采用UPPAAL[2]建立了CBI道岔轉換的時間自動機模型，最后驗證了模型的安全性，表明道岔滿足聯鎖系統的安全需求。

1 理論基礎

時間自動機在傳統有限自動機的基礎上擴展出了時鐘約束，包括為遷移添加的時鐘約束和為狀態添加的不變式約束兩種方式。遷移上的時鐘約束表示只有在此約束被滿足時遷移才能激活，狀態不變式約束表示只有滿足不變式時才能停留在此狀態。

定義1： 時鐘約束[3]

X是一個時鐘變量集合，時間約束δ的集合φ(X)如下：

其中，x為X的時鐘變量，c∈Q+，δ1和δ2表示時鐘約束。

定義2：時鐘解釋

時鐘集合X的一個時鐘解釋為X到非負實數集R+的一個映射。

在時鐘解釋v下，如果時鐘約束δ的值為真，則稱時鐘解釋v滿足X上的一個時鐘約束δ。

定義3：時間自動機

六元組＜S,S0,∑,X,I,E＞稱為時間自動機。

其中[3]：

S—有限位置集合；

S0—初始位置集合；

∑—有窮標記集合；

X—有限時鐘集合；

I—將S中的位置映射到φ(x)上的時間約束的映射；

E ? S·∑·2x·Φ(X)·S—轉移集合。

UPPAAL是一款時間自動機建模工具。UPPAAL建立的模型包括一組時間自動機，一組時鐘，全局變量以及同步信道。UPPAAL是一個模型檢測器，涵蓋了詳盡的系統動態行為，并使用復雜的約束求解技術完成符號模型判別，證明系統的安全性和受限活性[4]。

UPPAAL主要包括3個部分：編輯器、模擬器和驗證器，如圖1所示。編輯器主要用于建立時間自動機模型，模擬器用于模擬模型的執行過程，以便在驗證前發現潛在的錯誤。驗證器通過搜索機制檢測模型是否滿足相關性質。

圖1 UPPAAL結構

2 計算機聯鎖系統建模與驗證

2.1 計算機聯鎖系統

聯鎖系統的發展階段分為機械聯鎖、電氣聯鎖、計算機聯鎖。目前，隨著微處理器的飛速發展，計算機聯鎖已成為鐵路發展方向的新一代信號系統。計算機聯鎖系統以計算機技術為主要技術手段，負責處理進路內的道岔、信號機、區段之間的安全聯鎖關系，并在ATS或操作員的控制指令下向ATP、ATS輸出聯鎖信息。根據設備功能的不同以及所處位置不同，計算機聯鎖可以被劃分成4層結構，如圖2所示。

圖2 聯鎖系統結構

CBI接受來自人機會話層的控制信息，來自監控層的室外信號設備的狀態信息，依據這些信息及相關的聯鎖條件，進行聯鎖運算并產生道岔轉換、鎖閉、信號開放、關閉等命令。在CBTC系統中，計算機聯鎖子系統的功能要素相較于傳統聯鎖有了一些新的變化，主要體現在：

（1）列車位置檢查：傳統聯鎖系統通過軌道電路檢測列車位置，而CBTC中的聯鎖系統接收來自區域控制器的列車位置信息，該信息由車載ATP通過無線或其他方式傳輸給區域控制器；在后備模式下則是通過計軸設備來確定物理區段占用情況。

（2）聯鎖邏輯檢查：傳統聯鎖系統檢查進路始、終端信號機及狀態、進路所包含軌道區段狀態、待鎖閉進路相關敵對進路狀態；CBTC聯鎖系統大多數情況下無需檢查信號機條件，只需明確進路路徑，不需要檢查區段空閑狀態。

（3）聯鎖設備管理：傳統聯鎖系統以進、出站信號機為限，只管理站內進路及相關地面信號要素；CBTC的聯鎖系統實現區域化聯鎖控制，將區間設備也納入所屬聯鎖區統一管轄，聯鎖區之間通過通信方式實現照查。

CBTC聯鎖系統[5]的具體內容如圖3所示。

2.2 CBI道岔的時間自動機模型

CBI道岔控制模塊是計算機聯鎖的重要功能，主要負責道岔的轉換、鎖閉和解鎖。以道岔轉換功能為例：

CBI接收來自ATS/LCW的道岔單操或進路道岔需求命令，檢查道岔是否鎖閉、目前位置是否正確，決定是否啟動轉轍機轉換道岔。

利用UPPAAL建立道岔轉換模型，道岔模型全局聲明如下：

bool sw_lock,sw_position;

chan timeOut,setTime,sw_request,sw_locked,changeSucc。

其中，sw_lock表示道岔是否鎖閉，sw_position表示道岔是否在需求位置。信道setTime、timeOut、sw_request、sw_locked、changeSucc和SwitchTime模塊之間的通道，其中，setTime重置道岔轉換時鐘，timeOut表示道岔轉換超時，sw_request表示道岔轉換請求，sw_locked表示道岔鎖閉，changeSucc表示道岔轉換成功。

道岔轉換模型如圖4所示。Switch0構件接受到道岔轉換消息后，檢查道岔是否鎖閉，道岔是否在需求位置，當未道岔鎖閉且未在需求位置時，Switch0發送setTime消息給道岔轉換時鐘構件SwitchTime，轉換成功后則鎖閉。

圖3 系統聯鎖邏輯圖

圖4 道岔轉換模型

CBI要求道岔需要在13 s內轉換到需求位置。若轉換時間大于等于13 s，則轉換失敗，應由技術人員現場檢查道岔或重新轉換；若在13 s內轉換成功且道岔位置與命令中位置狀態一致，則道岔鎖閉，轉換完成。道岔轉換時鐘模塊如圖5所示。

圖5 道岔時鐘模型

2.3 模型驗證

UPPAAL模型分析包括模擬仿真和模型驗證兩個方面。模擬仿真是指對系統模型進行模擬，在驗證之前發現系統執行過程中可能發生的錯誤。模型驗證是指驗證器通過快速搜索機制搜索系統的狀態空間、檢查時鐘約束和相應性質。

道岔模型的一個隨機模擬序列如圖6所示。Switch0模型接受到道岔轉換請求后，轉移到CheckLock狀態檢查道岔是否鎖閉，未鎖閉后轉入CheckState檢查道岔位置狀態，由于道岔不在需求位置，Switch0向SwitchTime發送時鐘重置消息請求道岔轉換，SwitchTime啟動道岔轉換后，發現道岔轉換超時，并發送timeOut轉換超時消息給Switch0模型，使其進入故障處理狀態Error。

圖6 道岔控制消息序列圖

UPPAAL采用BNF語法描述系統安全需求[6]。道岔模型要求的安全需求包括：

（1）模型無死鎖：A[]not deadlock；

（2）道岔在規定的時間13 s內可以操作完成：

A[]Switch0.ChangeOver imply

SwitchTime.t ≤13

在UPPAAL的驗證器中驗證，兩條安全需求均滿足，表明模型滿足預期安全需求，驗證結果如圖7所示。

圖7 驗證結果

3 結束語

城市軌道交通聯鎖系統是信號系統的重要組成部分，在保障列車行車安全方面有極其重要的作用。聯鎖系統對安全性和實時性有著很高的要求，系統邏輯極其復雜。UPPAAL作為一種易于操作使用且功能強大的時間自動機工具，能夠完成聯鎖系統的建模、模擬和驗證，對開發系統過程中保證系統的安全性和可靠性具有十分重要的意義。下一步工作將對時間自動機在城市軌道交通信號系統中的應用做進一步研究。

[1]Pengfei Sun,Simon Collart-dutilleul,Philippe Bon,A Model Pattern of Railway Interlocking System by Petri Nets[C].International Conference on Models and Technologies for Intelligent Transportation Systems (MT-ITS),2015.

[2]郭 華.UPPAAL_一種適合自動驗證實時系統的工具[J].微計算機信息，2006，22（5）：1-2.

[3]孫全勇.時間自動機及其應用研究[D].哈爾濱：哈爾濱工程大學，2006.

[4]James L.Rash Christopher A.Rouff Walt Truszkowski Diana Gordon Michael G.Hinchey.Formal Approaches toAgent-Based Systems[Z].Springer,2000,117:120.

[5]楊 淘.基于CBTC系統的聯鎖邏輯研究[D].成都：西南交通大學，2014.

[6]王觀寧.基于UPPAAL的聯鎖進路控制流程建模與驗證[D].北京：北京交通大學，2009.

責任編輯 徐侃春

Modeling and verifcation of CBI switch transaction time based on timed automata

SHI Jia
( School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031,China)

Focusing on the problem that the safety of CBTC computer based interlocking is critical,this article introduced the theory of timed automata,analyzed the architecture and differences between CBTC computer based interlocking system and traditional interlocking system, took an example of switch transaction,switch transaction model was established by using UPPAAL.The security requirements of the model were also analyzed,which showed the feasibility and effectiveness of the modeling and verifcation methods based on timed automata,during the process of developing computer based interlocking system.

timed automata;computer based interlocking (CBI);modeling;verifcation

U213.6：TP39

A

1005-8451（2016）08-0052-04

2016-01-15

石 佳，在讀碩士研究生。