梁君海，李春峰，萬(wàn) 里，楊毅峰，薛一鳴

（1.中車(chē)成都機(jī)車(chē)車(chē)輛有限公司西南研發(fā)中心，成都 610511；2.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院，成都 610097）

1 概述

隨著社會(huì)經(jīng)濟(jì)的高速發(fā)展，軌道交通正向著智能和集約的方向迅速發(fā)展[1]，全自動(dòng)運(yùn)行系統(tǒng)（Fully Automatic Operation，F(xiàn)AO）已成為軌道交通領(lǐng)域的熱點(diǎn)研究?jī)?nèi)容。全自動(dòng)運(yùn)行系統(tǒng)基于計(jì)算機(jī)、通信和系統(tǒng)集成等技術(shù)，對(duì)相關(guān)設(shè)備自動(dòng)進(jìn)行控制，實(shí)現(xiàn)列車(chē)運(yùn)行全過(guò)程的自動(dòng)化[2]。全自動(dòng)運(yùn)行系統(tǒng)是典型的安全關(guān)鍵系統(tǒng)（Safety-Critical System），系統(tǒng)邏輯復(fù)雜，規(guī)模龐大，一旦失效，影響巨大。因此，在投入運(yùn)營(yíng)前對(duì)全自動(dòng)運(yùn)行系統(tǒng)進(jìn)行全面系統(tǒng)的測(cè)試具有重要意義。

文獻(xiàn)[3]提出一種城市軌道交通全自動(dòng)駕駛車(chē)輛仿真測(cè)試平臺(tái)方案，以測(cè)試驗(yàn)證車(chē)輛在全自動(dòng)運(yùn)營(yíng)場(chǎng)景和人工駕駛運(yùn)營(yíng)場(chǎng)景下的正常和故障工況。文獻(xiàn)[4]以上海軌道交通10 號(hào)線(xiàn)為例，對(duì)列車(chē)休眠和喚醒場(chǎng)景進(jìn)行了深入分析。文獻(xiàn)[5]對(duì)城市軌道交通全自動(dòng)運(yùn)行系統(tǒng)進(jìn)行介紹，以典型運(yùn)營(yíng)場(chǎng)景為例對(duì)全自動(dòng)運(yùn)營(yíng)場(chǎng)景進(jìn)行梳理，分析關(guān)鍵裝備的功能需求以及各設(shè)備專(zhuān)業(yè)之間的接口關(guān)系。文獻(xiàn)[6]結(jié)合國(guó)際標(biāo)準(zhǔn)研究全自動(dòng)運(yùn)行系統(tǒng)典型的系統(tǒng)功能與安全需求，對(duì)運(yùn)營(yíng)場(chǎng)景進(jìn)行分析，對(duì)國(guó)內(nèi)自主研發(fā)全自動(dòng)運(yùn)行系統(tǒng)提出參考建議。文獻(xiàn)[7]分析了CBTC-RF 信號(hào)系統(tǒng)駕駛模式及模式間轉(zhuǎn)換應(yīng)遵循的原則。

目前，全自動(dòng)運(yùn)行系統(tǒng)的研究主要集中在系統(tǒng)方案和仿真分析，對(duì)測(cè)試用例生成方法的研究較少。時(shí)間自動(dòng)機(jī)具有嚴(yán)格的數(shù)學(xué)定義，在軌道交通測(cè)試建模領(lǐng)域取得了廣泛的應(yīng)用[8-10]。本文結(jié)合全自動(dòng)運(yùn)行系統(tǒng)的特點(diǎn)，針對(duì)全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成過(guò)程中存在的指定路徑覆蓋的需求，基于時(shí)間自動(dòng)機(jī)建模理論，提出全自動(dòng)運(yùn)行系統(tǒng)的測(cè)試用例自動(dòng)生成方法，對(duì)全自動(dòng)運(yùn)行系統(tǒng)的安全性保障具有一定的意義。

2 時(shí)間自動(dòng)機(jī)及UPPAAL介紹

時(shí)間自動(dòng)機(jī)（Timed Automata，TA） 由Stanford 大學(xué)的Rajeev Alur 和David Dill 于20世紀(jì)90 年代提出。時(shí)間自動(dòng)機(jī)對(duì)有限自動(dòng)機(jī)進(jìn)行了擴(kuò)展，使用有限個(gè)時(shí)鐘變量表示有時(shí)間約束的狀態(tài)轉(zhuǎn)換圖，進(jìn)而描述系統(tǒng)的實(shí)時(shí)行為[11-12]。

