郭昊男，呂繼東，柴 銘，劉宏杰，唐 濤

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

輸入/輸出一致性測試(IOCO)，在嚴(yán)格的環(huán)境假設(shè)基礎(chǔ)上，通過環(huán)境產(chǎn)生測試激勵施加于被測系統(tǒng)并根據(jù)實際輸出與預(yù)期輸出的一致性關(guān)系，判斷被測系統(tǒng)是否滿足功能需求約束[1]，是驗證車載ATO控制邏輯正確性與安全性的重要手段，近年來國內(nèi)外學(xué)者已進行了大量的研究[2-6]。

基于模型的在線測試方法是針對黑盒系統(tǒng)的IOCO新方法[7],將測試激勵實時施加于真實被測系統(tǒng)，并實時對比實際被測系統(tǒng)與其需求模型的輸出，根據(jù)二者一致性關(guān)系判斷被測系統(tǒng)是否滿足需求規(guī)范。

同傳統(tǒng)離線測試相比，在線測試能夠根據(jù)被測系統(tǒng)實時輸出確定系統(tǒng)的行為軌跡，避免了不確定性帶來的測試案例數(shù)量爆炸，提高了測試的完備性[8]。時間自動機理論建模方法在完整的數(shù)理邏輯基礎(chǔ)上對時間系統(tǒng)進行刻畫，能夠?qū)ο到y(tǒng)安全需求進行嚴(yán)格與充分的驗證[9-10]。本文使用的UPPAAL-TRON測試工具以時間自動機模型為測試依據(jù)，實現(xiàn)了基于模型的在線一致性測試方法。

本文采用基于時間自動機模型的在線一致性測試方法驗證車載ATO自動控車命令生成設(shè)計原理和具體實現(xiàn)同功能需求是否一致。首先分析了追蹤場景下的ATO邏輯功能和安全特性，提出車載ATO在線測試的一致性需求；然后定義場景中各部分的一致性輸入/輸出接口，建立了相關(guān)自動機網(wǎng)絡(luò)模型并形成了在線測試框架；最后通過變異分析，針對車載ATO軟件典型的實現(xiàn)錯誤(錯誤的安全距離、靜態(tài)限速、功能邏輯以及命令丟失等)，進行安全性驗證。結(jié)論表明，該在線一致性測試方法能夠及時檢測出車載ATO軟件行為與規(guī)范模型的不一致，為未來CBTC的進一步研發(fā)與安全驗證提供一定的理論參考。

1 ATO功能介紹及應(yīng)用場景分析

具有ATO功能的列車運行控制系統(tǒng)見圖1，系統(tǒng)根據(jù)列車運行情況反饋及通過線路情況，自動調(diào)整目標(biāo)距離、目標(biāo)速度，實現(xiàn)列車的自動運行。通常ATO在設(shè)計時不會直接考慮ATP限速，而是由ATP直接對列車速度進行監(jiān)督[11]，這種方式雖然能夠保證運行安全，但可能造成正常情況下列車緊急停車，本文所討論的ATO子系統(tǒng)融合了ATP功能。

本文選取CBTC中典型的兩車追蹤控制運行過程作為測試場景，并使用該場景下的列車運行安全需求作為驗證依據(jù)。CBTC系統(tǒng)連續(xù)模式下兩車追蹤運行場景中系統(tǒng)的通信與控制過程見圖2。列車每個周期將自己的運行方向、列車位置、速度等信息通過軌旁無線接入點(AP)并經(jīng)由數(shù)據(jù)通信系統(tǒng)發(fā)送至相應(yīng)的區(qū)域控制器(ZC)①、區(qū)域控制器綜合數(shù)據(jù)服務(wù)單元(DSU)②、聯(lián)鎖系統(tǒng)(CI)③、以及車載提供的信息后，實時計算出列車的移動授權(quán)(MA)，并經(jīng)由數(shù)據(jù)通信系統(tǒng)通過軌旁無線接入點下發(fā)給相應(yīng)列車④、⑤、⑥。列車收到MA后，車載ATP根據(jù)MA中的授權(quán)終點距離、線路限速等信息計算列車的距離-速度安全防護曲線，車載ATO在安全防護曲線的監(jiān)督下，生成控車命令，控制列車自動運行⑦。

