梁君海,李春峰,萬 里,楊毅峰,薛一鳴
(1.中車成都機車車輛有限公司西南研發中心,成都 610511;2.西南交通大學信息科學與技術學院,成都 610097)
隨著社會經濟的高速發展,軌道交通正向著智能和集約的方向迅速發展[1],全自動運行系統(Fully Automatic Operation,FAO)已成為軌道交通領域的熱點研究內容。全自動運行系統基于計算機、通信和系統集成等技術,對相關設備自動進行控制,實現列車運行全過程的自動化[2]。全自動運行系統是典型的安全關鍵系統(Safety-Critical System),系統邏輯復雜,規模龐大,一旦失效,影響巨大。因此,在投入運營前對全自動運行系統進行全面系統的測試具有重要意義。
文獻[3]提出一種城市軌道交通全自動駕駛車輛仿真測試平臺方案,以測試驗證車輛在全自動運營場景和人工駕駛運營場景下的正常和故障工況。文獻[4]以上海軌道交通10 號線為例,對列車休眠和喚醒場景進行了深入分析。文獻[5]對城市軌道交通全自動運行系統進行介紹,以典型運營場景為例對全自動運營場景進行梳理,分析關鍵裝備的功能需求以及各設備專業之間的接口關系。文獻[6]結合國際標準研究全自動運行系統典型的系統功能與安全需求,對運營場景進行分析,對國內自主研發全自動運行系統提出參考建議。文獻[7]分析了CBTC-RF 信號系統駕駛模式及模式間轉換應遵循的原則。
目前,全自動運行系統的研究主要集中在系統方案和仿真分析,對測試用例生成方法的研究較少。時間自動機具有嚴格的數學定義,在軌道交通測試建模領域取得了廣泛的應用[8-10]。本文結合全自動運行系統的特點,針對全自動運行系統測試用例生成過程中存在的指定路徑覆蓋的需求,基于時間自動機建模理論,提出全自動運行系統的測試用例自動生成方法,對全自動運行系統的安全性保障具有一定的意義。
時間自動機(Timed Automata,TA) 由Stanford 大學的Rajeev Alur 和David Dill 于20世紀90 年代提出。時間自動機對有限自動機進行了擴展,使用有限個時鐘變量表示有時間約束的狀態轉換圖,進而描述系統的實時行為[11-12]。
定義1 (時間自動機)TA 定義為一個六元組〈S,S0,Σ,X,I,E〉,其中:
S是有窮位置的集合;
S0是初始事件的集合;
Σ是有窮事件的集合;
X是有窮時鐘的集合;
I是每個位置的映射,對s∈S指定Φ(x)中一個時間約束δ;
E?S×Σ×Φ(x)×2x×S表示位置轉移的集合。
〈s,a,φ,λ,s'〉 表示輸入動作a時,從位置s到s'的轉移;φ是X上的一個時鐘約束,在轉移發生時被滿足;λ∈X是在該轉移發生時復位的時鐘集合。
UPPAAL 是由瑞典Uppsala 大學和丹麥Aalborg 大學聯合開發的針對TA 理論的建模、驗證和測試用例生成工具。UPPAAL 拓展了TA 理論,擴展出變量和通道等元素,UPPAAL 提供Yggdrasil從TA 模型自動生成測試用例[13],包括3 個階段:
1)Query File,Yggdrasil 加載驗證Query文件,將可達性分析的路徑轉換為測試用例;
2)Depth Search,采用隨機深度優先搜索算法,將搜索所得路徑自動轉換為測試用例;
3)Single Step,針對階段1)和階段2)中未覆蓋的邊進行可達性分析生成測試用例,直到覆蓋模型中所有的邊。
全自動運行系統的測試用例主要由測試人員依據經驗人工編制,通常由測試人員根據積累的測試關鍵項,指定測試過程中的某幾個步驟,或指定某幾個環節之間需要滿足的條件,然后人工編制完整的測試用例。全自動運行系統交互復雜,測試步驟較多,人工編制測試用例存在效率低、容易遺漏測試需求等問題[14]。
定義2(指定路徑覆蓋) 測試需求包含一個測試路徑集合P,其中P以參數的形式給出。
如圖1 所示,TAex模型包括6 個位置,根據測試經驗,測試用例需要測試S4 →S5 →S6指定的測試路徑,即指定測試路徑覆蓋:P={(S4,S5),(S5,S6)}。

圖1 TAex模型示例Fig.1 TAex model example
Yggdrasil 生成測試用例時不考慮指定路徑覆蓋。如圖1 所示的TA 模型,Yggdrasil 生成如下4條測試用例,未覆蓋指定的測試需求P,不能滿足全自動運行系統指定路徑覆蓋的要求。
1)S0 →S3 →S4;
2)S0 →S2 →S6;
3)S0 →S3 →S4 →S5;
4)S0 →S1 →S5 →S6。
基于以上問題,提出全自動運行系統測試用例生成方法。首先,在全自動運行系統功能模型的基礎上增加測試標記變量,達到在模型的邊或節點位置上描述測試人員指定測試需求的目的,即在全自動運行系統的功能模型中表征測試人員指定的測試路徑需求,形成全自動運行系統的測試模型。測試標記變量僅用于反應測試人員指定的測試需求,不改變全自動運行系統模型的功能邏輯;然后,編制測試人員指定的測試需求的Query 文件,以Yggdrasil 的Query File 測試用例生成方法對驗證文件生成測試用例,滿足測試人員的指定路徑覆蓋;最后,針對尚未覆蓋的邊,利用UPPAAL 的Depth Search 和Single Step 方法生成測試用例,實現100% 邊覆蓋,如圖2 所示。

