易承龍，李開成，周晶晶

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

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

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

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

2 時(shí)間自動(dòng)機(jī)及Cover簡(jiǎn)介

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

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

3 基于UPPAAL的列車運(yùn)行場(chǎng)景建模

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

3.1 列車注冊(cè)與啟動(dòng)場(chǎng)景介紹

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

圖1 注冊(cè)場(chǎng)景流程圖

圖2 啟動(dòng)場(chǎng)景流程圖

3.2 列車注冊(cè)與啟動(dòng)場(chǎng)景建模與驗(yàn)證

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

3.2.1 司機(jī)模型

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

圖3 司機(jī)模型

司機(jī)模型的時(shí)間自動(dòng)機(jī)定義為：

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模型

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

圖4 EVC模型

3.2.3 RBC模型

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

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

圖5 RBC模型

1)功能要求。

A[] not deadlock

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

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

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

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

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

2)性能要求。

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

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

PosRepPeriod

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

A[]VC.EditonJudgeStu imply ConnectNum <=TryToConNo

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

A[] VC.EditonJudgeStu imply T_Con <=T_NVCONTACT

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

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

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

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

4.1 基于模型的測(cè)試原理

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

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

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

4.2.1 Cover工具配置

在用Cover自動(dòng)生成測(cè)試序列之前，必須對(duì)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工具選擇生成哪個(gè)時(shí)間自動(dòng)機(jī)模型的測(cè)試?yán)?，其語法結(jié)構(gòu)形式如下：

CoveredgeObs({P1,P2})

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

4.2.2 測(cè)試用例的自動(dòng)生成

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

·Trace #1:

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN……

可以將以上所生成的抽象狀態(tài)轉(zhuǎn)移語言轉(zhuǎn)換具體的狀態(tài)轉(zhuǎn)移圖，這樣所生成的測(cè)試用例的消息序列為：“初始狀態(tài)”—“待機(jī)狀態(tài)”—“準(zhǔn)備建立連接狀態(tài)”—“等待消息32狀態(tài)”—“判斷連接是否超時(shí)狀態(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ā)送列車位置報(bào)告狀態(tài)”。

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

5 結(jié)束語

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

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

[2]王超琦.CTCS-3級(jí)列控系統(tǒng)車載設(shè)備測(cè)試序列的生成方法及工具研究[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級(jí)列控系統(tǒng)測(cè)試案例優(yōu)化生成方法研究[D].北京：北京交通大學(xué)， 2010:16-17.

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

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

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

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

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