基于XML的時(shí)間自動(dòng)機(jī)狀態(tài)可達(dá)性分析在RBC子系統(tǒng)中的應(yīng)用

宋海鋒，唐 濤，李開(kāi)成，呂繼東

（1.北京交通大學(xué) 軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心，北京 100044 2.北京交通大學(xué) 軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室，北京 100044）

基于XML的時(shí)間自動(dòng)機(jī)狀態(tài)可達(dá)性分析在RBC子系統(tǒng)中的應(yīng)用

宋海鋒1，唐 濤2，李開(kāi)成1，呂繼東1

（1.北京交通大學(xué) 軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心，北京 100044 2.北京交通大學(xué) 軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室，北京 100044）

時(shí)間自動(dòng)機(jī)中的狀態(tài)可達(dá)性分析是模型建立完成之后的一個(gè)重要驗(yàn)證工作，大多數(shù)時(shí)間自動(dòng)機(jī)建模工具均為非開(kāi)源代碼，不能與實(shí)際系統(tǒng)進(jìn)行有機(jī)的結(jié)合。本文以CTCS-3中的無(wú)線閉塞中心（RBC）[1]為實(shí)際系統(tǒng)，提出基于XML的時(shí)間自動(dòng)機(jī)狀態(tài)可達(dá)性分析[2]，實(shí)現(xiàn)了建模工具與實(shí)際測(cè)試平臺(tái)不同開(kāi)發(fā)環(huán)境下的數(shù)據(jù)交互，為完善整個(gè)測(cè)試平臺(tái)在理論方法與實(shí)際應(yīng)用相結(jié)合方面提出一個(gè)較為可行的方法。

模型檢驗(yàn)；CTCS-3；可達(dá)性分析；形式化建模；測(cè)試分析

線閉塞中心（RBC）子系統(tǒng)測(cè)試平臺(tái)的主要任務(wù)是測(cè)試，發(fā)現(xiàn)在執(zhí)行一個(gè)測(cè)試序列的過(guò)程中出現(xiàn)的異常，并找出導(dǎo)致該異常的原因，能夠進(jìn)行自動(dòng)分析，是目前需要解決的一個(gè)問(wèn)題。我們引入模型檢驗(yàn)的方法，其基本思想是用狀態(tài)遷移來(lái)表示系統(tǒng)的行為，這樣“系統(tǒng)是否具有所期望的性質(zhì)”就轉(zhuǎn)化為數(shù)學(xué)問(wèn)題“狀態(tài)遷移系統(tǒng)S是否是公式F的一個(gè)模型”。在時(shí)間自動(dòng)機(jī)軟件UPPAAL以及有色Petri網(wǎng)軟件CPN中用來(lái)表示狀態(tài)遷移的都是通用的XML文件，通過(guò)對(duì)XML文件的解析，可以將用非開(kāi)源的形式化建模軟件所生成的模型一定程度上開(kāi)源化，直接從底層文件進(jìn)行系統(tǒng)層面的分析。本文以解析XML文件進(jìn)行時(shí)間自動(dòng)機(jī)中狀態(tài)可達(dá)性分析，為形式化建模軟件在實(shí)際應(yīng)用中的二次開(kāi)發(fā)提出了新途徑，將在一定程度上擴(kuò)寬該測(cè)試分析方法的適應(yīng)范圍。

1 時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)是為解決建模以及驗(yàn)證實(shí)時(shí)系統(tǒng)所遇到的時(shí)間問(wèn)題，而對(duì)原有自動(dòng)機(jī)理論的一個(gè)擴(kuò)展，最早由R. Alur等人提出。

自動(dòng)機(jī)可以表示為一個(gè)五元組，分別如下[3～4]：

（1）Q是狀態(tài)的集合；

（2）∑是符號(hào)的有限集合，可以稱(chēng)之為自動(dòng)機(jī)接受的字母表；

（3）δ是轉(zhuǎn)移函數(shù)，δ∶Q×∑→Q；

