基于在線一致性測試理論的CBTC車載ATO功能測試研究

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

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

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

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

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

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

1 ATO功能介紹及應用場景分析

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

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

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

2 基于模型的在線測試理論方法

2.1 時間輸入/輸出變遷系統及相關時間一致性關系

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

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

其中,d∈R≥0,d為非負實數，R為實數。

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

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

( 1 )

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

( 2 )

( 3 )

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

( 4 )

( 5 )

定義2e∈E表示某一確定的系統運行環境，i,s∈S表示系統狀態，則環境相關時間輸入/輸出一致性關系RTIOCOe[10]為

iRTIOCOes=?σ∈TTr(e)

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

( 6 )

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

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

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

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

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

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

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

3 車載ATO一致性在線測試設計

3.1 整體結構

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

(1) 測試環境

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

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

(2) 被測系統

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

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

(3) 運行原理

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

3.2 自動機網絡接口

根據圖5中被測系統的模型網絡結構，可定義相關的可觀測輸入/輸出通道。其中，用帶方向的箭頭表示設備交互行為，箭頭下方的通道名表示設備之間發送或者接收可觀測消息的行為。

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

3.3 UPPAAL時間自動機模型

(1) 列車動力學模型

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

表1 列車自動機符號說明

符號類型含義IDint列車編號Startlocation列車自動機起始位置tclock列車時間自動機內部時鐘STOPlocation周期開始處于停車狀態,速度為零train_v[ID]arrayslot編號為ID的列車(以下簡稱列車ID)的速度KEEPlocation周期開始處于巡航狀態train_s[ID]arrayslot列車ID的位置ACCElocation周期開始處于加速狀態Tint時間周期NBlocation周期開始處于常用制動狀態a1[ID]arrayslot加速度EBlocation周期開始處于緊急制動狀態ebrakea[ID]arrayslot最小緊急制動減速度move(k)function巡航運行一周期的動力學過程nbrakea[ID]arrayslot當前常用制動減速度move(a)function加速運行一周期的動力學過程syn?channel時鐘同步消息move(n)function常用制動運行一周期的動力學過程lvtoZC[ID]channel位置、速度消息move(e)function緊急制動運行一周期的動力學過程request[ID]channel請求消息t<2boolean在2個單位時間內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狀態組①為例說明列車運行一個周期的過程。其動作序列描述為：(a)周期開始自動機處于KEEP位置，表示列車處于巡航狀態。(b)當列車收到時鐘同步消息syn后，將內部時鐘t置為0，并遷移至下一匿名位置。(c)在兩個單位時間內(t<2)，列車通過lvtoZC[ID]消息向ZC發送當前的位置和速度報告，并遷移至下一匿名位置。(d)在兩個單位時間內(t<2)，列車向ATO發出request[ID]消息用于請求行車命令，并遷移至下一位置。(e)自動機執行move(k)函數，并遷移至狀態組中的最末位置，準備向其它狀態組轉移。move(k)函數依照牛頓第二定律描述了列車在巡航狀態下一個周期內的走行距離變化，動力學方程為

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

圖7中反映的狀態組①向其它狀態組的轉移關系見表2。

表2 狀態組①轉移關系

當時間自動機運行至狀態組①的最后一個位置，將根據收到的ATO消息轉移至相應的目標位置。例如當收到acce[ID]消息時，自動機將從當前位置轉移至狀態組④的ACCE位置。

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

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

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

(2) 車載ATO模型

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

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

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

表3 ATO自動機符號說明

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

第14～23行的while循環對應位置3、4、5、6及其之間的內部遷移，根據相應命令輸出假設條件，結合當前列車位置及速度判斷列車運行是否能夠遵從相應的MA限制。

算法1ATO控制算法:

表4 約束關系與輸出命令

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

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

(3) ZC時間自動機

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

(4) 時鐘自動機

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

3.4 被測軟件設計

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

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

Program1

public static oidconfig(int port) throws IOException{

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

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

socket=server.accept();

//初始化輸入/輸出數據流

is=newDataInputStream(socket.getInputStream());

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

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

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

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

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

os.flush();

}

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

4 模型驗證及結果分析

4.1 模型參數配置

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

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

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

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

4.2 模型驗證

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

表5 模型驗證結果

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

4.3 仿真結果分析

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

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

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

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

4.4變異測試

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

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

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

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

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

圖15 變異測試結果

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

5 結束語

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