一種基于時(shí)間自動機(jī)模型的區(qū)域控制器測試序列生成方法

宋 爽，劉伯鴻，周 科，陳躍東

(1.蘭州交通大學(xué)自動化與電氣工程學(xué)院，蘭州 730070；2.深圳熙斯特新能源技術(shù)有限公司，深圳 518118)

城市軌道交通采用基于通信的列車控制系統(tǒng)(Communication Based Train Control，CBTC)，通過精確的定位技術(shù)和高速、實(shí)時(shí)的通信技術(shù)實(shí)現(xiàn)對列車的控制，使列車可以以較短的追蹤間隔安全運(yùn)行。區(qū)域控制器(Zone Controller，ZC)作為CBTC系統(tǒng)的核心設(shè)備，在投入運(yùn)營前必須進(jìn)行一系列的測試。目前，CBTC系統(tǒng)功能測試仍以人工的方式編排測試序列，耗時(shí)長、執(zhí)行效率低且很難做到完備性測試，系統(tǒng)可靠性及安全性無法得到徹底保證。因此有必要對區(qū)域控制器測試序列的自動生成方法進(jìn)行研究。

形式化模型因其具有語義精確的優(yōu)點(diǎn)，可以很好地被計(jì)算機(jī)系統(tǒng)識別，近幾年出現(xiàn)了許多由形式化模型自動生成測試案例的方法。文獻(xiàn)[1-2]采用UML建模方法，對列控系統(tǒng)測試序列生成方法進(jìn)行研究；文獻(xiàn)[3]用Java語言實(shí)現(xiàn)由Event-B規(guī)范模型自動生成測試案例；北京交通大學(xué)基于CTCS-3級列控系統(tǒng)的時(shí)間自動機(jī)模型對測試案例自動生成方法進(jìn)行研究[4-6]；文獻(xiàn)[7]基于CBTC車載系統(tǒng)的因果圖研究了測試案例的生成方法。

研究對象的不同很大程度上決定了建模方法的差異，由于區(qū)域控制器的控制決策對時(shí)間要求嚴(yán)格，故本文利用時(shí)間自動機(jī)理論對實(shí)時(shí)系統(tǒng)建模與驗(yàn)證的優(yōu)越性，研究了測試序列的自動生成方法[8-12]。

1 時(shí)間自動機(jī)及驗(yàn)證工具UPPAAL

1.1 時(shí)間自動機(jī)理論

時(shí)間自動機(jī)(Timed Automata)是一個(gè)六元組T=〈S，S0，∑，X，I，E〉，其中:

(1)S是有限位置集合;

(2)S0是初始位置集合;

(3)∑是有限事件集合;

(4)X是有限時(shí)鐘集合;

(5)I是一個(gè)映射，它給每個(gè)位置s∈S指定Ф(х)中的一個(gè)時(shí)鐘約束δ;

(6)E?S×∑×Ф(х)×2х×S，為狀態(tài)轉(zhuǎn)移的集合。

一個(gè)轉(zhuǎn)換〈s，，δ，λ，s′〉表示輸入事件a(a∈∑)的發(fā)生時(shí)間滿足時(shí)鐘約束δ時(shí)，時(shí)間自動機(jī)從狀態(tài)s轉(zhuǎn)移到狀態(tài)s′，轉(zhuǎn)換完成后，將相應(yīng)的時(shí)鐘重置為0，λ?X表示需要重置時(shí)鐘的集合[13-15]。

1.2 UPPAAL

UPPAAL是以時(shí)間自動機(jī)理論為基礎(chǔ)建立模型并對模型性質(zhì)進(jìn)行分析驗(yàn)證的工具，主要由編輯器、模擬器和驗(yàn)證器3部分組成。用戶可以在UPPAAL中聲明通道、時(shí)鐘、變量以及約束條件。通道聲明(Chanb)將某一時(shí)刻的發(fā)送器和接收器聯(lián)系在一起，只有接收動作b？發(fā)生時(shí)，發(fā)送動作b!才能發(fā)生[15]。變量和通道可以實(shí)現(xiàn)不同模型的通信，將幾個(gè)簡單模型連接成復(fù)雜的系統(tǒng)模型。

1.3 BNF語法

為保證驗(yàn)證過程的標(biāo)準(zhǔn)性和驗(yàn)證結(jié)果的準(zhǔn)確性，UPPAAL為驗(yàn)證器提供了BNF需求規(guī)范語法：

Prop::=E< >p|A[ ]p|E[ ]p|A< >p|p→q。