（4） q0是開(kāi)始狀態(tài)，指的是當(dāng)自動(dòng)機(jī)還未處理輸入的時(shí)候的狀態(tài)（ q0∈Q）；

轉(zhuǎn)換系統(tǒng)SA從初始狀態(tài)s0（s0∈S0）開(kāi)始，E中的一個(gè)狀態(tài)轉(zhuǎn)移＜s, a, s'＞表示轉(zhuǎn)換系統(tǒng)SA在輸入字符a（a∈∑）時(shí)，從狀態(tài)s到狀態(tài)s'的一個(gè)轉(zhuǎn)移，記做：

如果對(duì)某個(gè)輸入 a，有：

則稱(chēng)狀態(tài)s'是從狀態(tài)s可達(dá)的。如果狀態(tài)s是從某個(gè)初始狀態(tài)可達(dá)的，那么s是轉(zhuǎn)換系統(tǒng)中的一個(gè)可達(dá)狀態(tài)。

時(shí)間自動(dòng)機(jī)是有限自動(dòng)機(jī)模型在時(shí)間域的一種自然擴(kuò)展，時(shí)間自動(dòng)機(jī)TA是一個(gè)六元組＜S, S0，∑，X，I，E＞[4]，由于時(shí)間自動(dòng)機(jī)的狀態(tài)與某一事件發(fā)生時(shí)間相關(guān)，而時(shí)間是單調(diào)無(wú)限遞增的，因此，時(shí)間自動(dòng)機(jī)所接受的語(yǔ)言就是時(shí)間序列上的無(wú)限事件序列。

2 RBC在CTCS-3級(jí)列控系統(tǒng)中定位

CTCS-3級(jí)列車(chē)運(yùn)行控制系統(tǒng)（簡(jiǎn)稱(chēng)：列控系統(tǒng)）采用鐵路移動(dòng)通信系統(tǒng)（GSM-R）實(shí)現(xiàn)車(chē)-地信息的雙向傳輸， RBC負(fù)責(zé)生成行車(chē)許可（MA）并在CTCS-3下進(jìn)行控車(chē)， RBC根據(jù)地面子系統(tǒng)或來(lái)自外部地面系統(tǒng)的信息，如列車(chē)位置信息、軌道占用信息、聯(lián)鎖進(jìn)路狀態(tài)等實(shí)時(shí)計(jì)算產(chǎn)生列車(chē)行車(chē)許可，通過(guò)GSM-R發(fā)送給車(chē)載列車(chē)自動(dòng)防護(hù)（ATP）設(shè)備，保證其管轄內(nèi)列車(chē)的高速安全運(yùn)行[5]。本文針對(duì)RBC的軟件控制邏輯測(cè)試。

3 時(shí)間自動(dòng)機(jī)模型建立

3.1 建模與驗(yàn)證框架設(shè)計(jì)流程

利用時(shí)間自動(dòng)機(jī)理論，對(duì)CTCS-3級(jí)列控系統(tǒng)建模與驗(yàn)證框圖如圖1所示。

圖1 時(shí)間自動(dòng)機(jī)理論建模與驗(yàn)證框圖

對(duì)RBC子系統(tǒng)進(jìn)行形式化建模的過(guò)程同時(shí)也是進(jìn)行RBC子系統(tǒng)設(shè)計(jì)的過(guò)程，包括概要設(shè)計(jì)和詳細(xì)設(shè)計(jì)。

概要設(shè)計(jì)的主要任務(wù)是確定RBC子系統(tǒng)的模塊結(jié)構(gòu)，以及各個(gè)子模塊之間的相互關(guān)系，隨后對(duì)功能模塊進(jìn)行劃分，每一個(gè)變量構(gòu)成一個(gè)自動(dòng)機(jī)組件。詳細(xì)設(shè)計(jì)是指根據(jù)每一個(gè)自動(dòng)機(jī)組件的內(nèi)部數(shù)據(jù)和算法來(lái)確定各個(gè)組件的時(shí)間約束和狀態(tài)動(dòng)作集，最終得到時(shí)間自動(dòng)機(jī)系統(tǒng)的網(wǎng)絡(luò)模型。

