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

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

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

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

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

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

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

時(shí)間自動(dòng)機(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í)間自動(dòng)機(jī)從狀態(tài)s轉(zhuǎn)移到狀態(tài)s′，轉(zhuǎn)換完成后，將相應(yīng)的時(shí)鐘重置為0，λ?X表示需要重置時(shí)鐘的集合[13-15]。

1.2 UPPAAL

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

1.3 BNF語(yǔ)法

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

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

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

圖1 BNF語(yǔ)義示意

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

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

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

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

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

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

3 測(cè)試序列生成

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

3.1 模型文件解析

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 測(cè)試序列的生成

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

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

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

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

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

圖4 測(cè)試案例串接流程

測(cè)試序列生成的部分代碼如下：

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

while(itr!=m_ComboMap.end())

{

if (itr->first==strBegin)

{

strBegin0[i]=strBegin;

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

}

itr++;

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

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

strTemp+=str;//案例連接

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

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

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

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

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

4.1 ZC切換過(guò)程建模

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

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

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

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

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

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

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

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

4.3 測(cè)試序列的生成

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

編寫(xiě)MFC應(yīng)用程序，提取模型文件信息，將變遷的起始狀態(tài)、結(jié)束狀態(tài)，及其對(duì)應(yīng)的約束條件進(jìn)行組合，生成符合測(cè)試規(guī)則的測(cè)試案例?；诠收隙ㄎ坏乃枷?，將測(cè)試功能細(xì)分，選擇相應(yīng)的測(cè)試初始狀態(tài)、結(jié)束狀態(tài)，自動(dòng)串接測(cè)試案例，生成測(cè)試序列，如圖7所示。

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

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

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

圖7 ZC切換測(cè)試序列

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

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

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

表2 測(cè)試序列

5 結(jié)語(yǔ)

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