基于在線一致性測試?yán)碚摰腃BTC車載ATO功能測試研究

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

( 1 )

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

( 2 )

( 3 )

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

( 4 )

( 5 )

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

iRTIOCOes=?σ∈TTr(e)

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

( 6 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(3) 運(yùn)行原理

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

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

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

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

3.3 UPPAAL時(shí)間自動(dòng)機(jī)模型

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

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

表1 列車自動(dòng)機(jī)符號(hào)說明

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

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

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

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

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

(2) 車載ATO模型

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

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

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

表3 ATO自動(dòng)機(jī)符號(hào)說明

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

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

算法1ATO控制算法:

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

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

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

(3) ZC時(shí)間自動(dòng)機(jī)

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

(4) 時(shí)鐘自動(dòng)機(jī)

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

3.4 被測軟件設(shè)計(jì)

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

(1) 適配器 使用Java語言根據(jù)TRON的輸入 / 輸出接口配置流程在測試工具和被測系統(tǒng)之間構(gòu)建適配器軟件。其部分程序如Program1，其根據(jù)TRON規(guī)定的TCP協(xié)議格式進(jìn)行輸入/輸出映射、仿真時(shí)間單位設(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ù)映射表配置符號(hào)輸入/輸出與物理輸入/輸出

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

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

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

os.flush();

}

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

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

4.1 模型參數(shù)配置

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

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

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

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

4.2 模型驗(yàn)證

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

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

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

4.3 仿真結(jié)果分析

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

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

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

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

4.4變異測試

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

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

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

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

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

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

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

5 結(jié)束語

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