3.2 模型舉例

鑒于篇幅原因，此處僅介紹列車(chē)注冊(cè)與啟動(dòng)的模型。

時(shí)序圖如圖2、圖3所示[4～5]：

圖2 注冊(cè)與啟動(dòng)時(shí)序圖（1）

當(dāng)RBC回復(fù)車(chē)載設(shè)備M32系統(tǒng)版本信息一致時(shí)，車(chē)載設(shè)備回復(fù)M159表示通信會(huì)話(huà)已建立。下面自動(dòng)機(jī)有3種發(fā)展路徑：（1）報(bào)告位置有效，RBC給車(chē)載設(shè)備發(fā)送M24，包含P27純文本“不在RBC管轄范圍”，通信會(huì)話(huà)結(jié)束，狀態(tài)遷移從初始狀態(tài)遷移至?xí)?huà)結(jié)束RBC注銷(xiāo)列車(chē)，流程結(jié)束；（2）位置報(bào)告“無(wú)效”或“未知”，RBC發(fā)送M41消息接受列車(chē)，司機(jī)輸入列車(chē)數(shù)據(jù)，車(chē)載設(shè)備發(fā)送M129經(jīng)過(guò)確認(rèn)的列車(chē)數(shù)據(jù)，RBC回復(fù)M8列車(chē)數(shù)據(jù)確認(rèn)，車(chē)載設(shè)備人機(jī)界面（DMI）顯示啟動(dòng)按鈕，狀態(tài)遷移從初始狀態(tài)遷移至列車(chē)數(shù)據(jù)確認(rèn)；（3）列車(chē)位置有效且以RBC已知位置的應(yīng)答器為基準(zhǔn)，司機(jī)輸入列車(chē)數(shù)據(jù)，車(chē)載設(shè)備發(fā)送M129經(jīng)過(guò)確認(rèn)的列車(chē)數(shù)據(jù)，RBC回復(fù)M8列車(chē)數(shù)據(jù)確認(rèn)，DMI顯示啟動(dòng)按鈕，狀態(tài)遷移從初始狀態(tài)遷移至列車(chē)數(shù)據(jù)確認(rèn)。

為減少自動(dòng)機(jī)狀態(tài)的冗余，為后面可達(dá)性分析提供便利，以3種不同的情況所共有的狀態(tài)進(jìn)行復(fù)用。

時(shí)間自動(dòng)機(jī)建模如圖4所示。

圖3 注冊(cè)與啟動(dòng)時(shí)序圖（2）

4 基于XML的時(shí)間自動(dòng)機(jī)可達(dá)性分析實(shí)現(xiàn)

4.1 XML的引入

將實(shí)際車(chē)載設(shè)備與RBC消息交互流程即RBC的控車(chē)流程轉(zhuǎn)換為計(jì)算機(jī)可執(zhí)行的狀態(tài)遷移系統(tǒng)（S），該系統(tǒng)（S）是在時(shí)間自動(dòng)機(jī)建模軟件UPPAAL中存在的[6]。

UPPAAL的開(kāi)發(fā)環(huán)境為Java，是一個(gè)不開(kāi)源的時(shí)間自動(dòng)機(jī)建模軟件，雖然在其內(nèi)部所使用的BNF驗(yàn)證語(yǔ)言中就含有可達(dá)性分析的程序，由于其不開(kāi)源性，不能夠?qū)⑵渑c測(cè)試平臺(tái)結(jié)合起來(lái)。在時(shí)間自動(dòng)機(jī)建模軟件UPPAAL所生成的XML中，包含了所建立模型的所有狀態(tài)點(diǎn)信息，以及狀態(tài)之間的遷移。

在XML中實(shí)現(xiàn)可達(dá)性分析算法，在數(shù)學(xué)層面為深度優(yōu)先與廣度優(yōu)先的計(jì)算[7]，前向分析與后向分析分別能夠提供不同的分析內(nèi)容。