字符E和A用來量化路徑，E表示至少有1條路徑滿足給定的性質(zhì)p，A表示給定的性質(zhì)p對于所有的路徑均滿足；符號< >和[ ]用來量化路徑上的狀態(tài)，< >表示路徑上至少有1個(gè)狀態(tài)滿足給定的性質(zhì)，[ ]表示路徑上的所有狀態(tài)均滿足給定的性質(zhì)[15]，p->q表示p正確，終究可以使得q正確。BNF語義如圖1所示。

圖1 BNF語義示意

2 區(qū)域控制器及測試系統(tǒng)

CBTC系統(tǒng)分為地面設(shè)備和車載設(shè)備兩部分，區(qū)域控制器設(shè)置于設(shè)備集中站，是CBTC系統(tǒng)的地面核心設(shè)備，負(fù)責(zé)管理其管轄范圍內(nèi)的所有通信列車。區(qū)域控制器的主要功能可劃分為列車管理、移動授權(quán)分配、區(qū)域控制器切換、與CBTC其他子系統(tǒng)的信息交互以及故障處理[14]。

列車管理是指ZC對管轄范圍內(nèi)列車的運(yùn)行狀態(tài)進(jìn)行管理，監(jiān)控列車的控制模式，記錄列車的車次號、運(yùn)行方向、運(yùn)行狀態(tài)、緊急制動信息等。移動授權(quán)(Movement Authority，MA)是由ZC為其管轄范圍內(nèi)的通信列車提供的從車尾到運(yùn)行前方第一個(gè)禁止通過的障礙物的距離，車載控制器根據(jù)移動授權(quán)信息和列車制動性能生成速度-距離曲線，控制列車運(yùn)行。ZC切換是指列車運(yùn)行到本ZC與相鄰ZC的控制區(qū)域重疊處時(shí)，列車控制權(quán)在無司機(jī)干涉的情況下平滑無縫的從本ZC移交給相鄰ZC的過程。區(qū)域控制器與其他子系統(tǒng)的信息交互是區(qū)域控制器其他功能實(shí)現(xiàn)的基礎(chǔ)，區(qū)域控制器與其他子系統(tǒng)信息交互流如圖2所示。故障處理指ZC對管轄范圍內(nèi)的列車出現(xiàn)故障后的處理策略[16]。

圖2 區(qū)域控制器信息流

仿真測試平臺是進(jìn)行實(shí)驗(yàn)室測試的前提條件，測試系統(tǒng)主要由人機(jī)界面、測試序列生成模塊、結(jié)果記錄及查詢模塊和數(shù)據(jù)庫模塊構(gòu)成，如圖3所示。人機(jī)界面主要功能有：測試功能配置、限速信息配置、障礙物信息配置、測試功能顯示、測試結(jié)果顯示。測試序列生成模塊從人機(jī)界面獲取所測試功能，生成測試序列，并從數(shù)據(jù)庫讀取相關(guān)數(shù)據(jù)賦予測試序列。結(jié)果記錄及查詢模塊用于記錄被測區(qū)域控制器對測試的響應(yīng)，便于后期數(shù)據(jù)查詢[17]。

圖3 測試系統(tǒng)結(jié)構(gòu)

3 測試序列生成

測試序列的生成是通過解析時(shí)間自動機(jī)模型文件，提取其中的對象、狀態(tài)和變遷信息，生成測試案例，并將其以鏈表結(jié)構(gòu)的形式存儲，然后按照功能特征將測試案例串接成為測試序列的過程。

3.1 模型文件解析

由UPPAAL建立的時(shí)間自動機(jī)模型文件為標(biāo)準(zhǔn)的XML格式標(biāo)記文本，TinyXML是C++編寫的一個(gè)開源的XML文件的解析庫，通過TinyXML中對象類庫可以很方便地遍歷模型文件信息。在TinyXML中，根據(jù)XML文件格式中的各種結(jié)構(gòu)元素，定義了一些對應(yīng)的對象類。

TiXmlBase：對應(yīng)整個(gè)模型文件的基類；

TiXmlAttribute：對應(yīng)模型文件中元素的屬性；

TiXmlNode：對應(yīng)于DOM結(jié)構(gòu)中的節(jié)點(diǎn)；

TiXmlComment：對應(yīng)于模型文件中的注釋；

TiXmlDeclaration：對應(yīng)于模型文件中的申明部分；

TiXmlDocument：對應(yīng)于模型文件的整個(gè)文檔；

TiXmlElement：對應(yīng)于模型文件中的元素；

TiXmlText：對應(yīng)于模型文件的文字部分；

TiXmlUnknown：對應(yīng)于模型文件的未知部分；

TiXmlHandler：定義了針對模型文件的一些操作。