圖2 測試用例生成流程Fig.2 Test case generation process
設U表示全自動運行系統測試人員指定的路徑覆蓋需求集,t表示算法當前迭代生成的測試用例,R表示算法生成的測試用例集。全自動運行系統測試用例生成算法如圖3 所示。算法開始時,R是一個空集。算法每次迭代生成一條測試用例,將該測試用例添加到R中,直到算法結束。

圖3 測試用例生成算法Fig.3 Test case generation algorithm
以圖1 所示的模型為例,指定路徑覆蓋為(S4,S5),(S5,S6)。對邊(S4,S5)和(S5,S6)分別增加測試標記的int 變量b45 和b56。滿足指定路徑覆蓋的驗證性質為:q::=E<>b45 andb56 。
采用算法1,Yggdrasil 生成3 條測試用例,100% 實現邊覆蓋,且測試用例3 覆蓋指定路徑覆蓋的需求。
1)S0 →S1 →S5;
2)S0 →S2 →S6;
3)S0 →S3 →S4 →S5 →S6。
以全自動運行系統模式轉換功能為例,介紹全自動運行系統的測試用例生成方法。
全自動運行系統模式轉換功能包括TIAS、司機、VOBC 與列車4 個參與者,功能流程如圖4 所示。全自動運行系統投入運營時,TIAS 將遠程喚醒指令發送到VOBC,VOBC 與車輛進行自檢,喚醒列車進入FAM 模式待命。列車以FAM 模式運行過程中出現車輛與VOBC 通信故障等情況時,系統申請進入CAM 模式,經TIAS 人工授權后,系統駕駛模式由FAM 模式轉換為CAM 模式。FAM 模式運行過程中,若列車遇到特殊情況需要降級時,列車停穩后,激活相應端的司機室鑰匙,車載VOBC 退出FAM 模式,進入CM 模式,轉入人工駕駛[15]。

圖4 全自動運行系統模式轉換流程序列Fig.4 FAO mode conversion process sequence diagram
根據全自動運行系統模式轉換流程建立全自動運行系統的TA 模型,并采用全自動運行系統測試用例生成算法生成測試用例。
全自動運行系統模式轉換流程包括TIAS、列車、司機和VOBC 4 個子系統,模式轉換的TA模型MODETA為各個子系統的TA 模型的積:MODETA=TIASTA||VOBCTA||DRIVERTA||TRAINTA。
其中,TIASTA主要完成TIAS 信息的發送和接受、列車動作授權的處理等功能;VOBCTA主要執行列車在模式轉換流程中的動作,包括列車上電自檢、升級條件的檢查、列車運行中故障信息的發送以及模式轉換;DRIVERTA主要模擬司機在模式轉換流程中手動操作鑰匙開關和模式轉換確認;TRAINTA主要輸出列車速度信息和非激活端換端等操作。
MODETA如圖5 所示,共含58 個位置、90 個遷移、27 個通道和13 個變量,主要變量名稱及其含義如表1 所示。

表1 MODETA位置及變量含義Tab.1 MODETA location and variable meaning
以CM 模式轉換到FAM 模式為例,介紹測試用例生成過程。根據專家經驗,模式轉換具有如表2 所示的測試需求。
根據全自動運行系統測試用例生成算法,為表征測試場景,MODETA模型中包含了測試標記的int 變量,主要變量如表3 所示。

表3 測試模型中的主要變量Tab.3 Main variables in test model
測試需求1 ~4 對應的BNF 驗證語句如表4所示。

表4 CM轉FAM模式測試需求及驗證性質Tab.4 Test requirements and verification properties of conversion of CM to FAM mode
利用UPPAAL 的Query 文件生成測試用例,針對表2 的4 個測試需求,生成4 條測試用例。以測試用例1 為例,其覆蓋測試場景1,測試過程如下:測試初始為CM 模式,列車速度不為0,司機制動將列車速度降為0 后,操作方向手柄至零位,操作制動手柄至零位,VOBC 檢測列車最高駕駛模式指令為全自動駕駛模式,提示司機確認模式轉換,但司機未確認該信息。同時,列車超速,司機將列車速度制動為0 后,確認模式轉換,列車轉換至FAM 模式。
利用Yggdrasil 的Depth Search 和Single Step 方法對模型中未覆蓋的邊繼續生成測試用例,新生成14 條測試用例,其中Depth Search 方法生成1 條測試用例,Single Step 方法生成13 條測試用例。即算法一共生成18 條測試用例,邊覆蓋率為100%,且完全覆蓋測試人員指定的4 條測試需求。
本文針對全自動運行系統測試用例編制過程中的指定路徑覆蓋問題,研究時間自動機建模理論,提出了基于Yggdrasil 的指定路徑覆蓋測試用例自動生成算法。以全自動運行系統的模式轉換功能為例,建立模式轉換的時間自動機模型,并采用論文提出的算法生成測試用例。結果表明,論文生成的測試用例100% 覆蓋測試人員指定的測試需求,同時100% 覆蓋時間自動機模型中所有的邊,能夠滿足全自動運行系統指定路徑覆蓋的測試用例生成要求。