上述場景中，每周期前后兩車分別向ZC報告列車位置、速度等消息(即圖2中①、②、③過程)的時序存在不確定性，因此使用離線測試方法難以做到完備測試。本文主要研究使用基于UPPAAL-TRON在線一致性測試方法，驗證上述典型的具有實時性和不確定性的運行場景下ATO控制邏輯是否滿足列控系統(tǒng)安全需求。

2 基于模型的在線測試?yán)碚摲椒?/h2>

2.1 時間輸入/輸出變遷系統(tǒng)及相關(guān)時間一致性關(guān)系

A為系統(tǒng)的可觀測行為集，由輸出行為Aout和輸入行為Ain組成。τ為系統(tǒng)不可觀測行為,τ?A,記Aτ=A∪{τ}。時間輸入/輸出變遷系統(tǒng)TIOTS(Timed Input/Output Transition Systems)定義為[12]：

定義1TIOTS由一個五元組(S,s0,Ain,Aout,T)表示。其中：S是狀態(tài)的集合；s0?S，表示初始狀態(tài)集合；T表示一個變遷：T?S×(Aτ∪d≥0)×S，且具有性質(zhì)：

其中,d∈R≥0,d為非負(fù)實數(shù)，R為實數(shù)。

σ∈(A∪d≥0)*為一個可觀測時間軌跡，σ=d1a1d2a2…akdk+1，且σ∈Aτ∪R≥0，d,d1,d2,…,dn∈R≥0。其中R為實數(shù)。

定義TTr(s)為一個狀態(tài)s的可觀測時間軌跡為

( 1 )

對于狀態(tài)s(及S′?S)和時間軌跡σ，sAfterσ表示s執(zhí)行σ遷移后的可達(dá)狀態(tài)集合，其定義為

( 2 )

( 3 )

定義可觀測輸出集Out(s)，表示由狀態(tài)s(s∈S′?S)產(chǎn)生的可觀測輸出行為集合(或者時間延遲)

( 4 )

( 5 )

定義2e∈E表示某一確定的系統(tǒng)運行環(huán)境，i,s∈S表示系統(tǒng)狀態(tài)，則環(huán)境相關(guān)時間輸入/輸出一致性關(guān)系RTIOCOe[10]為

iRTIOCOes=?σ∈TTr(e)

Out((i,e)Afterσ)?Out((s,e)Afterσ)

( 6 )

式中:(i,e)為實際設(shè)備狀態(tài)集；(s,e)為規(guī)范系統(tǒng)狀態(tài)集；上述一致性關(guān)系含義為：設(shè)備i在運行環(huán)境e激勵下，其任何可觀測輸出以及時間延遲必須滿足設(shè)備行為模型s在同一環(huán)境模型e的激勵下產(chǎn)生的輸出以及時間延遲。

2.2 基于UPPAAL-TRON在線一致性測試方法原理

基于模型的一致性測試原理[13-14]見圖3，分為系統(tǒng)層、模型層和測試層3個層次。

(1) 系統(tǒng)層：包含實際被測系統(tǒng)和真實運行環(huán)境，二者通過規(guī)定的輸入/輸出接口進行交互。

(2) 模型層：是對系統(tǒng)層中環(huán)境、設(shè)備以及輸入/輸出接口的數(shù)學(xué)抽象，它形式化地描述了環(huán)境以及設(shè)備的行為規(guī)范，并通過可觀測的輸入/輸出接口將二者耦合在一起。

(3) 測試層：為減少測試對運行環(huán)境的依賴，在模型層中使用環(huán)境模型ε定義被測設(shè)備的運行環(huán)境在可觀測輸入/輸出接口上的行為，測試層根據(jù)環(huán)境模型的描述產(chǎn)生相應(yīng)的輸入/輸出激勵代替真實環(huán)境同實際被測系統(tǒng)進行交互，并根據(jù)實際被測系統(tǒng)與設(shè)備模型M間的一致性關(guān)系得出測試結(jié)論。

基于UPPAAL-TRON的在線一致性測試工具可實現(xiàn)上述測試原理，見圖4，圖中符號“！”表示發(fā)送、“？”表示接收(下同)。TRON根據(jù)環(huán)境模型產(chǎn)生輸出序列代替真實的環(huán)境輸入，并判斷實際被測系統(tǒng)(IUT)的輸出是否符合其需求規(guī)范模型的描述。由于工具TRON產(chǎn)生的輸入/輸出(in與out)是依賴于TIOA模型描述的符號語言，需要使用適配器在其和IUT實際物理輸入/輸出接口(input與output)之間做對應(yīng)關(guān)系轉(zhuǎn)換。