定義1 （時(shí)間自動(dòng)機(jī)）TA 定義為一個(gè)六元組〈S,S0,Σ,X,I,E〉，其中：

S是有窮位置的集合；

S0是初始事件的集合；

Σ是有窮事件的集合；

X是有窮時(shí)鐘的集合；

I是每個(gè)位置的映射，對(duì)s∈S指定Φ(x)中一個(gè)時(shí)間約束δ；

E?S×Σ×Φ(x)×2x×S表示位置轉(zhuǎn)移的集合。

〈s,a,φ,λ,s'〉 表示輸入動(dòng)作a時(shí)，從位置s到s'的轉(zhuǎn)移；φ是X上的一個(gè)時(shí)鐘約束，在轉(zhuǎn)移發(fā)生時(shí)被滿(mǎn)足；λ∈X是在該轉(zhuǎn)移發(fā)生時(shí)復(fù)位的時(shí)鐘集合。

UPPAAL 是由瑞典Uppsala 大學(xué)和丹麥Aalborg 大學(xué)聯(lián)合開(kāi)發(fā)的針對(duì)TA 理論的建模、驗(yàn)證和測(cè)試用例生成工具。UPPAAL 拓展了TA 理論，擴(kuò)展出變量和通道等元素，UPPAAL 提供Yggdrasil從TA 模型自動(dòng)生成測(cè)試用例[13]，包括3 個(gè)階段：

1）Query File，Yggdrasil 加載驗(yàn)證Query文件，將可達(dá)性分析的路徑轉(zhuǎn)換為測(cè)試用例；

2）Depth Search，采用隨機(jī)深度優(yōu)先搜索算法，將搜索所得路徑自動(dòng)轉(zhuǎn)換為測(cè)試用例；

3）Single Step，針對(duì)階段1）和階段2）中未覆蓋的邊進(jìn)行可達(dá)性分析生成測(cè)試用例，直到覆蓋模型中所有的邊。

3 全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成算法

3.1 全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成問(wèn)題

全自動(dòng)運(yùn)行系統(tǒng)的測(cè)試用例主要由測(cè)試人員依據(jù)經(jīng)驗(yàn)人工編制，通常由測(cè)試人員根據(jù)積累的測(cè)試關(guān)鍵項(xiàng)，指定測(cè)試過(guò)程中的某幾個(gè)步驟，或指定某幾個(gè)環(huán)節(jié)之間需要滿(mǎn)足的條件，然后人工編制完整的測(cè)試用例。全自動(dòng)運(yùn)行系統(tǒng)交互復(fù)雜，測(cè)試步驟較多，人工編制測(cè)試用例存在效率低、容易遺漏測(cè)試需求等問(wèn)題[14]。

定義2（指定路徑覆蓋） 測(cè)試需求包含一個(gè)測(cè)試路徑集合P，其中P以參數(shù)的形式給出。

如圖1 所示，TAex模型包括6 個(gè)位置，根據(jù)測(cè)試經(jīng)驗(yàn)，測(cè)試用例需要測(cè)試S4 →S5 →S6指定的測(cè)試路徑，即指定測(cè)試路徑覆蓋：P＝{(S4,S5),(S5,S6)}。

圖1 TAex模型示例Fig.1 TAex model example

3.2 全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成算法

Yggdrasil 生成測(cè)試用例時(shí)不考慮指定路徑覆蓋。如圖1 所示的TA 模型，Yggdrasil 生成如下4條測(cè)試用例，未覆蓋指定的測(cè)試需求P，不能滿(mǎn)足全自動(dòng)運(yùn)行系統(tǒng)指定路徑覆蓋的要求。

1）S0 →S3 →S4；

2）S0 →S2 →S6；

3）S0 →S3 →S4 →S5；

4）S0 →S1 →S5 →S6。

