基于模型的車載設備測試用例自動生成研究

易承龍，李開成，周晶晶

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

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

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

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

2 時間自動機及Cover簡介

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

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

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

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

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

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

圖1 注冊場景流程圖

圖2 啟動場景流程圖

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

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

3.2.1 司機模型

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

圖3 司機模型

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

TA=

初始位置L0= {DriverInActivity};

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

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

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

3.2.2 EVC模型

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

圖4 EVC模型

3.2.3 RBC模型

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

由于篇幅有限就不再羅列EVC、RBC自動機模型的位置集合、事件集合等信息。列車注冊與啟動場景模型建立完成后，利用UPPAAL軟件自帶的模擬器檢查是否有語法錯誤。在通過語法編譯后，點擊自動運行按鈕，通過比較發(fā)現(xiàn)運行結果與規(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))

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

2)性能要求。

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

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

PosRepPeriod

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

A[]VC.EditonJudgeStu imply ConnectNum <=TryToConNo

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

A[] VC.EditonJudgeStu imply T_Con <=T_NVCONTACT

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

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

4 車載設備測試用例的自動生成

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

4.1 基于模型的測試原理

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

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

4.2 車載設備測試用例的自動生成

4.2.1 Cover工具配置

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

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

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

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

Observer.obs文件用于描述覆蓋標準算法。其使用非常靈活，具體語法結構形式如下所示，以下所描述的為全位置覆蓋標準。

observerObserver(procid P; )

{

node edgeNode(edgeid);

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

accepting edgeNode;

}

Property.q文件用于配置Cover工具選擇生成哪個時間自動機模型的測試例，其語法結構形式如下：

CoveredgeObs({P1,P2})

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

4.2.2 測試用例的自動生成

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

·Trace #1:

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN……

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

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

5 結束語

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

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

[2]王超琦.CTCS-3級列控系統(tǒng)車載設備測試序列的生成方法及工具研究[D].北京: 北京交通大學,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].北京：北京交通大學， 2010:16-17.

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

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

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

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

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