3 車載ATO一致性在線測試設(shè)計

3.1 整體結(jié)構(gòu)

基于UPPAAL-TRON的在線一致性ATO功能測試框架見圖5。

(1) 測試環(huán)境

① 測試規(guī)范：測試規(guī)范是整個運營場景中的各部分交互的自動機網(wǎng)絡(luò)模型，包括列車動力學(xué)自動機模型(Train0、Train1)，車載ATO自動機模型(ATO0，ATO1)，區(qū)域控制器ZC自動機模型，同步時鐘自動機模型(Timer)。

② UPPAAL-TRON工具：工具UPPAAL用于對實時系統(tǒng)進行時間自動機模型網(wǎng)絡(luò)的建模、校驗和驗證。TRON是基于時間自動機模型網(wǎng)絡(luò)的在線一致性測試工具，它根據(jù)UPPAAL建立的模型(XML格式數(shù)據(jù))對實際系統(tǒng)進行一致性測試。

(2) 被測系統(tǒng)

① ATO仿真軟件：實際的車載ATO設(shè)備物理和邏輯結(jié)構(gòu)復(fù)雜，測試周期長，難度大。本文借助計算機程序設(shè)計車載ATO仿真軟件并測試，一方面降低了測試復(fù)雜度，另一方面能夠改變軟件內(nèi)部結(jié)構(gòu)研究在線測試方法對軟件設(shè)計中錯誤及異常的檢測能力。

② 適配器(Adapter)：為了將自動機網(wǎng)絡(luò)中符號化的輸入/輸出通道和實際被測系統(tǒng)的輸入/輸出接口進行匹配，TRON提供了基于TCP/UDP通信的轉(zhuǎn)換匹配協(xié)議用于在測試工具和被測系統(tǒng)之間構(gòu)建適配器。

(3) 運行原理

ATO在運行過程中需要同ZC、時鐘、列車等進行交互，在基于模型的在線一致性測試中，測試工具將使用相應(yīng)的時間自動機模型產(chǎn)生輸入激勵與真實ATO進行交互，并根據(jù)真實ATO返回的信息與ATO模型返回的信息進行比對，通過二者的一致性關(guān)系得出測試結(jié)論。由于ATO的輸出為控車命令，不易理解與分析，本文使用列車的位置速度作為可觀測輸入/ 輸出接口上的數(shù)據(jù)監(jiān)控列車運行。

3.2 自動機網(wǎng)絡(luò)接口

根據(jù)圖5中被測系統(tǒng)的模型網(wǎng)絡(luò)結(jié)構(gòu)，可定義相關(guān)的可觀測輸入/輸出通道。其中，用帶方向的箭頭表示設(shè)備交互行為，箭頭下方的通道名表示設(shè)備之間發(fā)送或者接收可觀測消息的行為。

自動機網(wǎng)絡(luò)中的可觀測通道見圖6，其含義分別為：時鐘自動機每周期通過syn信號使Train0和Train1同步工作；Train0和Train1在每周期的同步信號到來后，向ZC發(fā)出lvtoZC消息報告自己當(dāng)前的位置和速度, ZC在收到消息后將更新兩車的移動授權(quán)；此外Train0和Train1每周期分別向ATO0和ATO1發(fā)送request消息，請求行車命令。ATO0與ATO1在收到列車的請求消息后，根據(jù)ZC給出的最新的MA計算行車命令，keep、acce、nbrake、ebrake分別表示巡航命令、加速命令、常用制動命令以及緊急制動命令。

3.3 UPPAAL時間自動機模型

(1) 列車動力學(xué)模型

列車運行的動力學(xué)過程時間自動機見圖7，由圖中虛線框所劃分的?～⑤六個主要狀態(tài)組及其之間的相互轉(zhuǎn)移關(guān)系構(gòu)成。?為自動機邏輯起點，①～⑤分別為1個周期中列車巡航、停車、常用制動、加速、緊急制動運行過程。圖7中相關(guān)的符號含義見表1。

