基于模型的CTCS-3 級(jí)列控系統(tǒng)測(cè)試案例自動(dòng)生成方法

呂繼東， 朱曉琳， 李開(kāi)成， 唐 濤， 王海峰

(1. 北京交通大學(xué)軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心，北京100044;2. 中國(guó)鐵道科學(xué)研究院通信信號(hào)研究所，北京100044;3. 北京交通大學(xué)軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室，北京100044)

作為典型的安全苛求系統(tǒng)，列控系統(tǒng)功能的任何故障都可能造成巨大的生命和財(cái)產(chǎn)損失［1］. 形式化方法和測(cè)試方法是保證列控系統(tǒng)功能正確性的兩個(gè)重要途徑，在列控系統(tǒng)開(kāi)發(fā)生命周期中起著不同的作用.

形式化方法一般用于列控系統(tǒng)開(kāi)發(fā)的前期，已廣泛用于列控系統(tǒng)需求規(guī)范的功能正確性研究［2］.早期列控系統(tǒng)的形式化研究主要使用時(shí)段演算方法(duration calculus，DC)［3］. 然而，時(shí)段演算不能完全滿足列控系統(tǒng)的形式化建模要求，隨著列控系統(tǒng)復(fù)雜度的提高，系統(tǒng)中諸如期限(deadline)、直到…才(wait until)、超時(shí)(time out)等形式化描述存在一 定 的 不足［4］. 進(jìn)程代 數(shù)(process algebra)通過(guò)描述并發(fā)和通信系統(tǒng)為分析離散事件系統(tǒng)提供了結(jié)構(gòu)化方法［5］，其中，HCSP(hybrid communication sequential process)方法是對(duì)CSP(communication sequential process)的一種擴(kuò)展，廣泛應(yīng)用于列控系統(tǒng)功能正確性研究［6］. 一致性測(cè)試是保證系統(tǒng)功能正確性的另一個(gè)重要手段，一般用于列控系統(tǒng)開(kāi)發(fā)的后期.通過(guò)分析被測(cè)系統(tǒng)(system under test，SUT)與其需求規(guī)范之間的關(guān)系，驗(yàn)證系統(tǒng)的功能是否與需求規(guī)范一致［7］. 國(guó)內(nèi)外列控系統(tǒng)功能一致性測(cè)試的研究主要集中在測(cè)試案例生成方法上［8-10］.

CTCS-3 級(jí)列控系統(tǒng)功能復(fù)雜，涵蓋了注冊(cè)與啟動(dòng)、注銷、等級(jí)轉(zhuǎn)換、行車許可、RBC(radio block center)切換、自動(dòng)過(guò)分相、重聯(lián)與摘解、臨時(shí)限速、降級(jí)情況、調(diào)車作業(yè)和特殊進(jìn)路等14 個(gè)典型的運(yùn)營(yíng)場(chǎng)景.運(yùn)營(yíng)場(chǎng)景之間具有順序和并發(fā)等特點(diǎn)(例如，行車許可場(chǎng)景和注冊(cè)與啟動(dòng)場(chǎng)景之間是順序關(guān)系，但與RBC 切換場(chǎng)景是并發(fā)關(guān)系).運(yùn)營(yíng)場(chǎng)景需求規(guī)范中包含了若干個(gè)并發(fā)執(zhí)行和交互的實(shí)時(shí)計(jì)算構(gòu)件，規(guī)定了車載設(shè)備和RBC 設(shè)備接口信息時(shí)序約束［11］.上述研究主要集中在列控系統(tǒng)單個(gè)運(yùn)營(yíng)場(chǎng)景時(shí)序約束行為的正確性上，對(duì)整個(gè)列控系統(tǒng)層次的建模描述鮮有研究;并且不同運(yùn)營(yíng)場(chǎng)景存在不同的時(shí)序約束(例如超時(shí)(TimeOut)、期限(deadline)、直到…才(wait until)等等)，針對(duì)這些時(shí)序約束的建模與驗(yàn)證也存在不足.形式化方法應(yīng)既能在列控系統(tǒng)層次上描述不同運(yùn)營(yíng)場(chǎng)景之間的關(guān)系，又能在運(yùn)營(yíng)場(chǎng)景層次上描述接口信息交互行為的時(shí)序約束，因此，結(jié)合運(yùn)營(yíng)場(chǎng)景需求規(guī)范的特征和特點(diǎn)選擇合適的形式化方法是研究的難點(diǎn).