基于以上問(wèn)題，提出全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成方法。首先，在全自動(dòng)運(yùn)行系統(tǒng)功能模型的基礎(chǔ)上增加測(cè)試標(biāo)記變量，達(dá)到在模型的邊或節(jié)點(diǎn)位置上描述測(cè)試人員指定測(cè)試需求的目的，即在全自動(dòng)運(yùn)行系統(tǒng)的功能模型中表征測(cè)試人員指定的測(cè)試路徑需求，形成全自動(dòng)運(yùn)行系統(tǒng)的測(cè)試模型。測(cè)試標(biāo)記變量?jī)H用于反應(yīng)測(cè)試人員指定的測(cè)試需求，不改變?nèi)詣?dòng)運(yùn)行系統(tǒng)模型的功能邏輯；然后，編制測(cè)試人員指定的測(cè)試需求的Query 文件，以Yggdrasil 的Query File 測(cè)試用例生成方法對(duì)驗(yàn)證文件生成測(cè)試用例，滿(mǎn)足測(cè)試人員的指定路徑覆蓋；最后，針對(duì)尚未覆蓋的邊，利用UPPAAL 的Depth Search 和Single Step 方法生成測(cè)試用例，實(shí)現(xiàn)100% 邊覆蓋，如圖2 所示。

圖2 測(cè)試用例生成流程Fig.2 Test case generation process

設(shè)U表示全自動(dòng)運(yùn)行系統(tǒng)測(cè)試人員指定的路徑覆蓋需求集，t表示算法當(dāng)前迭代生成的測(cè)試用例，R表示算法生成的測(cè)試用例集。全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成算法如圖3 所示。算法開(kāi)始時(shí)，R是一個(gè)空集。算法每次迭代生成一條測(cè)試用例，將該測(cè)試用例添加到R中，直到算法結(jié)束。

圖3 測(cè)試用例生成算法Fig.3 Test case generation algorithm

以圖1 所示的模型為例，指定路徑覆蓋為(S4,S5),(S5,S6)。對(duì)邊(S4,S5)和(S5,S6)分別增加測(cè)試標(biāo)記的int 變量b45 和b56。滿(mǎn)足指定路徑覆蓋的驗(yàn)證性質(zhì)為：q::＝E<>b45 andb56 。

采用算法1，Yggdrasil 生成3 條測(cè)試用例，100% 實(shí)現(xiàn)邊覆蓋，且測(cè)試用例3 覆蓋指定路徑覆蓋的需求。

1）S0 →S1 →S5；

2）S0 →S2 →S6；

3）S0 →S3 →S4 →S5 →S6。

4 全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換

以全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換功能為例，介紹全自動(dòng)運(yùn)行系統(tǒng)的測(cè)試用例生成方法。

全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換功能包括TIAS、司機(jī)、VOBC 與列車(chē)4 個(gè)參與者，功能流程如圖4 所示。全自動(dòng)運(yùn)行系統(tǒng)投入運(yùn)營(yíng)時(shí)，TIAS 將遠(yuǎn)程喚醒指令發(fā)送到VOBC，VOBC 與車(chē)輛進(jìn)行自檢，喚醒列車(chē)進(jìn)入FAM 模式待命。列車(chē)以FAM 模式運(yùn)行過(guò)程中出現(xiàn)車(chē)輛與VOBC 通信故障等情況時(shí)，系統(tǒng)申請(qǐng)進(jìn)入CAM 模式，經(jīng)TIAS 人工授權(quán)后，系統(tǒng)駕駛模式由FAM 模式轉(zhuǎn)換為CAM 模式。FAM 模式運(yùn)行過(guò)程中，若列車(chē)遇到特殊情況需要降級(jí)時(shí)，列車(chē)停穩(wěn)后，激活相應(yīng)端的司機(jī)室鑰匙，車(chē)載VOBC 退出FAM 模式，進(jìn)入CM 模式，轉(zhuǎn)入人工駕駛[15]。

圖4 全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換流程序列Fig.4 FAO mode conversion process sequence diagram

5 模式轉(zhuǎn)換UPPAAL建模

根據(jù)全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換流程建立全自動(dòng)運(yùn)行系統(tǒng)的TA 模型，并采用全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成算法生成測(cè)試用例。

5.1 模式轉(zhuǎn)換時(shí)間自動(dòng)機(jī)模型

全自動(dòng)運(yùn)行系統(tǒng)模式轉(zhuǎn)換流程包括TIAS、列車(chē)、司機(jī)和VOBC 4 個(gè)子系統(tǒng)，模式轉(zhuǎn)換的TA模型MODETA為各個(gè)子系統(tǒng)的TA 模型的積：MODETA=TIASTA||VOBCTA||DRIVERTA||TRAINTA。