表1 列車自動機符號說明

符號類型含義IDint列車編號Startlocation列車自動機起始位置tclock列車時間自動機內(nèi)部時鐘STOPlocation周期開始處于停車狀態(tài),速度為零train_v[ID]arrayslot編號為ID的列車(以下簡稱列車ID)的速度KEEPlocation周期開始處于巡航狀態(tài)train_s[ID]arrayslot列車ID的位置ACCElocation周期開始處于加速狀態(tài)Tint時間周期NBlocation周期開始處于常用制動狀態(tài)a1[ID]arrayslot加速度EBlocation周期開始處于緊急制動狀態(tài)ebrakea[ID]arrayslot最小緊急制動減速度move(k)function巡航運行一周期的動力學(xué)過程nbrakea[ID]arrayslot當(dāng)前常用制動減速度move(a)function加速運行一周期的動力學(xué)過程syn?channel時鐘同步消息move(n)function常用制動運行一周期的動力學(xué)過程lvtoZC[ID]channel位置、速度消息move(e)function緊急制動運行一周期的動力學(xué)過程request[ID]channel請求消息t<2boolean在2個單位時間內(nèi)keep[ID]channel巡航命令train_v[ID]>0boolean列車ID速度大于0acce[ID]channel加速命令train_v[ID]==0Boolean列車ID速度等于0nbrake[ID]channel常用制動命令t=0clockreset時鐘置0操作ebrake[ID]channel緊急制動命令

以圖7狀態(tài)組①為例說明列車運行一個周期的過程。其動作序列描述為：(a)周期開始自動機處于KEEP位置，表示列車處于巡航狀態(tài)。(b)當(dāng)列車收到時鐘同步消息syn后，將內(nèi)部時鐘t置為0，并遷移至下一匿名位置。(c)在兩個單位時間內(nèi)(t<2)，列車通過lvtoZC[ID]消息向ZC發(fā)送當(dāng)前的位置和速度報告，并遷移至下一匿名位置。(d)在兩個單位時間內(nèi)(t<2)，列車向ATO發(fā)出request[ID]消息用于請求行車命令，并遷移至下一位置。(e)自動機執(zhí)行move(k)函數(shù)，并遷移至狀態(tài)組中的最末位置，準(zhǔn)備向其它狀態(tài)組轉(zhuǎn)移。move(k)函數(shù)依照牛頓第二定律描述了列車在巡航狀態(tài)下一個周期內(nèi)的走行距離變化，動力學(xué)方程為

train_s[ID]=train_s[ID]+train_v[ID]×T

圖7中反映的狀態(tài)組①向其它狀態(tài)組的轉(zhuǎn)移關(guān)系見表2。

表2 狀態(tài)組①轉(zhuǎn)移關(guān)系

當(dāng)時間自動機運行至狀態(tài)組①的最后一個位置，將根據(jù)收到的ATO消息轉(zhuǎn)移至相應(yīng)的目標(biāo)位置。例如當(dāng)收到acce[ID]消息時，自動機將從當(dāng)前位置轉(zhuǎn)移至狀態(tài)組④的ACCE位置。

其余狀態(tài)組動作過程類似，僅是動力學(xué)方程或控制邏輯稍有不同，需要特別說明的是：

(a) 實際制動過程中，列車可能在任意時刻停車，由于模型是周期運行，為了防止出現(xiàn)負(fù)速度與位置偏差，對制動過程(④、⑤)增加了速度合法性判斷與參數(shù)補償邏輯。

(b) 自動機一旦進入狀態(tài)組⑤將一直停留在狀態(tài)組⑤直至停車，表示緊急制動過程不能緩解。

(2) 車載ATO模型

ATO時間自動機模型見圖8，由圖8中虛線框所劃分的?～②三個功能模塊及其之間的相互轉(zhuǎn)移關(guān)系構(gòu)成，主要作用分別是：參數(shù)初始化，速度防護以及命令觸發(fā)。圖中部分標(biāo)識符含義已經(jīng)在表1中說明，其余符號含義見表3。