另一方面，列控系統(tǒng)具有實(shí)時(shí)性、混雜性等特點(diǎn)，系統(tǒng)功能的正確性不僅要求邏輯功能的正確性，而且要求在規(guī)定的時(shí)間約束內(nèi)做出正確的邏輯響應(yīng).不同的運(yùn)營(yíng)場(chǎng)景、不同的測(cè)試目的和不同的時(shí)間約束都對(duì)應(yīng)不同的測(cè)試案例，功能測(cè)試面臨著狀態(tài)空間爆炸和時(shí)間特性測(cè)試的問(wèn)題. 例如，在列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景中，RBC 根據(jù)接收到車載設(shè)備發(fā)送消息的時(shí)間，結(jié)合運(yùn)營(yíng)場(chǎng)景中的時(shí)間約束要求，在規(guī)定的時(shí)間內(nèi)必須輸出對(duì)應(yīng)的邏輯功能(正常的移動(dòng)授權(quán)或緊急制動(dòng)).針對(duì)運(yùn)營(yíng)場(chǎng)景接口信息交互的時(shí)序特點(diǎn)，選擇恰當(dāng)?shù)臏y(cè)試目的，進(jìn)行高效的測(cè)試案例自動(dòng)生成，并形成涵蓋列控系統(tǒng)所有運(yùn)營(yíng)場(chǎng)景的測(cè)試套，是研究的另一個(gè)難點(diǎn).

本文基于HCSP 和TA(timed automata)理論［12］，提出了一種基于模型的列控系統(tǒng)測(cè)試案例生成方法.首先，結(jié)合列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景之間的執(zhí)行特點(diǎn)，利用HCSP 的順序和并發(fā)操作進(jìn)行了列控系統(tǒng)功能的形式化建模;其次，利用HCSP 支持中斷機(jī)制(通訊中斷、時(shí)間中斷等)的特點(diǎn)，針對(duì)相關(guān)運(yùn)營(yíng)場(chǎng)景內(nèi)部組件交互的時(shí)序約束(例如延遲、超時(shí)、中斷等)進(jìn)行了形式化建模，并通過(guò)引入轉(zhuǎn)換規(guī)則，將HCSP 的一個(gè)子集轉(zhuǎn)換成TA 網(wǎng)絡(luò)模型，從而進(jìn)行相關(guān)屬性的驗(yàn)證;再次，基于時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，給出了列控系統(tǒng)在單一運(yùn)營(yíng)場(chǎng)景執(zhí)行下不同覆蓋準(zhǔn)則下(全狀態(tài)、全變遷和自定義-使用)的測(cè)試案例生成算法，以及涵蓋所有列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景的測(cè)試案例套優(yōu)化算法，并在此基礎(chǔ)上，結(jié)合模型檢驗(yàn)工具Uppaal 和CoVer，提出了一條適合于列控系統(tǒng)測(cè)試案例自動(dòng)生成的工具鏈;最后，結(jié)合典型的CTCS-3 級(jí)列控系統(tǒng)RBC 切換運(yùn)營(yíng)場(chǎng)景，建立場(chǎng)景的HCSP 模型，驗(yàn)證了場(chǎng)景中時(shí)序約束的屬性.結(jié)合不同的測(cè)試覆蓋準(zhǔn)則，生成了相關(guān)的測(cè)試案例套，并進(jìn)行了比較分析.

1 列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景的建模與驗(yàn)證方法

HCSP［13-14］是一種以CSP 為基礎(chǔ)，引入描述混成系統(tǒng)中連續(xù)動(dòng)態(tài)行為的微分方程，以及各種中斷機(jī)制(通信中斷、時(shí)間中斷、事件中斷等)，以期實(shí)現(xiàn)對(duì)外部事件引發(fā)進(jìn)程遷移行為進(jìn)行描述的形式化建模語(yǔ)言.

1.1 列控系統(tǒng)功能的HCSP 模型

根據(jù)CTCS-3 級(jí)列控系統(tǒng)總體技術(shù)方案［11］，定義一列列車從“注冊(cè)與啟動(dòng)”到“注銷”的某種運(yùn)營(yíng)過(guò)程，如圖1 所示.

