基于時間自動機的CBI道岔轉(zhuǎn)換時間建模與驗證

石 佳

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

基于時間自動機的CBI道岔轉(zhuǎn)換時間建模與驗證

石 佳

（西南交通大學(xué) 信息科學(xué)與技術(shù)學(xué)院，成都 610031）

針對CBTC計算機聯(lián)鎖安全性十分重要的問題，介紹時間自動機理論，分析CBTC計算機聯(lián)鎖系統(tǒng)的結(jié)構(gòu)和與傳統(tǒng)聯(lián)鎖系統(tǒng)的區(qū)別，以CBTC聯(lián)鎖系統(tǒng)的道岔轉(zhuǎn)換功能為例，采用UPPAAL建立了道岔轉(zhuǎn)換模型，分析模型的安全需求。表明了在聯(lián)鎖系統(tǒng)開發(fā)過程中采用基于時間自動機建模與驗證的方法的可行性和有效性。

時間自動機；計算機聯(lián)鎖；建模；驗證

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

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

1 理論基礎(chǔ)

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

定義1： 時鐘約束[3]

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

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

定義2：時鐘解釋

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

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

定義3：時間自動機

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

其中[3]：

S—有限位置集合；

S0—初始位置集合；

∑—有窮標記集合；

X—有限時鐘集合；

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

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

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

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

圖1 UPPAAL結(jié)構(gòu)

2 計算機聯(lián)鎖系統(tǒng)建模與驗證

2.1 計算機聯(lián)鎖系統(tǒng)

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

圖2 聯(lián)鎖系統(tǒng)結(jié)構(gòu)

CBI接受來自人機會話層的控制信息，來自監(jiān)控層的室外信號設(shè)備的狀態(tài)信息，依據(jù)這些信息及相關(guān)的聯(lián)鎖條件，進行聯(lián)鎖運算并產(chǎn)生道岔轉(zhuǎn)換、鎖閉、信號開放、關(guān)閉等命令。在CBTC系統(tǒng)中，計算機聯(lián)鎖子系統(tǒng)的功能要素相較于傳統(tǒng)聯(lián)鎖有了一些新的變化，主要體現(xiàn)在：

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

（2）聯(lián)鎖邏輯檢查：傳統(tǒng)聯(lián)鎖系統(tǒng)檢查進路始、終端信號機及狀態(tài)、進路所包含軌道區(qū)段狀態(tài)、待鎖閉進路相關(guān)敵對進路狀態(tài)；CBTC聯(lián)鎖系統(tǒng)大多數(shù)情況下無需檢查信號機條件，只需明確進路路徑，不需要檢查區(qū)段空閑狀態(tài)。

（3）聯(lián)鎖設(shè)備管理：傳統(tǒng)聯(lián)鎖系統(tǒng)以進、出站信號機為限，只管理站內(nèi)進路及相關(guān)地面信號要素；CBTC的聯(lián)鎖系統(tǒng)實現(xiàn)區(qū)域化聯(lián)鎖控制，將區(qū)間設(shè)備也納入所屬聯(lián)鎖區(qū)統(tǒng)一管轄，聯(lián)鎖區(qū)之間通過通信方式實現(xiàn)照查。

CBTC聯(lián)鎖系統(tǒng)[5]的具體內(nèi)容如圖3所示。

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

CBI道岔控制模塊是計算機聯(lián)鎖的重要功能，主要負責(zé)道岔的轉(zhuǎn)換、鎖閉和解鎖。以道岔轉(zhuǎn)換功能為例：

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

利用UPPAAL建立道岔轉(zhuǎn)換模型，道岔模型全局聲明如下：

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重置道岔轉(zhuǎn)換時鐘，timeOut表示道岔轉(zhuǎn)換超時，sw_request表示道岔轉(zhuǎn)換請求，sw_locked表示道岔鎖閉，changeSucc表示道岔轉(zhuǎn)換成功。

道岔轉(zhuǎn)換模型如圖4所示。Switch0構(gòu)件接受到道岔轉(zhuǎn)換消息后，檢查道岔是否鎖閉，道岔是否在需求位置，當(dāng)未道岔鎖閉且未在需求位置時，Switch0發(fā)送setTime消息給道岔轉(zhuǎn)換時鐘構(gòu)件SwitchTime，轉(zhuǎn)換成功后則鎖閉。

圖3 系統(tǒng)聯(lián)鎖邏輯圖

圖4 道岔轉(zhuǎn)換模型

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

圖5 道岔時鐘模型

2.3 模型驗證

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

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

圖6 道岔控制消息序列圖

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

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

（2）道岔在規(guī)定的時間13 s內(nèi)可以操作完成：

A[]Switch0.ChangeOver imply

SwitchTime.t ≤13

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

圖7 驗證結(jié)果

3 結(jié)束語

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

[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_一種適合自動驗證實時系統(tǒng)的工具[J].微計算機信息，2006，22（5）：1-2.

[3]孫全勇.時間自動機及其應(yīng)用研究[D].哈爾濱：哈爾濱工程大學(xué)，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系統(tǒng)的聯(lián)鎖邏輯研究[D].成都：西南交通大學(xué)，2014.

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

責(zé)任編輯 徐侃春

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

石 佳，在讀碩士研究生。