圖4 注冊(cè)與啟動(dòng)時(shí)間自動(dòng)機(jī)模型

4.2 提取時(shí)間自動(dòng)機(jī)狀態(tài)點(diǎn)

將XML文件加載到XElement類(lèi)的一個(gè)實(shí)例中。XElement類(lèi)的名稱(chēng)屬性是XName類(lèi)型，它代表該元素的名稱(chēng)。XName類(lèi)的localName屬性返回XML文檔沒(méi)有命名空間限定符的根元素名稱(chēng)，這個(gè)名字被添加作為根節(jié)點(diǎn)。由于我們只對(duì)元素感興趣，所以代碼使用Elements()方法來(lái)檢索＜ template＞元素的所有子元素。位置（Location）記錄的是所有狀態(tài)的身份（ID）信息，因此可以通過(guò).Name方法進(jìn)行ID編號(hào)信息的統(tǒng)計(jì)。狀態(tài)遷移（Transition）的信息包含源狀態(tài)（source）與目標(biāo)狀態(tài)（target），source與target的ID編號(hào)可以通過(guò)Attribute()方法進(jìn)行訪問(wèn)，該方法接受其值預(yù)被檢索的元素的名稱(chēng)屬性作為參數(shù)，并返回一個(gè)代表該屬性的XAttribute實(shí)例的名稱(chēng)。XAttribute類(lèi)的Value屬性提供了屬性的值。

時(shí)間自動(dòng)機(jī)中XML的結(jié)點(diǎn)信息如圖5所示。

圖5 時(shí)間自動(dòng)機(jī)模型與其XML

其中，source和target都是source.Name；"id13" 為source.FirstAttribute.Value

通過(guò)遍歷可將狀態(tài)的遷移，以及初始狀態(tài)、目標(biāo)狀態(tài)、狀態(tài)名稱(chēng)等所有相關(guān)信息都查詢(xún)出來(lái)，存儲(chǔ)到狀態(tài)遷移數(shù)組中，遍歷算法如下所示：

Algorithm traverse conditions and edges {} Xis the XMLfile D N V K =,, d D∈0 d n v k 0 00 0 ={ ,,} foreach(XElement transition in X) if(transition.Name=="location") count++; foreach(XElement source in transition.Elements()) if(source.Name=="source") get n0Add 0d toD return D N V K ={} ,,

4.3 狀態(tài)遷移的數(shù)據(jù)存儲(chǔ)實(shí)現(xiàn)

在整合source與target狀態(tài)點(diǎn)的信息時(shí)，在程序處理上，借鑒圖數(shù)據(jù)的儲(chǔ)存方式。常用的圖的儲(chǔ)存結(jié)構(gòu)有鄰接表、鄰接多重表和十字鏈表[7]。

用鄰接表（Adjacency List）存儲(chǔ)從XML中遍歷出來(lái)的信息。文獻(xiàn)[8]表明，當(dāng)牽扯到時(shí)鐘帶的存儲(chǔ)的時(shí)候用鄰接表來(lái)存儲(chǔ)將節(jié)省更多的空間，而且在搜索算法層面，鄰接表的存儲(chǔ)結(jié)構(gòu)占用更少的時(shí)間和空間復(fù)雜度[9]。

鄰接表是圖的一種鏈?zhǔn)酱鎯?chǔ)結(jié)構(gòu)[7]，在鏈接表中，對(duì)圖中每個(gè)頂點(diǎn)建立一個(gè)單鏈表，第i個(gè)單鏈表中的結(jié)點(diǎn)表示依附于頂點(diǎn)Vi的邊（對(duì)有向圖是以頂點(diǎn)Vi為尾的弧）。每個(gè)結(jié)點(diǎn)由3個(gè)域組成，其中鄰接點(diǎn)域（adjvex）指示與頂點(diǎn)Vi鄰接的點(diǎn)在圖中的位置，鏈域（nextarc）指示下一條邊或弧的結(jié)點(diǎn)；數(shù)據(jù)域（info）儲(chǔ)存和邊或弧相關(guān)的信息，如權(quán)值等。每個(gè)鏈表上附設(shè)一個(gè)表頭結(jié)點(diǎn)。在表頭結(jié)點(diǎn)中，除了設(shè)有鏈域（firstarc）指向鏈表中的第一個(gè)結(jié)點(diǎn)之外，還設(shè)有儲(chǔ)存頂點(diǎn)Vi的名或其他有關(guān)信息的數(shù)據(jù)域（data）。如表1、表2所示。