假設(shè)以上整個(gè)系統(tǒng)層的每個(gè)運(yùn)營(yíng)場(chǎng)景都由一個(gè)HCSP 的原子公式來(lái)描述，注冊(cè)與啟動(dòng)場(chǎng)景:PS0;級(jí)間轉(zhuǎn)換場(chǎng)景:PS1;行車許可場(chǎng)景:PS2;臨時(shí)限速場(chǎng)景:PS3;自動(dòng)過(guò)分相場(chǎng)景:PS4;RBC 切換場(chǎng)景:PS5;降級(jí)場(chǎng)景:PS6;注銷場(chǎng)景:PS7.

利用HCSP 的順序操作和并發(fā)操作算子，定義整個(gè)列控系統(tǒng)功能的HCSP 模型為

SYS?PS0;PS1;PS2(PS3;PS4;PS5);PS6;PS7.

圖1 列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景過(guò)程Fig.1 Operation scenario process of the train control system

1.2 基于HCSP 子集的運(yùn)營(yíng)場(chǎng)景建模方法

主要研究集中在列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景內(nèi)部組件交互的時(shí)序約束行為描述上，結(jié)合列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景的描述特點(diǎn)，提出了6 種更適合于列控系統(tǒng)場(chǎng)景描述的時(shí)序模型:周期性、延遲、時(shí)間等待、超時(shí)、截止期限和時(shí)間中斷，并給出了適合于列控系統(tǒng)場(chǎng)景時(shí)序描述的一個(gè)HCSP 子集HCSPsub(僅考慮時(shí)間t是唯一的連續(xù)變量)，如表1 所示. 假設(shè)P 和Q 為兩個(gè)進(jìn)程，其HCSPsub進(jìn)程的定義見(jiàn)表1.

表1 HCSPsub的進(jìn)程定義Tab.1 Process definition of HCSPsub

1.3 基于TA 的驗(yàn)證方法

規(guī)則1 Stop

Stop 指系統(tǒng)永遠(yuǎn)不會(huì)終止的idle 進(jìn)程，記作Astop，Astop=({i}，i，φ，φ，φ，{(i，true)}，φ).

規(guī)則2 Skip

Skip 指系統(tǒng)立即終止的進(jìn)程，記作Askip，Askip=({i，f}，i，{f}，{τ}，φ，{i，urgent)，(f，true)}，{(i，τ，φ，true，f)}).

規(guī)則3 事件前綴

如圖2 所示，事件前綴是指事件a 發(fā)生在時(shí)間自動(dòng)機(jī)A 的任何變遷之前，記作eventprefix(a，A).

圖2 事件前綴Fig.2 Event prefix

規(guī)則4 尾遞歸

如圖3 所示，尾遞歸指系統(tǒng)永遠(yuǎn)不會(huì)終止的進(jìn)程，記作recur(A，S0).