編寫MFC應(yīng)用程序，利用TinyXML解析該模型文件，信息提取的部分代碼如下[18]。

TiXmlDocument->Parse(buffer);//將文件存入緩存區(qū)buffer

locationNodexml.id=locationElement->Attribute("id");//讀取狀態(tài)信息id號

locationNodexml.idName=nameElement->GetText( );//讀取狀態(tài)信息名稱

transitionNodexml.source_ref=transitionElement->Attribute("ref");//讀取變遷起始狀態(tài)

transitionNodexml.target_ref=transitionElement->Attribute("ref");//讀取變遷結(jié)束狀態(tài)

transitionNodexml.kind=transitionElement->Attribute("kind");//讀取變遷條件類型

transitionNodexml.labelName=transitionElement->GetText( );//讀取變遷條件信息

XmlInfoContent.push_back( );//將獲得的信息存入容器中

3.2 測試序列的生成

測試序列是測試某一功能時(shí)用到的一串連續(xù)的測試案例。遍歷存儲測試案例的容器，將符合要求的測試案例首尾相連構(gòu)成測試序列，測試案例在串接時(shí)應(yīng)滿足[19]：

(1)包含在初始狀態(tài)和結(jié)束狀態(tài)之間的狀態(tài)變遷都要被覆蓋到；

(2)前一測試案例的結(jié)束狀態(tài)和后一測試案例的起始狀態(tài)相同；

(3)測試序列中的測試案例應(yīng)滿足最小重復(fù)度。

由于區(qū)域控制器模型中狀態(tài)轉(zhuǎn)換大部分是單入度和單出度的，因此可采用深度優(yōu)先搜索，借助重復(fù)路徑標(biāo)記使測試案例的重復(fù)性最小，串接算法流程如圖4所示。

圖4 測試案例串接流程

測試序列生成的部分代碼如下：

itr=m_ComboMap.begin();//存儲測試案例的起始地址

while(itr!=m_ComboMap.end())

{

if (itr->first==strBegin)

{

strBegin0[i]=strBegin;

strEnd0[i++]=itr->second;

}

itr++;

}//存儲所有起始狀態(tài)與測試初始狀態(tài)相同的測試案例

str.Format(_T("%s->%s;")，strBegin1，strEnd1);//遇到可以連接的測試案例時(shí)，將str設(shè)置為測試案例狀態(tài)轉(zhuǎn)換格式“起始狀態(tài)->結(jié)束狀態(tài)”

strTemp+=str;//案例連接

strBegin=strEnd1;//將本測試案例的結(jié)束狀態(tài)作為下一個(gè)測試案例的起始狀態(tài)

if((strBegin==strEnd)&&Flag)

ShowInfo(strTemp); //當(dāng)起始狀態(tài)和結(jié)束狀態(tài)相同且過程中的多出度狀態(tài)測試案例全部被串接時(shí)，顯示測試序列

4 實(shí)例驗(yàn)證

以區(qū)域控制器切換為例證明該測試序列生成方法的有效性。

4.1 ZC切換過程建模

列車在某一時(shí)刻僅受其占用區(qū)間的區(qū)域控制器控制，當(dāng)列車經(jīng)過切換預(yù)告應(yīng)答器時(shí)，進(jìn)入本ZC與相鄰ZC的控制區(qū)域重疊處，觸發(fā)ZC切換流程。ZC切換分為以下步驟。

(1)當(dāng)列車在移交ZC控制下到達(dá)切換預(yù)告應(yīng)答器時(shí)，車載控制器(VOBC)將自己的位置信息發(fā)送給移交ZC，觸發(fā)切換流程。移交ZC向接管ZC發(fā)送連接申請，通信連接建立后，移交ZC將列車信息(車次號、運(yùn)行方向、列車位置、運(yùn)行模式等)發(fā)送給接管ZC，進(jìn)行MA擴(kuò)展。接管ZC接收到列車信息后，檢查列車進(jìn)路信息，如果列車進(jìn)路已經(jīng)排列，生成擴(kuò)展MA(MA2)，并將其發(fā)送給移交ZC。移交ZC將本區(qū)域的MA1與收到的MA2整合，生成混合MA發(fā)送給列車，控制列車運(yùn)行。

(2)當(dāng)列車前端到達(dá)切換應(yīng)答器時(shí)，VOBC根據(jù)從移交ZC獲取的接管ZC的ID號等信息與接管ZC建立通信連接。而此時(shí)VOBC僅與接管ZC保持通信連接，列車的控制權(quán)仍在移交ZC。此過程是接管區(qū)域控制器對列車的預(yù)接管過程。