表1 表結(jié)點(diǎn)

表2 頭結(jié)點(diǎn)

這些表頭結(jié)點(diǎn)通常以順序結(jié)構(gòu)的形式儲(chǔ)存，以便隨機(jī)訪問(wèn)任一頂點(diǎn)的鏈表。一個(gè)圖的鏈接表存儲(chǔ)結(jié)構(gòu)如圖6所示。

圖6 鄰接表

4.4 可達(dá)性分析算法實(shí)現(xiàn)

模型檢驗(yàn)采用計(jì)算樹(shù)邏輯與命題線性時(shí)序邏輯相結(jié)合的算法[10]，系統(tǒng)狀態(tài)的變化可以用樹(shù)或者圖的思想表示，因?yàn)橄到y(tǒng)的反應(yīng)是不確定的，因此在樹(shù)或圖中的表現(xiàn)為樹(shù)具有多個(gè)子樹(shù)（SubTree），圖具有不同的后繼頂點(diǎn)（Vertex），依次類(lèi)推系統(tǒng)的運(yùn)行狀態(tài)就生成了一棵狀態(tài)樹(shù)（Staging tree）或有向圖（Digraph）。

在整合source與target狀態(tài)點(diǎn)中，將時(shí)間自動(dòng)機(jī)的狀態(tài)遷移按照鄰接表的思想存儲(chǔ)。利用可達(dá)性分析算法進(jìn)行驗(yàn)證的過(guò)程如下：

normalreachability a orithm _ _ lg P={} W {(, ())} =∧( )W≠Φ (,) . () l Z I l 00 0 while do l Z W popstate =

if Pr (,) test operty l Z if (,) : l Y P Z Y ? ∈ ? then return true {(,)} P P l Z′′ ′′?? do if (, ) : =∪(, ):(,) (, ) l Z l Z l Z? ∈ ? then {(,)} l Y W Z Y′′ ′ ′W W l Z′′=∪endif done endif done return false

（1）用時(shí)間自動(dòng)機(jī)為系統(tǒng)建模，如果系統(tǒng)由若干個(gè)子進(jìn)程（process）組成，則分別對(duì)各個(gè)子系統(tǒng)建模，求這若干子進(jìn)程的積自動(dòng)機(jī)。

（2）利用下文所示的可達(dá)性分析算法，對(duì)積自動(dòng)機(jī)進(jìn)行深度或者廣度優(yōu)先搜索，求得所有的可達(dá)狀態(tài)。

（3）分析可達(dá)狀態(tài)集，如果可達(dá)狀態(tài)集中包含了不應(yīng)該的事實(shí)，則認(rèn)為系統(tǒng)模型不滿(mǎn)足系統(tǒng)規(guī)格說(shuō)明，否則說(shuō)明系統(tǒng)模型滿(mǎn)足系統(tǒng)規(guī)格說(shuō)明。

可達(dá)性分析算法如下：

其中，P表示所有可達(dá)狀態(tài)集合，且初始值為空，W表示當(dāng)前已經(jīng)遍歷到的等待判定是否可達(dá)的狀態(tài)集合。針對(duì)時(shí)鐘帶的存儲(chǔ)方式，對(duì)可達(dá)性分析算法進(jìn)行了改進(jìn)，改進(jìn)后的算法如下：