圖8中模塊①集成了車載ATP的超速防護功能，控制邏輯見算法1。算法1與自動機模型對應(yīng)關(guān)系為：第1～3行牽引假設(shè)對應(yīng)圖8中模塊?匿名位置至模塊①位置1之間的遷移，它考慮在上一時刻(-T)ATO輸出加速命令(最不利情況)，若當(dāng)前時刻(0)ATO也輸出加速命令，則下一時刻(T)ATO輸出相應(yīng)制動命令時，列車能否在MA限制內(nèi)安全停車。

不同制動曲線對列車運行過程所做的假設(shè)條件見圖9。圖9(a)中0～T階段列車執(zhí)行上一時刻ATO輸出的加速命令；T～2T階段列車執(zhí)行當(dāng)前時刻(0)ATO輸出的加速命令；2T～3T階段表示列車在T時刻的緊急制動命令下，列車牽引力被解除，制動力未施加時的惰行過程；3T～6T階段表示弱常用制動條件下列車在預(yù)留反應(yīng)時間(3T)內(nèi)的運行過程；6T～9T階段表示列車在制動力作用下至停車的過程。ev表示此過程中列車能夠達(dá)到的最大速度，曲線圍成的面積表示列車從當(dāng)前時刻位置至停車點的走行距離。圖9(b)～9(d)分別表示預(yù)留2T反應(yīng)時間的中常用制動、預(yù)留T反應(yīng)時間的強常用制動和緊急制動假設(shè)下的列車運行過程，margin表示在這些預(yù)留時間內(nèi)列車的運行距離。

表3 ATO自動機符號說明

第4～5行巡航假設(shè)對應(yīng)模型位置6到位置1之間的遷移，相較于加速假設(shè)，巡航假設(shè)列車運行過程中加速階段只有一個周期，其余階段均相同。7～13行的for循環(huán)對應(yīng)模型位置1、2、3及其之間的遷移，變量index的值由1到4分別對應(yīng)緊急制動觸發(fā)曲線以及強、中、弱常用制動觸發(fā)曲線。程序根據(jù)當(dāng)前命令假設(shè)依次判斷列車距離速度關(guān)系是否符合相應(yīng)的制動曲線約束，判斷結(jié)果與輸出命令對應(yīng)關(guān)系見表4。計算常用制動觸發(fā)曲線時，區(qū)段限速在MA給定值的基礎(chǔ)上保留2 m/s富余度。

第14～23行的while循環(huán)對應(yīng)位置3、4、5、6及其之間的內(nèi)部遷移，根據(jù)相應(yīng)命令輸出假設(shè)條件，結(jié)合當(dāng)前列車位置及速度判斷列車運行是否能夠遵從相應(yīng)的MA限制。

算法1ATO控制算法:

表4 約束關(guān)系與輸出命令

從列車當(dāng)前所在限速區(qū)段開始，計算列車制動力施加點位置到每一個限速區(qū)段終點位置的距離ed。其中：(a)conditon1()==evev2-nls2為列車能夠在MA終點前停車，并且不越過所有區(qū)段限速。

ATO首先考慮在牽引加速假設(shè)下，列車運動過程是否滿足condition1()與condition2()條件，如果滿足則表示ATO可給出加速命令，否則考慮巡航假設(shè)。如果巡航假設(shè)通過，則表示ATO可給出巡航命令，否則輸出相應(yīng)的制動命令。命令輸出過程見圖8模塊②。

(3) ZC時間自動機

區(qū)域控制器ZC時間自動機見圖10。在Start位置和Update位置之間有兩條路徑，分別表示ZC以不同的可能時序收到前車(編號0)和后車(編號1)發(fā)送的位置速度消息lvtoZC。變量ftrain表示前車的位置，前車依照線路靜態(tài)限速運行(終點為3 km)，后車以前車位置為移動授權(quán)終點運行。

(4) 時鐘自動機

時鐘自動機(下稱時鐘)見圖11，模型中的所有列車自動機(Train0，Train1)和ATO自動機(ATO0，ATO1)都使用時鐘發(fā)出的syn信號進行同步。系統(tǒng)運行開始時時鐘首先等待5個單位時間，對應(yīng)實際系統(tǒng)的上電初始化過程。之后將以10個單位時間為周期，每周期的前2個單位時間內(nèi)向列車發(fā)出時鐘同步信號。

3.4 被測軟件設(shè)計

被測軟件由仿真列車及車載ATO模塊和適配器組成，其中：

