易承龍，李開成，周晶晶

(北京交通大學(xué)軌道交通運行控制系統(tǒng)國家工程研究中心，北京 100044)

2004年，鐵道部提出“四橫四縱”鐵路快速客運專線網(wǎng)建設(shè)規(guī)劃，從此啟動了中國高速鐵路發(fā)展計劃。隨著鐵路事業(yè)的快速發(fā)展，列控系統(tǒng)的安全性也成為了人們關(guān)注的焦點[1]。作為列控系統(tǒng)核心的車載設(shè)備在正式使用前必須進(jìn)行全面測試，測試的基礎(chǔ)是測試用例的生成。目前，車載設(shè)備測試用例是根據(jù)專家經(jīng)驗通過啟發(fā)的方式得到，這種方式既耗時，又不能保證測試用例的覆蓋度[2]；因此，有必要在保證測試覆蓋度的前提下將測試用例的生成過程自動化。

1 列控系統(tǒng)車載設(shè)備測試現(xiàn)狀

現(xiàn)階段，CTCS-3級車載設(shè)備的測試是通過系統(tǒng)既有的外部接口進(jìn)行功能測試，采用的是黑盒測試及主動測試方法[3]。功能測試由系統(tǒng)功能需求規(guī)范提取出功能特征，依據(jù)功能特征編寫測試用例，然后由測試用例串聯(lián)成測試序列[3-5]。 目前，由功能特征設(shè)計測試用例的過程主要由手工完成，測試的效率低、耗時長，并且隨著測試規(guī)范和測試目的的改變，測試工作量增大。測試用例編寫人員需要對系統(tǒng)深入了解，并且具備豐富的測試經(jīng)驗，即使這樣在測試用例的編寫過程中也難免有所遺漏。顯然，使用這種方法編寫的車載設(shè)備測試用例往往難以保證測試質(zhì)量，因此有必要將測試用例生成的過程模型化、自動化。國內(nèi)外眾多專家的研究表明基于時間自動機模型的測試可以有效地提高車載設(shè)備的測試效率[6]。

2 時間自動機及Cover簡介

時間自動機是由R.Alur和D.Dill提出的，作為實時系統(tǒng)建模的方法，它為實時系統(tǒng)建模提供了快速易用的形式化方法[7]。首先，時間自動機引入了系統(tǒng)在某些狀態(tài)之間的轉(zhuǎn)移，這些狀態(tài)用位置元素來表示。其次，時間自動機在有限狀態(tài)機的基礎(chǔ)上引入了時間變量，這不僅可以記錄模型狀態(tài)轉(zhuǎn)移間所消耗的時間，同樣可用作判定是否應(yīng)該發(fā)生狀態(tài)轉(zhuǎn)移的條件。

Cover是一個基于模型的實時系統(tǒng)測試用例自動生成工具，由Uppsala大學(xué)開發(fā)并于2005年推出，它有一個表達(dá)能力很強的observer語言，可以用來描述一大類覆蓋準(zhǔn)則，包括結(jié)構(gòu)準(zhǔn)則(如位置或邊覆蓋)、數(shù)據(jù)流準(zhǔn)則(如定義使用對和語義覆蓋等)，能夠?qū)崿F(xiàn)從時間自動機模型到基于覆蓋度算法的測試用例套的自動轉(zhuǎn)換[8]。

3 基于UPPAAL的列車運行場景建模

車載設(shè)備是一個典型的實時系統(tǒng)，系統(tǒng)的安全性要求系統(tǒng)不僅要做出正確的響應(yīng)，還必須在規(guī)定的時間內(nèi)做出響應(yīng)。此外，列控系統(tǒng)出現(xiàn)故障之后，能否在規(guī)定的時間內(nèi)實現(xiàn)“故障-安全”也是關(guān)系列車安全運行的關(guān)鍵因素，因而列控系統(tǒng)的時間特性可以由時間自動機模型很好地反映。本文運用時間自動機理論形式化描述列控系統(tǒng)注冊與啟動場景，并從功能要求和性能要求2方面對模型進(jìn)行驗證。