normalreachability a orithm _ _ lg P={} W {(, ())} l Z I l 00 0 while do =∧( )W≠Φ (,) . () l Z W GetHead = for all(, )l Z P′∈get(, )l Z′AdjLinkToDBM Z′done ifZ Z′? for all(, )l Z P′∈ then :{(, ) () l Z′′′is the Successor of( ) , SuccSet l Z′′′= |( ) , l Z and endif for all SuccSet Z W. l ∈′′ ) , AddTail(l′( do ) ,Z′′P. ZlAdd( done done DBMToAdjLi ) nk (Z) ,

5 驗(yàn)證測(cè)試

在實(shí)時(shí)調(diào)試過(guò)程中，所有的設(shè)備都需要一直確保工作正常。為檢驗(yàn)本文所提出的分析方法的正確性，人為地在測(cè)試序列執(zhí)行過(guò)程中添加故障，用文中提出的方法對(duì)測(cè)試結(jié)果進(jìn)行分析，通過(guò)對(duì)比自動(dòng)分析的結(jié)果與人工添加的故障，驗(yàn)證該方法的正確性。可選擇的故障類(lèi)型如表3所示，實(shí)際測(cè)試中選用√標(biāo)記的“等級(jí)轉(zhuǎn)換未確認(rèn)”。

表3 可選故障類(lèi)型

在本次測(cè)試中，選用的方法是在CTCS-3級(jí)向CTCS-2級(jí)轉(zhuǎn)換時(shí)，ATP提示司機(jī)進(jìn)行操作，司機(jī)忽略，不予以確認(rèn)，使得ATP施加最大常用制動(dòng)，并記錄司機(jī)行為。

分析工具為本文軟件實(shí)現(xiàn)部分，其主界面如圖7所示。

圖7 分析工具主界面

選擇源ID（Source ID）與目標(biāo)ID（Target ID），點(diǎn)擊“可達(dá)性分析”按鈕，在分析結(jié)果中可以顯示狀態(tài)是否可達(dá)，并在可行路徑中，提供從Source ID到Target ID的可執(zhí)行序列。

在載入數(shù)據(jù)、選擇XML文件后，點(diǎn)擊菜單列表中的“自動(dòng)分析”，程序?qū)z索數(shù)據(jù)庫(kù)記錄數(shù)據(jù)，在可選故障下拉列表中顯示“施加最大常用制動(dòng)至停車(chē)”，分析結(jié)果框中包含3部分信息：

（1）“關(guān)聯(lián)時(shí)間自動(dòng)機(jī)狀態(tài)”，其顯示與ATP制動(dòng)停車(chē)所相關(guān)的可達(dá)路徑中相關(guān)的時(shí)間自動(dòng)機(jī)狀態(tài)ID以及名稱(chēng)。

（2）“原因分析”為測(cè)試工具進(jìn)行可達(dá)性分析自動(dòng)得出的結(jié)論，如圖8所示，原因分析以前“可選故障”的狀態(tài)Target ID為ID47-_Name_[Level_Transition_3To2]等級(jí)轉(zhuǎn)換未確認(rèn)。

圖8 自動(dòng)測(cè)試結(jié)果

（3）“時(shí)間自動(dòng)機(jī)狀態(tài)遷移路徑”顯示為進(jìn)行可達(dá)性分析過(guò)程中所檢索到的可達(dá)路徑，及與無(wú)線消息記錄（MGS）數(shù)據(jù)庫(kù)匹配過(guò)后的路徑，ID47_Name_[Level_Transition_3To2]--＞I D 4 0_N a m e_[]--＞I D 3 9_N a m e[]--＞ID38_Name[]--＞ID44_Name[]--＞ID43_Na me_[Hit_edge]--＞ID5_Name_[Without_confirm]--＞ID4_Name_[ATP_record_reason]--＞ID3_Name_ [Service_braking]--＞ID67_Name_[END]，將引起“可選故障”的一條路徑顯示出來(lái)；在自動(dòng)測(cè)試界面的右側(cè)顯示無(wú)線消息交互流程，將與故障原因相關(guān)的無(wú)線消息進(jìn)行標(biāo)紅顯示，方便分析。

從測(cè)試結(jié)果圖8中可以看出，自動(dòng)分析定位出的原因，與表3中選擇的故障吻合，一定程度上證明了該方法在實(shí)際測(cè)試工程中的準(zhǔn)確性。

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

