基于時(shí)間自動(dòng)機(jī)的CBI道岔轉(zhuǎn)換時(shí)間建模與驗(yàn)證

石 佳

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

基于時(shí)間自動(dòng)機(jī)的CBI道岔轉(zhuǎn)換時(shí)間建模與驗(yàn)證

石 佳

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

針對(duì)CBTC計(jì)算機(jī)聯(lián)鎖安全性十分重要的問(wèn)題，介紹時(shí)間自動(dòng)機(jī)理論，分析CBTC計(jì)算機(jī)聯(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)開(kāi)發(fā)過(guò)程中采用基于時(shí)間自動(dòng)機(jī)建模與驗(yàn)證的方法的可行性和有效性。

時(shí)間自動(dòng)機(jī)；計(jì)算機(jī)聯(lián)鎖；建模；驗(yàn)證

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

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

1 理論基礎(chǔ)

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

定義1： 時(shí)鐘約束[3]

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

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

定義2：時(shí)鐘解釋

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

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

定義3：時(shí)間自動(dòng)機(jī)

六元組＜S,S0,∑,X,I,E＞稱為時(shí)間自動(dòng)機(jī)。

其中[3]：

S—有限位置集合；

S0—初始位置集合；

∑—有窮標(biāo)記集合；

X—有限時(shí)鐘集合；

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.2 CBI道岔的時(shí)間自動(dòng)機(jī)模型

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

CBI接收來(lái)自ATS/LCW的道岔單操或進(jìn)路道岔需求命令，檢查道岔是否鎖閉、目前位置是否正確，決定是否啟動(dòng)轉(zhuǎn)轍機(jī)轉(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)換時(shí)鐘，timeOut表示道岔轉(zhuǎn)換超時(shí)，sw_request表示道岔轉(zhuǎn)換請(qǐng)求，sw_locked表示道岔鎖閉，changeSucc表示道岔轉(zhuǎn)換成功。

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

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

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

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

圖5 道岔時(shí)鐘模型

2.3 模型驗(yàn)證

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

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

圖6 道岔控制消息序列圖

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

（1）模型無(wú)死鎖：A[]not deadlock；

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

A[]Switch0.ChangeOver imply

SwitchTime.t ≤13

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

圖7 驗(yàn)證結(jié)果

3 結(jié)束語(yǔ)

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

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

[3]孫全勇.時(shí)間自動(dòng)機(jī)及其應(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)鎖進(jìn)路控制流程建模與驗(yà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

石 佳，在讀碩士研究生。