3.1 列車注冊與啟動場景介紹

注冊與啟動場景[9]描述的是列車從站內(nèi)或區(qū)間車載設(shè)備從停止?fàn)顟B(tài)開始，依次經(jīng)過設(shè)備上電、激活并開啟駕駛臺、輸入列車數(shù)據(jù)、具備發(fā)車條件至列車啟動時信號系統(tǒng)的整個工作流程。其工作流程如圖1、圖2所示。

圖1 注冊場景流程圖

圖2 啟動場景流程圖

3.2 列車注冊與啟動場景建模與驗證

通過以上對系統(tǒng)流程的分析，注冊與啟動場景關(guān)系到司機、EVC和RBC之間的信息交互，所以需要使用UPPAAL分別對司機、EVC和RBC建立時間自動機模型。

3.2.1 司機模型

在列車注冊與啟動場景中司機扮演重要角色，EVC通過DMI與司機進(jìn)行交互，提示司機輸入信息或進(jìn)行確認(rèn)，其UPPAAL模型如圖3所示。

圖3 司機模型

司機模型的時間自動機定義為：

TA=

初始位置L0= {DriverInActivity};

位置集合L={DriverInActivity,DriverActivity, WaitToConRBC,ConToRbcReady,ReadyToGo,Go}

事件集合A={InputDriverID , InputDriverIDReady, EVCConWithRbc, TurnToC2SOM, InputVCData, InputVCDataReady, ReadyToStart……

狀態(tài)轉(zhuǎn)移E={,,

3.2.2 EVC模型

在列車注冊與啟動場景中，EVC邏輯最為復(fù)雜，它需要同時與RBC和司機進(jìn)行交互，其UPPAAL模型如圖4所示。

圖4 EVC模型

3.2.3 RBC模型

在列車注冊與啟動場景中，RBC負(fù)責(zé)與EVC進(jìn)行信息交互，RBC功能的正確是列車行車安全的保障，其UPPAAL模型如圖5所示。

由于篇幅有限就不再羅列EVC、RBC自動機模型的位置集合、事件集合等信息。列車注冊與啟動場景模型建立完成后，利用UPPAAL軟件自帶的模擬器檢查是否有語法錯誤。在通過語法編譯后，點擊自動運行按鈕，通過比較發(fā)現(xiàn)運行結(jié)果與規(guī)范中的流程圖完全一致，整個模型所完成的功能和性能要求如下：

圖5 RBC模型

1)功能要求。

A[] not deadlock

系統(tǒng)沒有死鎖；

E<>((VC.VCWaitM3)and(RBC.RBCWaitM132))

RBC能定時接受車載發(fā)送的MA請求并向車載發(fā)送最新MA；

E<>((VC.VCWaitM24)and(RBC.RBCWaitM136))

車載設(shè)備能定時向RBC發(fā)送列車實時位置信息并收到RBC回復(fù)。

2)性能要求。

A[] VC.VCWaitM3 imply T_MaReq >MAReqPer-iod

車載設(shè)備周期向RBC發(fā)送請求MA；A[]VC.VCWaitM24 imply T_PositionReport >

PosRepPeriod

車載設(shè)備周期向RBC發(fā)送位置報告信息；

A[]VC.EditonJudgeStu imply ConnectNum <=TryToConNo

車載設(shè)備與RBC建立安全連接嘗試呼叫的次數(shù)小于3次；

A[] VC.EditonJudgeStu imply T_Con <=T_NVCONTACT

車載設(shè)備與RBC建立安全連接時間不超過60 s。

在UPPAAL軟件驗證器中執(zhí)行上述驗證語句，結(jié)果顯示上面所描述的性質(zhì)都能通過，表明系統(tǒng)滿足這些性質(zhì)，模型是安全正確的，這為后面測試用例自動生成提供了正確的前提。