(3)當(dāng)列車后端通過切換應(yīng)答器時(shí)，VOBC向移交ZC發(fā)送位置信息，移交ZC接收到后注銷列車信息并斷開與VOBC的通信連接。同時(shí)VOBC向接管ZC發(fā)送登錄請求信息，登錄接管ZC后，接管ZC正式管轄該列車，切換過程結(jié)束[20]。

ZC切換過程涉及到的對象有移交ZC、接管ZC和列車，分析該過程的信息交互流程，分別對單個(gè)對象建立時(shí)間自動機(jī)模型，并在單個(gè)時(shí)間自動機(jī)模型的基礎(chǔ)上添加并行組合和約束條件，構(gòu)成時(shí)間自動機(jī)的積，以保證系統(tǒng)各成員之間的信息交互。針對ZC切換過程建立的時(shí)間自動機(jī)模型如圖5所示。

4.2 模型正確性驗(yàn)證

從區(qū)域控制器的需求分析提取切換過程應(yīng)滿足的功能性和實(shí)時(shí)性要求，并用BNF語言描述，如表1所示。

建立的模型必須滿足這些特定的功能性和實(shí)時(shí)性要求，以保證系統(tǒng)的安全性和受限活性，將以上性質(zhì)輸入驗(yàn)證器中，驗(yàn)證結(jié)果如圖6所示。

4.3 測試序列的生成

測試主要目的是發(fā)現(xiàn)產(chǎn)品的缺陷，給產(chǎn)品質(zhì)量水平做出盡可能準(zhǔn)確的評估，保證產(chǎn)品質(zhì)量。測試過程的細(xì)分有助于快速定位缺陷的位置。

編寫MFC應(yīng)用程序，提取模型文件信息，將變遷的起始狀態(tài)、結(jié)束狀態(tài)，及其對應(yīng)的約束條件進(jìn)行組合，生成符合測試規(guī)則的測試案例。基于故障定位的思想，將測試功能細(xì)分，選擇相應(yīng)的測試初始狀態(tài)、結(jié)束狀態(tài)，自動串接測試案例，生成測試序列，如圖7所示。

表1 模型應(yīng)該滿足的性質(zhì)列表

圖5 ZC切換時(shí)間自動機(jī)模型

圖6 性質(zhì)驗(yàn)證結(jié)果

圖7 ZC切換測試序列

圖7上半部分主要是從模型文件中獲取的信息，上左為建模對象信息及其所對應(yīng)的狀態(tài)信息，上右為變遷信息，即測試案例。測試案例中條件數(shù)據(jù)后面的符號“？”表示向被測對象發(fā)送該數(shù)據(jù)包，“!”表示被測對象輸出該數(shù)據(jù)包。圖7下半部分是測試序列信息，測試功能選擇欄中可以給測試功能添加描述，方便測試功能的選取及日后查找，測試序列欄顯示了功能特征對應(yīng)的測試序列。

以“列車尾部越過切換應(yīng)答器，由接管ZC向列車發(fā)送MA控制列車運(yùn)行”的測試為例，一個(gè)測試序列共包含5個(gè)狀態(tài)，5個(gè)測試案例，如表2所示。

在測試過程中，測試序列生成模塊從數(shù)據(jù)庫模塊獲取測試序列中用到的數(shù)據(jù)包，測試系統(tǒng)按照測試序列中測試案例的串接順序，通過測試用通信接口向被測區(qū)域控制器發(fā)送測試數(shù)據(jù)，并將被測對象的輸出響應(yīng)送給測試序列生成模塊。測試序列生成模塊將被測區(qū)域控制器的輸出與標(biāo)準(zhǔn)輸出比較，判斷測試結(jié)果的正確性，并將測試結(jié)果送給結(jié)果記錄與查詢模塊進(jìn)行記錄。

表2 測試序列

5 結(jié)語

針對CBTC系統(tǒng)現(xiàn)有測試序列生成方法的不足，在實(shí)驗(yàn)室仿真測試的基礎(chǔ)上，基于測試系統(tǒng)正常工作的前提下，結(jié)合時(shí)間自動機(jī)理論研究了測試序列自動生成的方法。通過性質(zhì)驗(yàn)證，在保證模型正確性的前提下，利用TinyXML解析庫對模型文件解析，提取有效信息，并生成測試序列，通過區(qū)域控制器切換功能的測試序列生成證明該方法的有效性。利用UPPAAL對模型正確性進(jìn)行驗(yàn)證，保證了測試案例的正確性，全變遷覆蓋原則保證了測試序列的完備性，另外，此測試序列生成方法具有普遍性，可根據(jù)不同的測試對象更改模型配置和數(shù)據(jù)庫配置，以生成不同測試對象的測試序列。