(1) 適配器 使用Java語言根據(jù)TRON的輸入 / 輸出接口配置流程在測試工具和被測系統(tǒng)之間構(gòu)建適配器軟件。其部分程序如Program1，其根據(jù)TRON規(guī)定的TCP協(xié)議格式進行輸入/輸出映射、仿真時間單位設(shè)置等工作。

Program1

public static oidconfig(int port) throws IOException{

initialTable();//初始化映射表

server=newServerSocket(port); //初始化socket

socket=server.accept();

//初始化輸入/輸出數(shù)據(jù)流

is=newDataInputStream(socket.getInputStream());

os=new DataOutputStream(socket.getOutputStream());

setIO();//根據(jù)映射表配置符號輸入/輸出與物理輸入/輸出

setTimeUnit(100 000); //設(shè)置測試時間單位

setTimeOut(3 000);//設(shè)置測試時長

os.writeByte(SA_TestExec);//開始執(zhí)行測試

os.flush();

}

(2) 被測軟件設(shè) 車輛仿真即遵照牛頓第二定律編寫的車輛在不同命令下位置速度隨時間的變化關(guān)系，ATO的控制算法已在算法1中詳細(xì)描述，程序?qū)崿F(xiàn)邏輯基本與模型描述一致。

4 模型驗證及結(jié)果分析

4.1 模型參數(shù)配置

(1) 線路參數(shù)：線路全長3 km，包含兩個靜態(tài)限速區(qū)段，范圍為0～2、2～3 km，分別對應(yīng)限速20、10 m/s。

(2) 車輛參數(shù)：兩車的動力特性相同，最大牽引加速度為1 m/s2,最小制動減速度為1 m/s2,弱、中、強常用制動減速度分別為1.1、1.2、1.3 m/s2，前后車初始位置分別0.5、0 km。

(3) 安全距離：后車MA終點位置距離前車當(dāng)前位置至少300 m。

(4) 仿真時間：模型中初始化時間為5個單位時間，運行周期為10個單位時間；測試框架中每個單位時間對應(yīng)物理時間100 ms。

4.2 模型驗證

模型建立后需要在此基礎(chǔ)上進行安全性質(zhì)驗證，UPPAAL提供了基于計算樹邏輯(CTL)的性質(zhì)描述語言及驗證器[15]。描述語言由路徑表達(dá)式和狀態(tài)表達(dá)式組成，前者規(guī)定了表達(dá)式在狀態(tài)路徑上的作用范圍，后者規(guī)定了有效范圍內(nèi)的狀態(tài)應(yīng)該滿足的邏輯約束。根據(jù)路徑表達(dá)式可以將驗證性質(zhì)分為可達(dá)性、安全性、存在性三類。可達(dá)性表達(dá)式E<>φ含義為給定狀態(tài)公式φ，存在一條從開始狀態(tài)出發(fā)的狀態(tài)路徑，沿著該路徑φ最終被滿足。安全性表示危險狀態(tài)永遠(yuǎn)不會發(fā)生; 表達(dá)式A[]φ表示對于任意可達(dá)狀態(tài)，φ始終被滿足；表達(dá)式E[]φ含義為存在一條狀態(tài)路徑，φ始終被滿足。存在性表示某些事件最終會發(fā)生; 表達(dá)式A<>φ含義為對于所有狀態(tài)路徑，φ最終都會被滿足；表達(dá)式φ-->ψ表示只要φ被滿足，ψ最終也會被滿足。根據(jù)ATO控制邏輯原理及安全要求，對相關(guān)性質(zhì)進行驗證，表達(dá)式及結(jié)果見表5。

表5 模型驗證結(jié)果

性質(zhì)(1)驗證自動機網(wǎng)絡(luò)中是否存在死鎖，系統(tǒng)可能因為死鎖而停留在危險的狀態(tài)；性質(zhì)(2)驗證ATO控制下兩車是否能保持300 m的安全車距；性質(zhì)(3)、(4)驗證列車在靜態(tài)限速區(qū)段是否遵守相應(yīng)的限速要求；性質(zhì)(5)表示列車緊急制動后一定會停車；性質(zhì)(6)表示在最后一個限速區(qū)段內(nèi)，前車一定能夠停下；性質(zhì)(7)表示存在列車速度不為0的停車狀態(tài)。以上性質(zhì)中(1)、(2)、(3)、(4)是列車運行的安全約束，性質(zhì)(5)、(6)、(7)則是對系統(tǒng)實現(xiàn)原理進行驗證，除性質(zhì)(7)外其余性質(zhì)均被驗證通過。因為列車停車狀態(tài)規(guī)定車速應(yīng)當(dāng)為零，(7)中描述的車速大于零的停車狀態(tài)不存在。形式化驗證進一步保證了系統(tǒng)實現(xiàn)機理的正確性及系統(tǒng)安全需求得到滿足。