4 車載設(shè)備測試用例的自動生成

本文首先介紹了基于模型測試的原理和過程，然后引入基于覆蓋度算法的輔助軟件Cover，自動生成了車載設(shè)備的測試用例。

4.1 基于模型的測試原理

首先敘述一個事實：基于模型的測試序列自動生成方法應(yīng)用的前提條件是假設(shè)系統(tǒng)是TITOS系統(tǒng)，也就是說對于每一個測試用例的輸入，系統(tǒng)都有一個對應(yīng)于系統(tǒng)詳細(xì)設(shè)計中所描述的明確輸出，車載設(shè)備滿足這個條件。假設(shè)系統(tǒng)A是實時系統(tǒng)，它由2個部分組成，分別是系統(tǒng)模型S和系統(tǒng)所在的環(huán)境E。時間自動機在運轉(zhuǎn)時，組成系統(tǒng)的各個部件在時鐘約束的條件下從一個狀態(tài)到達(dá)另一個狀態(tài)形成一條序列，而特征軌跡就是序列的集合。利用UPPAAL對可達(dá)性問題分析產(chǎn)生的特征軌跡可用以下數(shù)學(xué)公式表達(dá)：

其中：si和ei分別是系統(tǒng)模型S和運行環(huán)境模型E的狀態(tài)；ri是時間延遲或者其他同步動作。系統(tǒng)延遲和其他同步動作組成了測試用例中的事件因子，因此從特征軌跡到測試用例的轉(zhuǎn)換，最簡單的方法就是通過將特征軌跡映射到系統(tǒng)環(huán)境模型E中，疊加相關(guān)聯(lián)的系統(tǒng)延遲，去掉不可見的轉(zhuǎn)換過程，最后，將要在真實環(huán)境中執(zhí)行的測試用例引入判決。其判決過程可以解釋如下：時間自動機中某個狀態(tài)用一個Bool類型變量標(biāo)識，可以標(biāo)識Pass和Fail狀態(tài)，如果測試序列不能執(zhí)行到這個狀態(tài)，那么他將被標(biāo)識為Fail狀態(tài)，如果能執(zhí)行經(jīng)過這個狀態(tài)，他將被標(biāo)識為Pass狀態(tài)。

4.2 車載設(shè)備測試用例的自動生成

4.2.1 Cover工具配置

在用Cover自動生成測試序列之前，必須對Cover進(jìn)行相應(yīng)的配置，相關(guān)配置參數(shù)如表1所示。

表1 Cover工具配置參數(shù)

Cover工具需要輸入Model.xml文件、Observer.obs文件和Property.q文件。

Model.xml文件即上一節(jié)使用UPPAAAL軟件建模所生成的文件，需要拷貝到Cover工具所在的根目錄下。

Observer.obs文件用于描述覆蓋標(biāo)準(zhǔn)算法。其使用非常靈活，具體語法結(jié)構(gòu)形式如下所示，以下所描述的為全位置覆蓋標(biāo)準(zhǔn)。

observerObserver(procid P; )

{

node edgeNode(edgeid);

rulestartto edgeNode(E)with E :=edge(P);

accepting edgeNode;

}

Property.q文件用于配置Cover工具選擇生成哪個時間自動機模型的測試?yán)?，其語法結(jié)構(gòu)形式如下：

CoveredgeObs({P1,P2})

在這里，時間自動機過程集為{P1,P2}，也就是說P1和P2會分別代入Observer文件中的procid P進(jìn)行運算。

4.2.2 測試用例的自動生成