(SS0，init，F(xiàn)S0，Σ，C，Inv，T')，

其中:

圖3 尾遞歸Fig.3 Tail recursion

規(guī)則5 延遲

如圖4 所示，延遲主要用于描述系統(tǒng)執(zhí)行某一段延遲時(shí)間單元的進(jìn)程，記作delay(t)，

其中:

圖4 延遲Fig.4 Delay

規(guī)則6 期限

如圖5 所示，期限指系統(tǒng)執(zhí)行完成進(jìn)程必須在一定時(shí)間單元內(nèi)，記作deadline(A，t)，

圖5 期限Fig.5 Deadline

規(guī)則7 時(shí)間等待

如圖6 所示，時(shí)間等待(WaitUntil)表示系統(tǒng)在等待某段時(shí)間后終止的進(jìn)程，記作waitunitl(A，t)，

圖6 時(shí)間等待Fig.6 Wait until

規(guī)則8 外部選擇

如圖7 所示，外部選擇表示系統(tǒng)根據(jù)外部的事件進(jìn)行動(dòng)作變遷選擇的進(jìn)程，記作extchoice(A1，A2)，

圖7 外部選擇Fig.7 External choice

規(guī)則9 順序組合

如圖8 所示，順序組合表示系統(tǒng)執(zhí)行任務(wù)先后順序的進(jìn)程，記作seq(A1，A2)，

圖8 順序組合Fig.8 Sequential composition

規(guī)則10 超時(shí)

如圖9 所示，超時(shí)描述系統(tǒng)通過(guò)時(shí)間段切換控制權(quán)的進(jìn)程，記作timeout(A1，A2，t)，

圖9 超時(shí)Fig.9 Time out

規(guī)則11 時(shí)間中斷

圖10 所示，時(shí)間中斷描述系統(tǒng)通過(guò)時(shí)間點(diǎn)中斷切換控制權(quán)的進(jìn)程，記作timeinter(A1，A2，t)，

圖10 時(shí)間中斷Fig.10 Time interrupt

規(guī)則12 事件中斷

如圖11 所示，時(shí)間中斷描述系統(tǒng)通過(guò)事件中斷切換控制權(quán)的進(jìn)程，記作evtinter(A1，A2，a)，

圖11 事件中斷Fig.11 Event interrupt

更多定義詳見(jiàn)文獻(xiàn)［13］.假設(shè)P 為HCSPsub的進(jìn)程，A 為一個(gè)時(shí)間自動(dòng)機(jī)，定義轉(zhuǎn)換函數(shù)Φ:P→A為HCSPsub到時(shí)間自動(dòng)機(jī)A 的映射，從而有以下轉(zhuǎn)換規(guī)則:

基于上述轉(zhuǎn)換規(guī)則，可以利用典型的模型檢驗(yàn)工具Uppaal［15］進(jìn)行TA 模型相關(guān)屬性的自動(dòng)驗(yàn)證分析，相關(guān)研究可參考文獻(xiàn)［13］.

2 基于TA 模型的測(cè)試案例生成方法

在模型轉(zhuǎn)換規(guī)則的基礎(chǔ)上，利用典型的模型檢驗(yàn)工具(Uppaal 和CoVer［16］)，給出了一條適合于列控系統(tǒng)測(cè)試案例自動(dòng)生成的工具鏈. 如圖12 所示，整個(gè)測(cè)試方法包括4 個(gè)步驟.

圖12 基于模型的測(cè)試案例生成方法Fig.12 Model-based test case generation method

第1 步 規(guī)范分析階段

通過(guò)分析列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景規(guī)范，提取列控系統(tǒng)建模對(duì)象和驗(yàn)證屬性. 例如，CTCS-3 級(jí)列控系統(tǒng)“行車許可”運(yùn)營(yíng)場(chǎng)景(PS2)中規(guī)定:

(1)RBC 能夠發(fā)送移動(dòng)授權(quán)信息給車載;

(2)車載能夠發(fā)送給RBC 位置報(bào)告信息;

(3)車載如果在［0，T］內(nèi)接收不到移動(dòng)授權(quán)信息則實(shí)施緊急制動(dòng)操作，其中，T 是一個(gè)大于0的常數(shù).

第2 步 模型抽象階段

通過(guò)對(duì)列控系統(tǒng)規(guī)范的分析，基于HCSPsub和TA 理論，抽象出列控系統(tǒng)場(chǎng)景規(guī)范的形式化模型.

(1)通過(guò)定義列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景中相關(guān)對(duì)象的進(jìn)程，建立列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景的時(shí)序模型. 上述“行車許可”運(yùn)營(yíng)場(chǎng)景(PS2)的時(shí)序模型定義如下:

式中:Prbc和Pevc分別為“行車許可”運(yùn)營(yíng)場(chǎng)景中的RBC 和車載的進(jìn)程;PEB為緊急制動(dòng)進(jìn)程(這里用stop 表示);MA 和pos 分別為移動(dòng)授權(quán)信息和位置報(bào)告信息.

(2)結(jié)合1.3 節(jié)的轉(zhuǎn)換規(guī)則，將列控系統(tǒng)的HCSPsub模型轉(zhuǎn)換成TA 網(wǎng)絡(luò)模型.上述行車許可場(chǎng)景的HCSPsub模型可轉(zhuǎn)換成如下自動(dòng)機(jī)網(wǎng)絡(luò)模型:

Φ(PrbcPevc)=para(Φ(Prbc)，Φ(Pevc)).

由規(guī)則3、4 和9，得到RBC 的TA 模型，如圖13 所示.

圖13 RBC 模型Fig.13 RBC model

由規(guī)則3、4、9 和12，得到EVC 的TA 模型，如圖14 所示.

結(jié)合TA 理論，RBC 和EVC 自動(dòng)機(jī)時(shí)序模型的行為可以描述成:

圖14 EVC 模型Fig.14 European vital computer (EVC)model

第3 步 模型建立階段

利用UPPAAL 和CoVer 兩個(gè)TA 模型檢驗(yàn)工具，進(jìn)行測(cè)試案例自動(dòng)生成研究.

(1)利用建模工具Uppaal 建立TA 網(wǎng)絡(luò)模型，并驗(yàn)證相關(guān)屬性(安全相關(guān)屬性和時(shí)間相關(guān)屬性).結(jié)合上述的“行車許可”運(yùn)營(yíng)場(chǎng)景TA 模型，定義該自動(dòng)機(jī)網(wǎng)絡(luò)Uppaal 模型為R-E:

RBC EVC.

R-E 的UPPAAL 模型如下圖15 所示.

圖15 R-E 模型Fig.15 R-E model

(2)利用測(cè)試案例生成工具CoVer，結(jié)合不同測(cè)試準(zhǔn)則，進(jìn)行測(cè)試套的自動(dòng)生成.

典型的測(cè)試案例tc(test case)可以表示成一個(gè)三元組＜input，step，output ＞，即測(cè)試輸入、執(zhí)行步驟和期望輸出. 測(cè)試序列ts(test sequence)則為運(yùn)行測(cè)試案例過(guò)程中執(zhí)行的行為序列.假設(shè)被測(cè)設(shè)備為EVC，上述例子中，測(cè)試執(zhí)行序列ts 可以通過(guò)時(shí)間自動(dòng)機(jī)時(shí)序模型run(rbc)變遷上的輸入或輸出序列:

該測(cè)試序列ts 表示RBC 執(zhí)行了3 條相同的測(cè)試案例tc:＜MA，NULL，pos ＞. RBC 首先執(zhí)行第1條測(cè)試案例tc，向被測(cè)設(shè)備EVC 接口輸入消息MA，等待期望輸出消息pos，一旦收到pos，繼續(xù)執(zhí)行第2 條測(cè)試案例tc，直到所有測(cè)試案例執(zhí)行完為止.

CoVer 利用觀測(cè)器原理［16］，提供了3 種領(lǐng)域功能無(wú)關(guān)的覆蓋準(zhǔn)則(全狀態(tài)、全變遷或者自定義-使用)，如圖16(a)～(c)所示. 根據(jù)不同的測(cè)試目的，針對(duì)運(yùn)營(yíng)場(chǎng)景的自動(dòng)機(jī)時(shí)序模型，給出全狀態(tài)、全變遷和自定義-使用3 種測(cè)試案例自動(dòng)生成算法.

圖16 測(cè)試案例覆蓋準(zhǔn)則Fig.16 Test case coverage criteria

圖16(a)定義了全狀態(tài)覆蓋準(zhǔn)則，其包含被測(cè)進(jìn)程TA 模型中所有狀態(tài)的覆蓋準(zhǔn)則.

圖16(b)定義了全變遷覆蓋準(zhǔn)則，其包含被測(cè)進(jìn)程TA 模型中所有變遷的覆蓋準(zhǔn)則.

圖16(c)定義了自定義-使用全覆蓋準(zhǔn)則，其包含被測(cè)進(jìn)程TA 模型中所有自定義變量的覆蓋準(zhǔn)則.

結(jié)合本節(jié)實(shí)例，僅給出滿足被測(cè)設(shè)備EVC 自動(dòng)機(jī)全狀態(tài)和全變遷覆蓋準(zhǔn)則下的測(cè)試序列(自定義-使用覆蓋準(zhǔn)則在第3 節(jié)介紹).

(1)全狀態(tài)覆蓋測(cè)試序列

根據(jù)R-E 自動(dòng)機(jī)時(shí)序行為模型run(rbc evc)，構(gòu)造1 條測(cè)試序列，使之在執(zhí)行測(cè)試序列的過(guò)程中，被測(cè)EVC 的行為run(evc)能夠經(jīng)過(guò)所有EVC的狀態(tài).可直觀地定義:

(2)全變遷覆蓋測(cè)試序列

同理，構(gòu)造1 條測(cè)試序列，使之經(jīng)過(guò)所有EVC的變遷，可直觀地定義:

式中:d1＜T，d2≥T，d3≥0.

第4 步 列控系統(tǒng)測(cè)試案例自動(dòng)生成階段

由于列控系統(tǒng)不同的運(yùn)營(yíng)場(chǎng)景具有不同的時(shí)序模型，通過(guò)簡(jiǎn)單疊加各個(gè)運(yùn)營(yíng)場(chǎng)景測(cè)試案例的方式，能夠得到整個(gè)系統(tǒng)的測(cè)試案例套，然而這會(huì)造成大量重復(fù)的測(cè)試案例.為了得到在某種測(cè)試準(zhǔn)則條件下，100%覆蓋整個(gè)列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景時(shí)序模型的測(cè)試案例集，設(shè)計(jì)了如下優(yōu)化算法:

算法描述如下:

對(duì)于任何一個(gè)給定的運(yùn)營(yíng)場(chǎng)景時(shí)序模型M0和S0，定義i=0，并給定一個(gè)測(cè)試準(zhǔn)則?.

(1)進(jìn)入循環(huán)，針對(duì)初始的運(yùn)營(yíng)場(chǎng)景時(shí)序模型，進(jìn)行測(cè)試案例自動(dòng)生成操作Total_TestCase，并將結(jié)果存儲(chǔ)在ts 中;

(2)判斷測(cè)試案例套Sts中是否含有ts.如果含有，則執(zhí)行i=i+1，并且跳轉(zhuǎn)至循環(huán);

(3)如果不含有ts，存儲(chǔ)ts 到Sts中;

(4)執(zhí)行change_initial(Mi，Si)操作，得到下一個(gè)運(yùn)營(yíng)場(chǎng)景時(shí)序模型，執(zhí)行i=i+1;

(5)循環(huán)執(zhí)行步驟(1)，直到i=N 為止.

3 案例分析

3.1 RBC 切換場(chǎng)景

RBC 切換是指RBC 間在指定區(qū)域(切換應(yīng)答器)實(shí)現(xiàn)對(duì)列車無(wú)縫切換［11］，如圖17 所示.

根據(jù)CTCS-3 級(jí)列控系統(tǒng)總體技術(shù)方案內(nèi)容，以兩部電臺(tái)的RBC 切換過(guò)程為例，HRBC 表示移交RBC，TRBC 表示接管RBC，整個(gè)切換流程如圖18 所示.

圖17 RBC 切換場(chǎng)景原理Fig.17 Principle of RBC transition scenario

圖18 RBC 切換場(chǎng)景流程Fig.18 Process of RBC handover scenario

3.2 RBC 切換的HCSP 模型

(1)Timer 進(jìn)程

Timer 進(jìn)程通過(guò)通道circle 來(lái)控制HRBC、TRBC 與EVC 進(jìn)程之間消息的交互.

(2)Speed 進(jìn)程

Speed 進(jìn)程由speed0 進(jìn)程、speed1 進(jìn)程、speed2進(jìn)程和speed3 進(jìn)程組成，通過(guò)通道acc 和Dec 模擬列車的加速和減速過(guò)程，其HCSP 模型如下:

(3)Queue 進(jìn)程

Queue 進(jìn)程是一個(gè)由add 進(jìn)程和shift 進(jìn)程組成的尾遞歸進(jìn)程，主要完成HRBC 和TRBC 對(duì)EVC的管理功能.對(duì)應(yīng)的HCSP 模型如下:

(4)HRBC 進(jìn)程

HRBC 進(jìn)程描述的HRBC 與EVC 之間的周期性信息交互過(guò)程，由建立鏈接start、建立通信會(huì)晤buildconnect、控制control、MA 計(jì)算computeMA、切換預(yù)通告pre、進(jìn)路信息請(qǐng)求req、混合MA 計(jì)算comPmixMA、注銷logout 和刪除列車delete 共9 個(gè)進(jìn)程組成.對(duì)應(yīng)的HCSP 模型如下:

(5)EVC 進(jìn)程

EVC 進(jìn)程描述EVC 與HRBC 和TRBC 之間的周期性信息交互過(guò)程，由建立鏈接start、建立通信會(huì)晤buildconnect、發(fā)送位置報(bào)告reportPos、MA 請(qǐng)求MAreq、速度控制ControlSpeed、切換handover、建立鏈接start1、建立通信會(huì)晤buildconnect1、注銷logout 和鏈接失敗disconnect 等10 個(gè)進(jìn)程組成.對(duì)應(yīng)的HCSP 模型如下:

(6)TRBC 進(jìn)程

TRBC 進(jìn)程描述TRBC 與HRBC 和EVC 之間的周期性信息交互過(guò)程，由切換預(yù)通告pre、進(jìn)路信息Routeinfo、建立鏈接 start、建立通信會(huì)晤buildconnect、控制control、MA 計(jì)算compMA、切換handover 等7 個(gè)進(jìn)程組成.對(duì)應(yīng)的HCSP 模型如下:

通過(guò)1.3 節(jié)的轉(zhuǎn)換規(guī)則，將RBC 的切換HCSP模型轉(zhuǎn)換成TA 網(wǎng)絡(luò)模型，定義為T(mén)SQ-HET:

其中各個(gè)進(jìn)程的轉(zhuǎn)換關(guān)系如下:

如圖19 所示，利用Uppaal 工具對(duì)TSQ-HET進(jìn)行了仿真和驗(yàn)證.模型中，“!”和“?”表示自動(dòng)機(jī)網(wǎng)絡(luò)模型間信息交互的發(fā)生.

3.3 自動(dòng)測(cè)試案例生成

在TSQ-HET 模型的基礎(chǔ)上，以TSQ-HET 模型中的EVC 為被測(cè)對(duì)象(SUT)，針對(duì)3 種不同的測(cè)試案例覆蓋準(zhǔn)則(全狀態(tài)、全變遷和MA(消息M3)相關(guān)的測(cè)試案例)進(jìn)行了自動(dòng)測(cè)試案例的生成.圖20 描述了M3 相關(guān)的測(cè)試案例生成算法，依據(jù)該算法可以通過(guò)模型自動(dòng)生成M3 相關(guān)的測(cè)試案例套.

如圖21 所示，整個(gè)M3 相關(guān)的測(cè)試案例套包含3 部分:路徑trace(trace #1)、測(cè)試案例覆蓋項(xiàng)test case item 以及轉(zhuǎn)移條件transitions.

本文給出以下3 個(gè)指標(biāo)來(lái)衡量測(cè)試案例自動(dòng)生成的有效性.

(1)測(cè)試套:滿足相關(guān)覆蓋準(zhǔn)則的測(cè)試案例數(shù)量，以及測(cè)試案例覆蓋的事件執(zhí)行(EdgeN)數(shù)量.測(cè)試套的數(shù)量越大，表明測(cè)試越充分，反之亦然;

圖19 TSQ-HET 時(shí)間網(wǎng)絡(luò)自動(dòng)機(jī)Fig.19 Network of TSQ-HET timed automata

圖20 M3 相關(guān)的測(cè)試案例生成準(zhǔn)則Fig.20 Test case generation criterion about M3

(2)測(cè)試時(shí)間:滿足相關(guān)覆蓋準(zhǔn)則條件下，測(cè)試案例自動(dòng)生成的時(shí)間. 時(shí)間越短，表明測(cè)試案例生成效率越高，反之亦然;

(3)內(nèi)存消耗:滿足相關(guān)覆蓋準(zhǔn)則條件下，CoVer 軟件消耗的內(nèi)存大小. 內(nèi)存消耗越小，表明測(cè)試案例生成效率越高，反之亦然.不同測(cè)試準(zhǔn)則下的測(cè)試套比較見(jiàn)表2.

圖21 EVC 的測(cè)試套Fig.21 Test suites of EVC

表2 從測(cè)試套(案例數(shù)量、測(cè)試案例覆蓋項(xiàng))、測(cè)試時(shí)間和內(nèi)存消耗3 個(gè)方面，對(duì)3 種不同的測(cè)試案例覆蓋準(zhǔn)則(全狀態(tài)、全變遷和MA(消息M3)相關(guān)的測(cè)試案例)進(jìn)行了對(duì)比分析. 結(jié)論表明，全狀態(tài)覆蓋的測(cè)試套執(zhí)行時(shí)間和內(nèi)存消耗均大于全變遷和自定義-使用，自定義-使用的測(cè)試時(shí)間和內(nèi)存消耗最小，能夠有效的提高測(cè)試的效率.

表2 不同測(cè)試準(zhǔn)則下的測(cè)試套比較Tab.2 Comparison of test suites under different criteria

4 結(jié)束語(yǔ)

本文基于HCSP 和TA 理論，提出了一種基于模型的列控系統(tǒng)測(cè)試案例生成方法.針對(duì)HCSP 的一個(gè)子集，提出了HCSP 的子集模型轉(zhuǎn)換成TA 網(wǎng)絡(luò)模型的轉(zhuǎn)換規(guī)則，實(shí)現(xiàn)了列控系統(tǒng)HCSP 安全屬性和時(shí)間相關(guān)屬性的自動(dòng)驗(yàn)證. 基于TA 網(wǎng)絡(luò)模型，提出了全狀態(tài)、全變遷和自定義-使用3 種覆蓋準(zhǔn)則下的測(cè)試案例自動(dòng)生成算法，優(yōu)化了列控系統(tǒng)測(cè)試案例套的自動(dòng)生成. 在此基礎(chǔ)上，給出了一個(gè)基于Uppaal＆CoVer 模型檢驗(yàn)工具鏈，實(shí)現(xiàn)了列控系統(tǒng)測(cè)試案例自動(dòng)生成. 最后，結(jié)合實(shí)際CTCS-3級(jí)列控系統(tǒng)RBC 切換場(chǎng)景進(jìn)行了案例分析，生成了不同覆蓋準(zhǔn)則的測(cè)試套，并進(jìn)行了比較分析，測(cè)試結(jié)果表明了方法的有效性.

［1］ 呂繼東. 列車運(yùn)行控制系統(tǒng)分層形式化建模與驗(yàn)證分析［D］. 北京:北京交通大學(xué)，2011.

［2］ 古天龍. 軟件開(kāi)發(fā)的形式化方法［M］. 北京:高等教育出版社，2005:6-8.

［3］ CHAOCHEN Z，HANSEN M. Duration calculus a formal approach to real-time systems［M］. ［S. l.］:Springer-Verlag，2003:14-16.

［4］ DONG Jinsong，HAO Ping，QIN Shengchao，et al.Timed automata patterns［J］. IEEE Transactions on Software Engineering，34，2008:844-845.

［5］ HOARE C A R. Communicating sequential processes［J］.Communications of the ACM，1978，21(8):666-677.

［6］ LIU Jiang，Lü Jidong，ZHAO Quan. Programming languages and systems:a calculus for hybrid CSP［M］.Berlin:Springer，2010:1-15.

［7］ BEIZER B. Black-box testing，techniques for functional testing of software and systems［M］. New York:Wiley，1995:39-41.

［8］ 張勇，王超琦. CTCS-3 級(jí)列控系統(tǒng)車載設(shè)備測(cè)試序列優(yōu)化生成方法［J］. 中國(guó)鐵道科學(xué)，2011，32(3):100-106.ZHANG Yong，WANG Chaoqi. The method for the optimal generation of test sequence for CTCS-3 on-board equipment［J］. China Railway Science，2011，32(3):100-106.

［9］ 徐中偉，吳芳美. 形式化故障樹(shù)分析建模和軟件安全性測(cè)試［J］. 同濟(jì)大學(xué)學(xué)報(bào):自然科學(xué)版，2001，29(11):1299-1302.XU Zhongwei，WU Fangmei. Formal fault tree analysis modeling and software safety testing［J］. Journal of Tongji University:Natural Science，2001，29(11):1299-1302.

［10］ 趙顯瓊，唐濤. 多端口形式化測(cè)試自動(dòng)生成方法在CTCS-3 車載系統(tǒng)中的應(yīng)用［J］. 鐵道學(xué)報(bào)，2011，33(7):44-51.ZHAO Xianqiong， TANG Tao. Multi-port based automatic formal testing generation and its application in CTCS-3 level on-board system［J］. Journal of the China Railway Society，2011，33(7):44-51.

［11］ 張曙光. CTCS-3 級(jí)列控系統(tǒng)總體技術(shù)方案［M］. 北京.中國(guó)鐵道出版社，2008:49-50.

［12］ ALUR R，DILL D L. A theory of timed automata［J］.Theoretical Computer Science，1994，126:183-235.

［13］ 呂繼東，唐濤. 高速鐵路列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景實(shí)時(shí)性建模與驗(yàn)證［J］. 鐵道學(xué)報(bào)，2011，33(6):54-61.Lü Jidong，TANG Tao. Modeling and verification of time constraints of operation scenarios of high-speed train control system［J］. Journal of the China Railway Society，2011，33(6):54-61.

［14］ ZHOU Chaochen，WANG Ji，ANDERS P. Ravn a formal description of hybrid systems［C］∥Proc. of the DIMACS/SYCON Workshop on Hybrid Systems III:Verification and Control. New York:Springer-Verlag，1996:511-530.

［15］ BEHRMANN G，LARSEN K G，MOLLER O，et al.UPPAAL-present and future［C］∥Proc. of the 40th IEEE Conference on Decision and Control. Orlando:［s. n.］，2001:2881-2886.

［16］ HESSEL A，PETTERSSON P. CoVer:a real-time test case generation tool［C］∥19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software. Berlin:Springer，2007:73-77.