4.3 仿真結(jié)果分析

根據(jù)上述配置方案使用UPPAAL-TRON測試工具對仿真車載ATO邏輯功能進行測試，結(jié)果見圖12，仿真時長為3 000個單位時間，mtu為model time unit 模型時間單位，在有效測試時間內(nèi)環(huán)境時鐘激勵下，仿真軟件的輸出結(jié)果和自動機模型網(wǎng)絡(luò)輸出結(jié)果完全一致(TEST PASSED)。

圖12 仿真車載ATO邏輯功能進行測試結(jié)果

兩車追蹤場景相關(guān)參數(shù)關(guān)系見圖13。圖13(a)為在相應(yīng)限速區(qū)段運行時列車速度符合靜態(tài)限速要求。圖13(b)為兩車位置隨時間的變化，開始時刻兩車距離500 m，到終點時兩車距離接近安全車距300 m。值得注意的是，兩車距離縮短過程總是發(fā)生在限速區(qū)段的分界點附近，這是因為在0～2 km限速區(qū)段，前車的MA終點遠(yuǎn)超后車MA終點，前車運行速度逐漸超過后車，兩車距離逐漸增加。前車到達(dá)限速區(qū)段分界點附近時，受2～3 km區(qū)段限速限制，車速逐漸降低，由于后車動作的遲滯性，后車速度超過前車速度，兩車距離逐漸減少。圖13(c)為后車速度相對于前車速度變化的遲滯性，表現(xiàn)為從一個限速區(qū)段到另一個限速區(qū)段，后車速度變化晚于前車速度變化。在正常運營場景下，遲滯性降低了前車速度對后車速度的影響程度，能夠讓后車運行過程更為平穩(wěn)，但在緊急場景下遲滯性增加了后車的反應(yīng)時間，對行車安全產(chǎn)生不利影響。圖13(d)為列車在收到時鐘信號后向ZC發(fā)送位置速度消息的時間間隔。不同的時序關(guān)系表明對于具有不確定性的系統(tǒng)，UPPAAL-TRON也能夠很好地工作。

在線測試過程中，前100個單位時間自動機網(wǎng)絡(luò)可達(dá)狀態(tài)集大小的變化以及相關(guān)信號發(fā)生時刻見圖14。以10到20單位時間內(nèi)的一個周期為例，ab段表示時鐘激勵信號發(fā)出后系統(tǒng)可達(dá)集增長的過程，ZC收到兩車速度位置信號不同的時序關(guān)系導(dǎo)致了可達(dá)空間的急速增長；在b點當(dāng)任意一輛列車首先發(fā)送速度位置報告后，之前的不確定時序關(guān)系就固定下來，因此bc段狀態(tài)空間又急速減小。針對具有不確定性的系統(tǒng)的測試問題，在線測試方法能夠根據(jù)被測系統(tǒng)實時反饋確定其行為路徑，避免了狀態(tài)空間增長導(dǎo)致的測試案例爆炸。

4.4變異測試

一致性測試的結(jié)果表明車載ATO軟件的行為符合自動機模型的描述，其原理滿足安全要求，實現(xiàn)符合規(guī)范描述。在此基礎(chǔ)上，通過一些變異算子對仿真軟件進行變異操作，驗證UPPAAL-TRON測試方法的檢錯能力，變異算子及測試結(jié)果描述如下：

(1) 錯誤的安全距離：系統(tǒng)實現(xiàn)中將安全距離300 m錯誤地編寫為200 m。測試結(jié)果見圖15(a)，圖中@為分隔符(下同)。測試工具檢測到系統(tǒng)實現(xiàn)在第166～169個單位時間內(nèi)的輸出結(jié)果與規(guī)范模型運行結(jié)果不一致，給出了測試失敗結(jié)論(TEST FAILED)。