其中，TIASTA主要完成TIAS 信息的發(fā)送和接受、列車(chē)動(dòng)作授權(quán)的處理等功能；VOBCTA主要執(zhí)行列車(chē)在模式轉(zhuǎn)換流程中的動(dòng)作，包括列車(chē)上電自檢、升級(jí)條件的檢查、列車(chē)運(yùn)行中故障信息的發(fā)送以及模式轉(zhuǎn)換；DRIVERTA主要模擬司機(jī)在模式轉(zhuǎn)換流程中手動(dòng)操作鑰匙開(kāi)關(guān)和模式轉(zhuǎn)換確認(rèn)；TRAINTA主要輸出列車(chē)速度信息和非激活端換端等操作。

MODETA如圖5 所示，共含58 個(gè)位置、90 個(gè)遷移、27 個(gè)通道和13 個(gè)變量，主要變量名稱(chēng)及其含義如表1 所示。

表1 MODETA位置及變量含義Tab.1 MODETA location and variable meaning

5.2 測(cè)試用例生成

以CM 模式轉(zhuǎn)換到FAM 模式為例，介紹測(cè)試用例生成過(guò)程。根據(jù)專(zhuān)家經(jīng)驗(yàn)，模式轉(zhuǎn)換具有如表2 所示的測(cè)試需求。

根據(jù)全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例生成算法，為表征測(cè)試場(chǎng)景，MODETA模型中包含了測(cè)試標(biāo)記的int 變量，主要變量如表3 所示。

表3 測(cè)試模型中的主要變量Tab.3 Main variables in test model

測(cè)試需求1 ～4 對(duì)應(yīng)的BNF 驗(yàn)證語(yǔ)句如表4所示。

表4 CM轉(zhuǎn)FAM模式測(cè)試需求及驗(yàn)證性質(zhì)Tab.4 Test requirements and verification properties of conversion of CM to FAM mode

利用UPPAAL 的Query 文件生成測(cè)試用例，針對(duì)表2 的4 個(gè)測(cè)試需求，生成4 條測(cè)試用例。以測(cè)試用例1 為例，其覆蓋測(cè)試場(chǎng)景1，測(cè)試過(guò)程如下：測(cè)試初始為CM 模式，列車(chē)速度不為0，司機(jī)制動(dòng)將列車(chē)速度降為0 后，操作方向手柄至零位，操作制動(dòng)手柄至零位，VOBC 檢測(cè)列車(chē)最高駕駛模式指令為全自動(dòng)駕駛模式，提示司機(jī)確認(rèn)模式轉(zhuǎn)換，但司機(jī)未確認(rèn)該信息。同時(shí)，列車(chē)超速，司機(jī)將列車(chē)速度制動(dòng)為0 后，確認(rèn)模式轉(zhuǎn)換，列車(chē)轉(zhuǎn)換至FAM 模式。

利用Yggdrasil 的Depth Search 和Single Step 方法對(duì)模型中未覆蓋的邊繼續(xù)生成測(cè)試用例，新生成14 條測(cè)試用例，其中Depth Search 方法生成1 條測(cè)試用例，Single Step 方法生成13 條測(cè)試用例。即算法一共生成18 條測(cè)試用例，邊覆蓋率為100%，且完全覆蓋測(cè)試人員指定的4 條測(cè)試需求。

6 結(jié)論

本文針對(duì)全自動(dòng)運(yùn)行系統(tǒng)測(cè)試用例編制過(guò)程中的指定路徑覆蓋問(wèn)題，研究時(shí)間自動(dòng)機(jī)建模理論，提出了基于Yggdrasil 的指定路徑覆蓋測(cè)試用例自動(dòng)生成算法。以全自動(dòng)運(yùn)行系統(tǒng)的模式轉(zhuǎn)換功能為例，建立模式轉(zhuǎn)換的時(shí)間自動(dòng)機(jī)模型，并采用論文提出的算法生成測(cè)試用例。結(jié)果表明，論文生成的測(cè)試用例100% 覆蓋測(cè)試人員指定的測(cè)試需求，同時(shí)100% 覆蓋時(shí)間自動(dòng)機(jī)模型中所有的邊，能夠滿(mǎn)足全自動(dòng)運(yùn)行系統(tǒng)指定路徑覆蓋的測(cè)試用例生成要求。