對(duì)時(shí)間自動(dòng)機(jī)建模軟件UPPAAL所生成的XML文件進(jìn)行深入分析研究，將非開(kāi)源軟件UPPAAL，進(jìn)行基于XML的編程解析，實(shí)現(xiàn)了可達(dá)性分析工作，將原本不可開(kāi)源的狀態(tài)可達(dá)性分析變?yōu)榱碎_(kāi)源。

自動(dòng)分析尋找引起故障的原因，減少了測(cè)試人員的工作強(qiáng)度的同時(shí)，提高了測(cè)試過(guò)程的自動(dòng)化程度，其利用XML進(jìn)行解析的方法可以應(yīng)用到所有基于標(biāo)記語(yǔ)言的建模軟件的可達(dá)性分析中。

[1]寧 濱，唐 濤，李開(kāi)成，董海榮. 高速列車(chē)運(yùn)行控制系統(tǒng)[M]. 北京：北京科學(xué)出版社，2012.

[2]許 丹. 基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)形式化建模與驗(yàn)證[D]. 蘇州：蘇州大學(xué)，2007：24-36.

[3]古天龍．軟件開(kāi)發(fā)的形式化方法[M]．北京：高等教育出版社，2005：5-67．

[4]譚 耿.基于UPPAAL的RBC系統(tǒng)控車(chē)流程分析[D]．北京：北京交通大學(xué)，2008：7-17．

[5]張愛(ài)玲. CTCS--3級(jí)列控系統(tǒng)RBC行車(chē)許可生成的形式化建模與分析[D]. 蘭州：蘭州交通大學(xué)，2012.

[6]王大偉. 面向自動(dòng)化模型檢測(cè)的模型提取工具的設(shè)計(jì)與實(shí)現(xiàn)[D]. 湖南：湖南大學(xué)，2009.

[7]嚴(yán)蔚敏. 數(shù)據(jù)結(jié)構(gòu)[M]. 北京：清華大學(xué)出版社，1997.

[8]岳香芬，繆淮扣，許慶國(guó).一種改進(jìn)的實(shí)時(shí)系統(tǒng)可達(dá)性分析算法[J]. 上海大學(xué)學(xué)報(bào)（自然科學(xué)版），2006，12（3）：311-315.

[9]郭永林，齊楠楠.基于鄰接表存儲(chǔ)結(jié)構(gòu)的潛藏通路搜索算法的研究[J].科學(xué)技術(shù)與工程，2007（7）：1621-1623.

[10]林惠民.模型檢測(cè)：理論、方法與應(yīng)用[J].電子學(xué)報(bào)，2002.

責(zé)任編輯 楊利明

Reachability analysis of timed automata based on XML in RBC Sub-system

SONG Haifeng1, TANG Tao2, LI Kaicheng1, LV Jidong1
( 1. National Engineering Research Center of Rail Transportation Operation and Control System, Beijing Jiaotong University, Beijing 100044, China; 2.State Key Laboratory of Rail Traf fi c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

Reachability analysis was an important verification work after the model was built in timed automata, while most of the timed automata modeling tools were belong to non-open source software, which couldn’t join with the real system. This paper used the RBC Sub-system of CTCS-3 as an example, proposed a method based on the XML to implement the reachability analysis of the timed automata model, as a result, it was available to transport data between different development environment, a more feasible methods were put forward to complete the testing platform in both theoretical method and practical application.

model checking; CTCS-3; reachability analysis; formal modeling; tested analysis

U284.4∶TP39

：A

1005-8451（2014）06-0010-06

2013-12-20

國(guó)際863計(jì)劃項(xiàng)目（2012AA112800）；軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室（北京交通大學(xué)）開(kāi)放課題基金資助（RCS2011K010）；中央高校基本科研業(yè)務(wù)費(fèi)專(zhuān)項(xiàng)資金資助（2012JBM024）。

宋海鋒，在讀碩士研究生；唐 濤，教授。