(2) 錯誤的靜態(tài)限速：系統(tǒng)實現(xiàn)中將0～2 km區(qū)段的靜態(tài)限速20 m/s錯誤地編寫成22 m/s。測試結(jié)果見圖15(b)，檢測工具在第195～198個單位時間內(nèi)發(fā)現(xiàn)前車的距離速度與模型預(yù)期結(jié)果不一致，給出了測試失敗結(jié)論(TEST FAILED)。

(3) 邏輯錯誤：算法1超速防護邏輯實現(xiàn)中，將制動終點到當(dāng)前限速區(qū)段終點距離ed計算公式中a1*t2/2項錯寫為a1*t2測試結(jié)果見圖15(c)，檢測工具在第285～288個單位時間內(nèi)發(fā)現(xiàn)后車的位置與速度同模型預(yù)期不符，若列車按照當(dāng)前情況繼續(xù)運行可能產(chǎn)生危險。

(4) 命令丟失：在實際系統(tǒng)中，因為通信原因可能出現(xiàn)命令延遲與丟失等情況，在ATO仿真軟件中，可以模擬行車命令丟失的場景。測試結(jié)果見圖15(d)，檢測工具并沒有發(fā)現(xiàn)系統(tǒng)中存在的異常。檢查后發(fā)現(xiàn)雖然運行過程中ATO丟失了一個巡航命令，但是在實際設(shè)計中如果列車在一個周期內(nèi)沒有收到行車命令，將會參照上一個周期的命令繼續(xù)運行，而上一個周期ATO發(fā)出的恰好也是巡航命令，因此在外部可觀測通道上，仿真系統(tǒng)的輸出行為和規(guī)范模型的輸出結(jié)果完全一致。

圖15 變異測試結(jié)果

以上4個變異測試在一定程度上反映了UPPAAL-TRON方法對于不確定實時系統(tǒng)的在線監(jiān)測能力，同時圖15(d)也揭示了該方法的一點不足。對黑盒測試而言，測試者(或測試工具)只能觀察到被測系統(tǒng)與外界環(huán)境的交互行為，因此測試只能在可觀測的輸入/輸出接口上進行，當(dāng)內(nèi)部錯誤未影響到交互接口時,如圖15(d)，該錯誤就無法被檢測。事實上，當(dāng)被測系統(tǒng)內(nèi)部存在邏輯錯誤時，基本都能以錯誤的輸出形式表現(xiàn)出來，但是具有一定的隨機性與不確定性，需要通過完備的測試環(huán)境激勵及較大規(guī)模的重復(fù)測試來捕獲。在不了解被測系統(tǒng)具體實現(xiàn)的情況下，針對黑盒系統(tǒng)的在線一致性測試方法能夠較好地檢驗被測系統(tǒng)實現(xiàn)是否符合相應(yīng)的需求規(guī)范及安全約束。在掌握系統(tǒng)具體實現(xiàn)細(xì)節(jié)的情況下，對于外部難以檢驗的行為，可以使用白盒測試如單元測試等來提高系統(tǒng)的可靠性，對于內(nèi)部組件間的交互行為可以通過集成測試等手段來提高安全性。在條件允許的情況下(可以進入系統(tǒng)內(nèi)部進行測試)，應(yīng)當(dāng)使用多種測試方法充分發(fā)揮不同測試手段的優(yōu)點，針對具體問題展開測試，提高系統(tǒng)的安全性，可靠性及穩(wěn)定性。

5 結(jié)束語

本文采用基于模型的在線一致性測試?yán)碚摷胺椒?，針對CBTC車載ATO的安全功能進行測試與分析，結(jié)果表明在線一致性測試方法能夠?qū)崟r地監(jiān)控被測系統(tǒng)可觀測輸入/輸出接口上的變化，動態(tài)追蹤系統(tǒng)運行軌跡，有效地避免了傳統(tǒng)離線測試的狀態(tài)空間爆炸問題，提高了對CBTC車載ATO軟件的檢錯能力與測試效率，為未來CBTC的進一步研發(fā)與安全驗證提供一定的理論參考。此外，將進一步研究在線測試方法在混合測試中的應(yīng)用，研究采用多種測試手段提高測試完備性，保證被測系統(tǒng)安全可靠。