根據(jù)上一節(jié)描述的配置方法配置Cover工具，并將XML格式的注冊與啟動場景的UPPAAL模型和使用全位置覆蓋標(biāo)準(zhǔn)算法的Observer.obs文件拷貝到Cover程序所在的文件夾的根目錄，運行Cover工具。將生成的測試案例用例保存在abc.tr文件中，運行結(jié)果表明共生成了7個測試案例。下面以Trace#1為例，介紹所生成的抽象語言描述的具體含義。Trace#1的具體描述如下：

·Trace #1:

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN……

可以將以上所生成的抽象狀態(tài)轉(zhuǎn)移語言轉(zhuǎn)換具體的狀態(tài)轉(zhuǎn)移圖，這樣所生成的測試用例的消息序列為：“初始狀態(tài)”—“待機狀態(tài)”—“準(zhǔn)備建立連接狀態(tài)”—“等待消息32狀態(tài)”—“判斷連接是否超時狀態(tài)”—“判斷系統(tǒng)版本狀態(tài)”—“建立連接狀態(tài)”—“等待配置參數(shù)狀態(tài)”—“等待輸入列車數(shù)據(jù)狀態(tài)”—“等待列車數(shù)據(jù)確認(rèn)狀態(tài)”—“等待發(fā)車狀態(tài)”—“正常工作狀態(tài)”—“等待行車許可狀態(tài)”—“發(fā)送列車位置報告狀態(tài)”。

通過對比《CTCS-3級列控系統(tǒng)測試案例》中功能特征47的測試案1的基本信息和測試步驟，可以發(fā)現(xiàn)，其所描述的事件與Cover工具所生產(chǎn)的Trace#1相吻合。由上面的案例可知，利用時間自動機建模不僅可以驗證模型的可達(dá)性，還可以通過搜索路徑生成覆蓋度完整的測試用例，并且可以通過配置Cover工具搜索算法改變測試用例的路徑選擇。

5 結(jié)束語

傳統(tǒng)的車載系統(tǒng)功能測試用例生成主要依靠專家經(jīng)驗手工編制完成，測試的主觀性強、效率低、耗時長，并且隨著測試規(guī)范和測試目的的改變，測試工作量大，而且測試的覆蓋度無法得到滿足。本文提出了一種基于模型的車載系統(tǒng)安全測試用例自動生成方法，使用UPPAAL軟件對列車注冊與啟動運營場景進(jìn)行建模，并從功能和性能2方面對所建立的模型進(jìn)行了驗證，最后運用基于覆蓋度的工具Cover自動生成車載設(shè)備測試用例，這為復(fù)雜時變系統(tǒng)測試用例的自動生成提出了一種新的思路。

[1]唐濤. 高速鐵路列車運行控制系統(tǒng)車載設(shè)備安全性設(shè)計[J]. 北方交通大學(xué)學(xué)報,1999:23(5):83-87.

[2]王超琦.CTCS-3級列控系統(tǒng)車載設(shè)備測試序列的生成方法及工具研究[D].北京: 北京交通大學(xué),2010:5-27.

[3]Beizer B . Black-Box Testing: Techniques for Functional Testing of SoftWare and Systems[M]. New York:John Wiley & Sons:1995:160-165.

[4]王倩倩.CTCS-3級列控系統(tǒng)測試案例優(yōu)化生成方法研究[D].北京：北京交通大學(xué)， 2010:16-17.

[5]章慧.CTCS-3級列控系統(tǒng)車載設(shè)備測試方法研究[D].北京：北京交通大學(xué)，2007.

[6]范素娟.基于時間自動機模型的測試用例生成方法研究[D].鄭州：鄭州大學(xué)，2010.

[7]Alur R,Dill D L A.Theory of Timed Automata[J]. Theoretical Computer Science,1994,126:183-235.

[8] 范素娟,莊雷.基于時間自動機模型的測試用例生成方法[J]. 計算機工程與設(shè)計,2010(12): 2765-2768.

[9]張曙光.CTCS-3級列控系統(tǒng)總體技術(shù)方案[M].北京:中國鐵道出版社, 2008:6-8.