基于UPPAAL-TRON的高速鐵路列控系統(tǒng)非確定性時(shí)延一致性測試研究

呂繼東， 朱曉琳， 王海峰， 李開成, 唐 濤

(1. 北京交通大學(xué) 軌道交通運(yùn)行控制系統(tǒng)國家工程研究中心， 北京 10044; 2. 中國鐵道科學(xué)研究院 通信信號研究所, 北京 100044)

集成測試是保證高速鐵路列控系統(tǒng)功能正確性的重要途徑和手段。然而，由于CTCS-3級列控系統(tǒng)采用了GSM-R無線通信網(wǎng)絡(luò)實(shí)現(xiàn)信息交互，車載設(shè)備與無線閉塞中心RBC(Radio Block Center)設(shè)備的通信過程中存在非確定性的時(shí)間延遲(簡稱時(shí)延)，具有典型的實(shí)時(shí)性特征。因此，保證系統(tǒng)功能的正確性不僅要求設(shè)備在規(guī)定的時(shí)間約束內(nèi)做出正確的邏輯響應(yīng)，還要求系統(tǒng)能夠根據(jù)不同的非確定性時(shí)延采取變化的控制策略。如RBC接收車載設(shè)備消息，消息的不同非確定性時(shí)延將導(dǎo)致功能上的輸出邏輯也不同(如輸出正常的移動(dòng)授權(quán)或緊急制動(dòng))。如何在系統(tǒng)集成測試過程中，保證列控系統(tǒng)在時(shí)延非確定的情況下，列控系統(tǒng)能夠滿足功能上的正確性將尤為重要。

輸入輸出一致性測試基于嚴(yán)格的環(huán)境假設(shè)條件，通過將環(huán)境激勵(lì)信號施加于被測系統(tǒng)SUT(System Under Test)，判斷輸出結(jié)果與規(guī)范預(yù)期的一致性關(guān)系[1]，驗(yàn)證系統(tǒng)能否實(shí)現(xiàn)其功能上的正確性。目前國內(nèi)外列控系統(tǒng)功能一致性測試主要集中在測試案例生成方法的研究上，基于模型的測試MBT(Model-Based Testing)受到廣泛的關(guān)注[2-4]。MBT通過提供自動(dòng)化、可重復(fù)性、可選擇性的測試案例，避免了手工測試的主觀性，有助于提高測試案例的生成效率[5]。傳統(tǒng)的MBT主要基于離線測試方法OT(Offline Testing)，將測試用例的生成和執(zhí)行分離，因而限制了模型對非確定性的描述?；跁r(shí)間自動(dòng)機(jī)TA(Timed Automata)模型的離線測試方法廣泛的用于實(shí)時(shí)系統(tǒng)測試過程中[6-8]，通過建立確定性的時(shí)間自動(dòng)機(jī)時(shí)序模型，自動(dòng)生成相關(guān)的測試案例。離線測試方法需要輸入/輸出具有確定性，而且不同的時(shí)延會(huì)產(chǎn)生不同的測試案例，對于描述的實(shí)時(shí)系統(tǒng)很難生成完備的測試用例集[9]。

在線測試方法OT是一種針對集成黑盒系統(tǒng)的MBT新方法[10]，指的是基于模型產(chǎn)生唯一的(單步)測試原語(Test Primitive)，通過接口適配輸入到真實(shí)被測設(shè)備IUT(Implement Under Test)中立即執(zhí)行，即測試案例在生成的同時(shí)就被執(zhí)行；然后將實(shí)際設(shè)備的對應(yīng)輸出結(jié)果及時(shí)間戳與模型規(guī)范進(jìn)行一致性比對，據(jù)此產(chǎn)生新的輸入，如此反復(fù)至測試結(jié)束或檢測到錯(cuò)誤。測試過程記錄為一條加蓋有時(shí)間戳的輸入/輸出行為和時(shí)延的交替序列[9]，從而有效地解決了離線測試對時(shí)延非確定性描述不足的問題，適用于實(shí)時(shí)嵌入式系統(tǒng)的時(shí)延測試中。相比離線測試方法，在線測試在以下兩個(gè)方面具有一定的優(yōu)勢：

(1) 離線測試的測試案例自動(dòng)生成建立在確定性的時(shí)延模型基礎(chǔ)上，輸入/輸出具有確定性，而且不同的時(shí)延會(huì)產(chǎn)生不同的測試案例，從而造成被測系統(tǒng)的測試案例集異常龐大，而在線測試能夠針對時(shí)延非確定性的并發(fā)系統(tǒng)自動(dòng)生成滿足所有時(shí)延相關(guān)的測試案例，保證了測試的充分性；

(2) 離線測試案例在測試執(zhí)行之前生成，而在線測試能夠根據(jù)被測系統(tǒng)的實(shí)際輸出結(jié)果(不同的功能或者時(shí)延)實(shí)時(shí)調(diào)整測試案例的執(zhí)行，從而大大縮減了測試案例的執(zhí)行過程，提高了測試執(zhí)行的效率。

基于模型的黑盒一致性在線測試工具UPPAAL-TRON為該方法的實(shí)現(xiàn)提供了便利，如Mikucionis和Sasnauskaite對多列車并發(fā)通過橋梁場景進(jìn)行在線測試，分析得出了可能造成安全隱患的最大-最小時(shí)延界限[11]；隨后Larsen和Mikucionis等人將在線測試方法應(yīng)用到工業(yè)制冷設(shè)備控制中，通過測試恒溫器對室溫的跟蹤靈敏度進(jìn)行定量分析并證明了該方法的有效性[12]。本文基于時(shí)間狀態(tài)機(jī)理論，將基于模型的在線測試方法引入到列控系統(tǒng)非確定性時(shí)延的一致性測試中，通過對RBC切換場景中交互消息非確定性行為進(jìn)行建模描述，結(jié)合模型檢驗(yàn)工具UPPAAL和黑盒一致性測試套件UPPAAL-TRON，實(shí)現(xiàn)對列控系統(tǒng)實(shí)時(shí)性能的一致性在線測試。最終找出了仿真RBC測試模型與測試需求中不一致的地方，并通過改進(jìn)測試模型中RBC處理占用參數(shù)的設(shè)置，實(shí)現(xiàn)了RBC切換過程中跨界傳遞聯(lián)鎖消息時(shí)延非確定性的一致性測試，可以為我國下一代列控系統(tǒng)規(guī)范的制定和系統(tǒng)開發(fā)提供一定參考。

1 RBC切換邊界聯(lián)鎖信息不同步場景非確定性時(shí)延分析

RBC切換通常采用RBC直接通信的方式，但在特殊情況下也可以通過聯(lián)鎖間接聯(lián)系。在此方式下，RBC設(shè)備間不直接傳遞列控信息，而是通過各自分界點(diǎn)內(nèi)的聯(lián)鎖設(shè)備獲取軌道占用狀態(tài)，形成不同RBC分界點(diǎn)處交叉重疊的行車許可，從而實(shí)現(xiàn)列車在兩個(gè)RBC間行車許可控制的安全切換[14]。見圖1，聯(lián)鎖與RBC之間通信采用單點(diǎn)連接方式，當(dāng)一個(gè)RBC需要兩個(gè)聯(lián)鎖信息時(shí)，另一個(gè)聯(lián)鎖信息通過車站列控中心TCC(Train Control Center)傳輸至該聯(lián)鎖。

在實(shí)際列車信息傳輸過程中，跨界聯(lián)鎖間通信網(wǎng)路狀態(tài)直接影響消息的實(shí)時(shí)性能，導(dǎo)致非確定性時(shí)延。圖2是對上述場景中信息傳遞的路徑示意圖，列車運(yùn)行方向自右向左，則列車前方軌道占用信息自左向右(列車位置)傳遞。其中，邊界左側(cè)的軌道占用狀態(tài)信息由中繼1發(fā)送，經(jīng)過TCC1、聯(lián)鎖1、聯(lián)鎖2最終傳給RBC2，考慮信息傳輸過程中單個(gè)通道故障的最不利情況，從左側(cè)進(jìn)路軌間繼電器落下/吸起開始到右側(cè)RBC2收到占用/出清狀態(tài)的整個(gè)傳輸過程中，最大可能時(shí)延為TDelay_max=t0+T1+T2+T3；同理軌間繼電器狀態(tài)傳到RBC2的過程中最小可能時(shí)延為

TDelay_min=t0+t1+t2+t3

另一方面，車-地間實(shí)現(xiàn)無線通信的GSM-R網(wǎng)絡(luò)屬于文獻(xiàn)[15]定義的開放網(wǎng)絡(luò)，容易受到電磁干擾、小區(qū)切換等外界因素影響，導(dǎo)致RBC與列車傳送無線消息延遲，是非確定性時(shí)延的另一重要來源。CTCS-3級列控系統(tǒng)無線報(bào)文定義中對不同消息的發(fā)送周期、等待時(shí)間有不同要求，例如連續(xù)發(fā)送兩個(gè)位置報(bào)告消息M136的時(shí)間間隔默認(rèn)為6 s，但當(dāng)超過20 s車載系統(tǒng)仍未收到新的“安全”消息，則認(rèn)為系統(tǒng)斷鏈，視為故障狀態(tài)。

本文主要研究被測設(shè)備是否滿足這些時(shí)間上的限制以及時(shí)間非確定性帶來的功能邏輯正確性問題。該RBC切換場景的流程見圖3。

① 若RBC收到邊界內(nèi)(MA范圍內(nèi))的進(jìn)路占用狀態(tài)，應(yīng)立刻向車載設(shè)備發(fā)送CEM(有條件緊急停車)消息，該消息無需車載設(shè)備應(yīng)答；

② 若RBC收到邊界后第一段進(jìn)路的占用狀態(tài)，則等待一段反應(yīng)時(shí)間Tdelay判斷是否為本車占用，若非本車占用則發(fā)送SMA(縮短MA)消息，并需在Tack時(shí)間內(nèi)由車載設(shè)備響應(yīng)該消息；

③ 若RBC收到邊界后其他(非第1段)進(jìn)路的占用狀態(tài)信息，則RBC立刻向列車發(fā)送SMA消息，并需在Tack時(shí)間內(nèi)由車載設(shè)備響應(yīng)該消息；

④ 另外，若在列車尚未應(yīng)答SMA消息的前提下，RBC又收到MA范圍內(nèi)的軌道占用狀態(tài)信息，則RBC不再向列車發(fā)送CEM消息，而是升級發(fā)送UEM(無條件緊急停車)消息。

2 基于TRON的一致性在線測試框架

在線測試是一種典型的“黑盒”一致性測試，將系統(tǒng)看成“黑箱”(測試只關(guān)心系統(tǒng)的行為，不關(guān)心系統(tǒng)的內(nèi)部結(jié)構(gòu))。測試對象是實(shí)際設(shè)備，測試激勵(lì)來自于環(huán)境(與實(shí)際設(shè)備進(jìn)行交互的其他實(shí)際系統(tǒng))，兩者之間的輸入/輸出信息通過可觀測接口進(jìn)行觀測(該交互內(nèi)容和時(shí)序規(guī)定在被測系統(tǒng)的接口規(guī)范中)。例如，在環(huán)境約束條件確定的情況下(如列控系統(tǒng)的某個(gè)運(yùn)營場景)，被測設(shè)備的一致性測試。圖4為基于模型的相關(guān)一致性測試關(guān)系過程示意圖，分成系統(tǒng)層、模型層和測試層3個(gè)層次：

(1) 系統(tǒng)層：包含被測設(shè)備和實(shí)際環(huán)境。在環(huán)境約束條件確定的情況下，實(shí)際設(shè)備與實(shí)際環(huán)境之間的交互通過可觀測接口輸入/輸出行為。這些行為需要滿足相關(guān)的接口需求規(guī)范要求；

(2) 模型層：將系統(tǒng)層的輸入/輸出行為抽象成數(shù)學(xué)模型的過程。具體為實(shí)際環(huán)境抽象成環(huán)境模型，被測設(shè)備抽象成設(shè)備模型，環(huán)境模型和設(shè)備模型之間通過可觀測接口形成1個(gè)并發(fā)的系統(tǒng)模型。針對環(huán)境模型的每個(gè)輸入信息，其對應(yīng)期望的輸出信息均在系統(tǒng)模型的行為中進(jìn)行描述，并作為測試過程中的評判標(biāo)準(zhǔn)；

(3) 測試層：通過設(shè)計(jì)模型層和測試層之間的接口適配，將模型層中環(huán)境模型的每個(gè)輸入信息同時(shí)發(fā)給設(shè)備模型和真實(shí)設(shè)備；同理，真實(shí)設(shè)備也通過接口適配將輸出信息發(fā)送給環(huán)境模型。系統(tǒng)模型根據(jù)環(huán)境模型的輸入和真實(shí)設(shè)備的輸出，結(jié)合模型層中的評判標(biāo)準(zhǔn)，給出一致性測試的結(jié)論：通過或失敗。

UPPAAL-TRON (簡稱TRON)實(shí)現(xiàn)了上述測試?yán)砟?，它從?shí)際IUT及虛擬外界環(huán)境模型中產(chǎn)生和執(zhí)行在線測試[13]。取代了圖4中的測試工具，測試規(guī)范由時(shí)間自動(dòng)機(jī)模型工具UPPAAL完成，被測設(shè)備SUT和測試規(guī)范之間由TRON和適配器Adapter連接(具體應(yīng)用過程后述)，其在線測試框架見圖5。

圖5中，實(shí)際的IUT設(shè)備是被測方，一般為黑盒系統(tǒng)；工具TRON為測試者，扮演虛擬環(huán)境的角色，TRON一方面依據(jù)環(huán)境模型向IUT產(chǎn)生激勵(lì)，另一方面將收到的IUT反饋與設(shè)備的規(guī)范模型進(jìn)行比較，判定測試通過與否[17]。其中，UPPAAL時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型在設(shè)計(jì)過程中需充分考察對時(shí)間延遲非確定性的描述。

3 基于TRON的RBC切換場景一致性在線測試設(shè)計(jì)

3.1 環(huán)境和被測系統(tǒng)

在上述運(yùn)營場景規(guī)范中，RBC2作為典型的實(shí)時(shí)系統(tǒng)，既接收來自地面網(wǎng)絡(luò)聯(lián)鎖的通信信息，又接收來自無線的車載ATP信息，其邏輯相關(guān)功能和時(shí)間相關(guān)功能尤為重要，以典型的RBC2設(shè)備為案例(仿真RBC軟件程序)，進(jìn)行相關(guān)在線測試研究。因此，整個(gè)運(yùn)營場景的行為抽象成被測設(shè)備RBC2(IUT)模型和環(huán)境模型。由于在邊界聯(lián)鎖傳遞軌道占用信息的過程中，后車MA的擬定發(fā)送由RBC、聯(lián)鎖、TCC(列控中心)、中繼共同完成，為了簡化建模的復(fù)雜度，本文僅考慮聯(lián)鎖、TCC、中繼只考慮傳遞軌道占用狀態(tài)信息的邏輯功能和傳遞時(shí)間方面特征，故將3者簡化合并為一個(gè)整體對象，共同考慮其最大/最小時(shí)延，RBC切換場景的在線測試框架見圖6。

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

測試環(huán)境包含除RBC2設(shè)備相關(guān)的測試規(guī)范(由自動(dòng)機(jī)模型表示)和測試工具UPPAAL-TRON工具，其中,

① 測試規(guī)范：見圖6，測試規(guī)范是整個(gè)運(yùn)營場景中的列控系統(tǒng)交互的自動(dòng)機(jī)網(wǎng)絡(luò)模型，由環(huán)境時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型(RBC1，EVC1，EVC2，CBI1，CBI2，TCC1，TCC2以及通信延遲模型)和被測設(shè)備RBC2的時(shí)間自動(dòng)機(jī)模型(處理占用，處理位置和MA生成功能)組成；其中，通信延遲部分主要刻畫CBI1和EVC1與RBC2設(shè)備之間的傳輸延遲(地面和GSM-R)模型；

② 2UPPAAL-TRON：如前節(jié)介紹，該工具用來執(zhí)行測試規(guī)范(自動(dòng)機(jī)網(wǎng)絡(luò)模型，一般為XML文件)，接收環(huán)境時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型與設(shè)備的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型之間輸入輸出信息流，并發(fā)送給實(shí)際被測設(shè)備，反之亦然。

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

被測系統(tǒng)為RBC2設(shè)備，本文采用仿真軟件(PC機(jī)是硬件環(huán)境)實(shí)現(xiàn)，雖然該仿真不能替代真實(shí)設(shè)備和真實(shí)物理環(huán)境中的通信延遲，但通過設(shè)計(jì)仿真參數(shù)(延遲的大小)，在一定程度可以達(dá)到應(yīng)用方法和驗(yàn)證的目的。該軟件需要模擬真實(shí)環(huán)境中仿真功能和與環(huán)境模型相關(guān)的接口Adapter功能，其中,

① 仿真功能：仿真功能由邏輯功能和通信延遲功能組成。邏輯功能主要包括接收CBI1的占用信息(通過地面網(wǎng)絡(luò))，接收EVC2的無線消息和向EVC2發(fā)送移動(dòng)授權(quán)(MA)消息(通過無線網(wǎng)絡(luò))；通信延遲功能主要通過提取真實(shí)設(shè)備RBC2中完成RBC切換運(yùn)營場景的真實(shí)接口信息，進(jìn)行時(shí)序上的分析，得到通信延遲(地面以太網(wǎng)和GRM-R無線網(wǎng)絡(luò))的具體實(shí)現(xiàn)參數(shù)。

② Adapter：實(shí)現(xiàn)RBC2與環(huán)境模型之間的信息交互。利用TRON中提供的Adapter API功能函數(shù)，將TRON識別的抽象的符號化輸入/輸出映射到實(shí)際被測設(shè)備具體的輸入/輸出行為，定義TRON模型與被測軟件之間可觀測的輸入/輸出通道。環(huán)境模型通過該測試接口TRON提供外部輸入/輸出邏輯，并判別非法的輸入/輸出。設(shè)備模型是完全按照需求規(guī)范的要求表述的被測設(shè)備應(yīng)遵守的測試標(biāo)準(zhǔn)，該規(guī)范描述模型通過與環(huán)境模型和實(shí)際被測設(shè)備的輸入/輸出邏輯及對應(yīng)的時(shí)間戳進(jìn)行比對，從而找出實(shí)際設(shè)備與規(guī)范不一致的地方。

3.2 測試規(guī)范的接口定義

根據(jù)圖6中測試環(huán)境和被測設(shè)備之間的結(jié)構(gòu)關(guān)系，定義相關(guān)的可觀測輸入輸出消息。其中，帶方向的箭頭表示設(shè)備交互行為，箭頭下方的通道名表示設(shè)備之間發(fā)送或者接收可觀測消息的行為(“！”表示發(fā)送，“？”表示接收)；箭頭旁的賦值表示設(shè)備執(zhí)行發(fā)送或接收行為后進(jìn)行的本地操作。由于同一時(shí)段RBC要控制多輛列車，并且列車的位置和速度要實(shí)時(shí)更新，又增加了多車隊(duì)列控制QUEUE模塊。這里，模型緊緊考慮了EVC1進(jìn)入RBC1邊界第一個(gè)區(qū)段之前的狀態(tài)，沒有考慮列車注銷本RBC區(qū)域的功能及其EVC在相鄰RBC之間的受控運(yùn)行過程。

(1) 測試規(guī)范的可觀測接口定義

① RBC2與CBI2的可觀測接口

CBI2與RBC2之間主要完成列車位置占用信息交互的功能，其消息主要由可觀測接口OCCHRBC_req和OCCHRBC_info完成。見圖7。

② RBC2與EVC的可觀測接口

RBC2與EVC(EVC1，EVC2)之間的消息交互主要滿足CTCS-3級列控系統(tǒng)無線報(bào)文定義原則，其車-地通信的無線消息可以劃分為兩類：周期消息和非周期消息。周期性消息包括列車位置報(bào)告和請求MA，發(fā)送周期分別為6 s和60 s，RBC回復(fù)一般消息及MA信息，如果消息丟失則等待下一周期消息,見圖8。車-地的周期消息模型應(yīng)包含的可觀測消息有M136(位置報(bào)告消息)，M132(MA請求消息)。

非周期性消息即為場景功能消息，在列車啟動(dòng)或運(yùn)行到某個(gè)狀態(tài)時(shí)才會(huì)觸發(fā)。在RBC切換場景中，非周期性消息模型中可觀測消息主要包含：M155(版本消息)，M159(通信會(huì)晤建立信息)，M32(版本確認(rèn))，M24(消息確認(rèn))，CEM(有條件緊急停車消息)，SMA(MA縮短消息)，UEM(無條件緊急停車消息)。

為了簡化接口定義，本文使用M[R][E]表示1個(gè)二維消息數(shù)組，其中R表示RBC，E表示EVC，如RM155[R1][E1]!，表示車載EVC1向RBC1發(fā)送消息M155消息。

上述周期消息模型和非周期消息模型統(tǒng)稱為無線消息模型，描述了無線消息通過GSM-R無線信道進(jìn)行傳輸?shù)竭_(dá)接收端的過程。

③ RBC2的延遲可觀測接口

CTCS-3級列控系統(tǒng)中， RBC2與EVC(EVC1和EVC2)之間消息交互通過GSM-R網(wǎng)絡(luò)進(jìn)行，網(wǎng)絡(luò)中的延遲無法忽略。本文給出了RBC與EVC之間的消息延遲模型(Delay)，相關(guān)可觀測接口包括：in和out。其中In和Out是地址參數(shù)，不同的消息可以通過傳址方式進(jìn)行。例如圖9中RM155和M155，通過Delay的In和Out進(jìn)行延遲設(shè)計(jì)，分別將RM155和M155賦予In和Out變量中，并在一定時(shí)間內(nèi)輸出Out變量，達(dá)到了延遲發(fā)送消息M155的目的。

(2) 測試規(guī)范的非可觀測接口定義

由于該場景模型未涉及RBC之間的消息交互，測試規(guī)范中的非可觀測接口主要包括：RBC1與EVC1的接口，RBC1與EVC2的接口，CBI1與CBI2之間的接口以及RBC與QUEUE的接口。見圖10。

其中，Delay模型中的in和out分別代表CBI之間通信的rocc_req, occ_req，rocc_info,occ_info。 QUEUE主要包含add(增加列車信息)，pop(出棧列車信息)，Out(發(fā)送列車信息)。

3.3 跨界聯(lián)鎖信息傳遞的環(huán)境時(shí)間自動(dòng)機(jī)模型

利用UPPAAL工具支持模型復(fù)用的特點(diǎn)，建立跨界聯(lián)鎖信息傳遞的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。在模型建立和檢驗(yàn)工具UPPAAL的輔助下建立運(yùn)營場景下的列控系統(tǒng)TA網(wǎng)絡(luò)，其系統(tǒng)之間的并發(fā)行為由時(shí)間自動(dòng)機(jī)的積完成，其系統(tǒng)的行為由時(shí)間自動(dòng)機(jī)的跡描述[16]。模型中所有系統(tǒng)的時(shí)鐘均滿足(dot(t)=1，且可重置t:=0)，具體成員時(shí)間自動(dòng)機(jī)模型包括：CBI1‖EVC1‖ RBC1 ‖ CBI2‖EVC2‖RBC2‖Delay‖QUEUE，簡稱2CER-DQ模型。

(1) CBI自動(dòng)機(jī)

聯(lián)鎖、TCC、中繼抽象為聯(lián)鎖CBI(Computer Based Interlocking)模型見圖11，主要包含處理本RBC管轄區(qū)域軌道區(qū)段占用信息和相鄰RBC第1段占用區(qū)段的占用信息功能。

(2) EVC自動(dòng)機(jī)

EVC包含EVC1自動(dòng)機(jī)和EVC2自動(dòng)機(jī)見圖12，其主要功能包括處理本RBC管轄區(qū)域內(nèi)登陸RBC，登陸相鄰RBC，RBC交互信息(CEM，SMA和UEM)以及MA計(jì)算功能。

(3) RBC自動(dòng)機(jī)

RBC自動(dòng)機(jī)包含RBC1自動(dòng)機(jī)和RBC2自動(dòng)機(jī)見圖13，RBC的主要功能包括列車注冊功能處理，列車隊(duì)列管理功能，與EVC之間的消息交互功能以及MA計(jì)算功能。

(4) Delay自動(dòng)機(jī)

另外，對建模工具UPPAAL，TA網(wǎng)絡(luò)中進(jìn)程間的通道通信被認(rèn)為是瞬時(shí)的，即通道的同步變遷不消耗時(shí)間，因此在模型中添加描述時(shí)間、延遲的進(jìn)程，以對應(yīng)場景中通信網(wǎng)絡(luò)(包括跨界聯(lián)鎖和GSM-R無線網(wǎng)絡(luò))的傳輸延遲，見圖14。Delay自動(dòng)機(jī)主要負(fù)責(zé)環(huán)境與被測RBC2之間，CBI之間的消息傳輸功能。傳輸延遲由帶參數(shù)控制的Delay(chan &in, chan &out)自動(dòng)機(jī)，實(shí)現(xiàn)從[mindelay，maxdelay]中隨機(jī)選擇延遲的時(shí)刻點(diǎn)。該消息傳輸延遲是非確定性的，即傳輸延遲可以在最小延遲和最大延遲范圍之內(nèi)。

(5) QUEUE自動(dòng)機(jī)

圖15所示的QUEUE自動(dòng)機(jī)主要完成RBC(RBC1和RBC2)的列車管理功能，通過add,pop,out和empty消息進(jìn)行添加列車，后進(jìn)先出LIFO(Last In First Out)列車處理，列車隊(duì)列重置以及清除列車等功能。

首先EVC1和EVC2通過RM155[R1][E1](RM155[R1][E2])，RM159[R1][E1](RM159[R1][E2])，RM136[R1][E1](RM136[R1][E2])完成在RBC2的登錄功能，然后通過RM132[R1][E1](RM132[R1][E2])向RBC2發(fā)送MA請求信息，等待回復(fù)。

RBC(RBC2和RBC1)完成列車登陸功能后，激活隊(duì)列控制功能。LIFO表示后添加的列車先出棧，等待MA的請求信息。收到MA請求信息后，立即向相關(guān)的CBI(CBI2和CBI1)發(fā)送消息OCCHRBC_req(OCCTRBC_req)請求軌道區(qū)段占用信息。收到相關(guān)CBI發(fā)送的軌道占用信息OCCHRBC_info(OCCTRBC_info)后，激活MA計(jì)算功能，并根據(jù)列車的位置發(fā)送相關(guān)的信息，例如向RBC2向EVC1發(fā)送RM3[R2][E1](正常MA消息)，或者RCEM[R2][E1](有條件緊急停車消息)，RSMA[R2][E1](MA回撤消息)和RUEM[R2][E1](緊急停車消息)。

EVC(EVC1和EVC2)根據(jù)收到相關(guān)的RBC信息，發(fā)送對應(yīng)的消息確認(rèn)信息，例如收到RSMA[R1][E1]后，立即發(fā)送RConf_SMA[R1][E1]消息進(jìn)行回復(fù)。當(dāng)EVC控制列車的位置到達(dá)RBC之前的切換預(yù)告點(diǎn)，則激活與相鄰RBC的登陸功能，例如EVC1在RBC2控制區(qū)域內(nèi)，通過RM155[R2][E1]，RM159[R2][E1]和RM136[R2][E1]消息進(jìn)行RBC1登陸。

當(dāng)EVC1機(jī)車進(jìn)入RBC1控制區(qū)域后，CBI2通過rocc_req消息向CBI1請求RBC邊界的第1個(gè)軌道區(qū)段占用信息，并通過occ_info得到相關(guān)占用信息。此時(shí)，RBC2根據(jù)CBI2的軌道區(qū)段占用信息(包含CBI1提供的邊界外第1個(gè)軌道區(qū)段占用信息)，計(jì)算混合MA并發(fā)送給RBC2。

特別時(shí)，在RBC切換的過程中，如果RBC發(fā)送了MA回撤消息SMA[R1][E1](SMA[R1][E2])，需在[mindelay, maxdelay]時(shí)間范圍內(nèi)收到Conf_SMA[R1][E1](Conf_SMA[R1][E2])確認(rèn)信息，如果在此期間滿足發(fā)送CEM[R1][E1](CEM[R1][E2])的條件，則升級為UEM[R1][E1](UEM[R1][E2])消息。

值得說明的是，本文中RBC與EVC之間，CBI之間的信息傳輸均通過Delay自動(dòng)機(jī)進(jìn)行，即：任何消息傳輸均為非確定性。

3.4 RBC2被測系統(tǒng)設(shè)計(jì)

被測系統(tǒng)為RBC2設(shè)備，由Adapter和仿真功能組成，其中，

(1) Adapter設(shè)計(jì)：本文利用VC++定義了TRON模型與被測軟件之間可觀測的輸入/輸出通道，利用TRON中提供的Adapter API功能函數(shù)(getInputEncoding(·)和getOutputEncoding(·))識別環(huán)境模型與被測系統(tǒng)之間的輸入/輸出信息流。Adapter中輸入/輸出部分功能實(shí)現(xiàn)見圖16。

(2) 邏輯功能設(shè)計(jì)

RBC仿真軟件主要完成測試規(guī)范中規(guī)定的功能。其中接收CBI的占用信息(通過地面網(wǎng)絡(luò))由Occ_Process(·)函數(shù)完成；接收EVC的無線消息由EVC_Process(·)函數(shù)完成；向EVC發(fā)送移動(dòng)授權(quán)(MA)消息(通過無線網(wǎng)絡(luò))由MA_Send(·)函數(shù)完成；

(3) 延遲功能

通過提取真實(shí)設(shè)備RBC2中完成RBC切換運(yùn)營場景的真實(shí)接口信息，進(jìn)行時(shí)序上的分析，得到通信延遲(地面以太網(wǎng)和GRM-R無線網(wǎng)絡(luò))的具體實(shí)現(xiàn)參數(shù)。仿真中，假設(shè)CBI的占用信息由Delay_CBI( )函數(shù)處理(暫定為1～3 s)， 與EVC交互的信息由Delay_EVC(·)函數(shù)處理(暫定為隨機(jī)數(shù)1～3 s)。RBC2被測系統(tǒng)處理聯(lián)鎖占用信息的實(shí)現(xiàn)部分，見圖17。

4 結(jié)果分析

(1) 系統(tǒng)模型參數(shù)配置

該場景模型中涉及如下參數(shù)

① 線路參數(shù)：每段線路長度均為500 m，RBC邊界為s7和s8, 切換預(yù)告點(diǎn)為s5；

② EVC1：初始位置Pos[0]=0 m，占用區(qū)段s0；

③ EVC2：初始位置Pos[1]=3 000 m，占用區(qū)段s5；

④ Delay延遲設(shè)置：RBC與EVC之間mindelay=1 mtu,maxdelay=3 mtu; CBI之間mindelay=1 mtu,maxdelay=3 mtu。mtu表示模型時(shí)間單元(model time unit)；

⑤ RBC軟件參數(shù)設(shè)置：列車占用信息在RBC仿真軟件中由Delay_CBI(·)函數(shù)處理,即：RBC2處理CBI2的區(qū)段出清和占用信息，這里處理時(shí)間可忽略不計(jì)(為0)；RBC回復(fù)消息的延遲由Delay_EVC完成，表示RBC在收到EVC信息后，在[1,3]間回復(fù)確認(rèn)信息。

⑥ MA延伸策略：EVC1控制列車運(yùn)行2個(gè)空閑區(qū)段后(運(yùn)行1 000 m)，EVC2列車可延伸新的EOA；

⑦ 仿真步長設(shè)置：當(dāng)EVC1控制的列車運(yùn)行到5 100 m(s9)時(shí)，重置模型的狀態(tài)和變量。

值得說明的是：RBC軟件的執(zhí)行時(shí)間與模型的執(zhí)行時(shí)間對應(yīng)關(guān)系為：1 mtu=1 s。

(2) 仿真結(jié)果分析

在測試過程中，每次仿真測試規(guī)定最大時(shí)限2 000 mtu，觀察跨界聯(lián)鎖消息延遲和無線車-地消息延遲對輸出的影響。見圖18，測試結(jié)果均為passed，表明RBC仿真軟件的功能和時(shí)延均滿足系統(tǒng)規(guī)范要求。

然而，通過數(shù)據(jù)分析發(fā)現(xiàn)每次測試RBC2均存在不同概率發(fā)送UEM的現(xiàn)象。根據(jù)仿真設(shè)置，系統(tǒng)仿真1次需要200 s，在EVC1控制的列車運(yùn)行至5 100 m處，進(jìn)行重置，即：EVC2運(yùn)行到2 100 mtu處進(jìn)行重置(每隔21 s進(jìn)行重置)，見圖19。

圖19給出了系統(tǒng)某次仿真中前兩次重置的結(jié)果，分別在約21 s和42 s處，出現(xiàn)了EOA從4 km延伸到5 km后，又縮短至4 km的現(xiàn)象，表明發(fā)生了SMA。

從文件數(shù)據(jù)分析可知，由于RBC2與EVC2之間的非確定性時(shí)延，第一次發(fā)送SMA消息后，CEM條件滿足之前收到了SMA的確認(rèn)消息，然后發(fā)送CEM消息；第2次發(fā)送SMA消息后，CEM條件滿足之前未收到SMA的確認(rèn)消息，則消息升級為UEM消息，見圖20。

導(dǎo)致發(fā)送UEM的原因可能有多種，例如，邏輯功能方面，設(shè)備收到不符合邏輯的異常消息或空消息；實(shí)時(shí)性方面，實(shí)際聯(lián)鎖傳遞軌道占用信息的時(shí)延超出了規(guī)范中允許的時(shí)間限制，或車載設(shè)備與RBC之間無線通信網(wǎng)絡(luò)存在延遲導(dǎo)致輸出邏輯異常等。文中跨界聯(lián)鎖信息傳遞的環(huán)境時(shí)間自動(dòng)機(jī)模型中規(guī)定，當(dāng)RBC2發(fā)送SMA以后，需要在[1,3]時(shí)間范圍內(nèi)等待確認(rèn)確認(rèn)信息。由于CBI2與CBI1之間的非確定時(shí)延，如果在該時(shí)間范圍內(nèi)滿足CEM發(fā)送條件，則升級為UEM(該消息是系統(tǒng)不期望的)。

為了更好的分析原因，結(jié)合模型的測試過程，圖21給出了發(fā)送UEM消息順序圖。由圖21可知，RBC2先收到管轄范圍內(nèi)s7出清信息，后收到邊界區(qū)段s8占用信息(正常情況下應(yīng)該先收到s8占用，再收到s7出清)。這一原因是由于在RBC切換邊界，s8的占用信息通過CBI1傳輸給CBI2，再傳輸給RBC2的時(shí)延造成。通過分析，由于規(guī)范中設(shè)計(jì)的RBC2判斷CBI2區(qū)段出清為瞬時(shí)0 s(模型中用"U"狀態(tài)位置表達(dá)，仿真軟件中由Delay_CBI(·)函數(shù)處理),即RBC2收到CBI2的區(qū)段出清信息后，立刻計(jì)算MA，造成后續(xù)發(fā)送SMA的情況。因此，整個(gè)測試發(fā)送UEM的本質(zhì)是：由于RBC2收到CBI2占用信息的延遲于出清信息，RBC切換過程中發(fā)送了SMA消息。

根據(jù)模型參數(shù)設(shè)置，CBI1發(fā)送給CBI2交接處S8的狀態(tài)信息存在[1mtu,3mtu]時(shí)間延遲，造成RBC2發(fā)送SMA消息的現(xiàn)象。由于該延遲不可忽略，為了解決緊急制動(dòng)問題，選擇修改模型中RBC2判斷CBI2發(fā)送的出清區(qū)段信息處理時(shí)間，將RBC2處理CBI2發(fā)送的區(qū)段出清信息至少延遲3 mtu進(jìn)行處理(本模型選擇延遲3 mtu)，即在列車出清某區(qū)段后，延遲3 mtu再使用更新的區(qū)段占用信息，測試結(jié)見圖22。由圖22可見，通過修改需求規(guī)范模型中的RBC2處理占用出清信息的時(shí)延參數(shù)，RBC2未發(fā)送SMA消息，結(jié)果顯示UEM不再發(fā)生。

5 結(jié)束語

高速鐵路列控系統(tǒng)作為一個(gè)典型的分布式實(shí)時(shí)系統(tǒng)，其消息邏輯間的時(shí)間約束對于列車運(yùn)行安全和行車效率具有重要意義。本文提出一種適合于列控系統(tǒng)時(shí)間特性的在線測試方法，利用時(shí)間自動(dòng)機(jī)理論對RBC切換過程中跨界聯(lián)鎖消息的傳遞流程進(jìn)行建模，并重點(diǎn)描述軌道占用消息傳輸延遲的非確定性、車-地?zé)o線消息傳輸延遲的非確定性等時(shí)間特性。最終找出了仿真RBC測試模型與測試需求中不一致的地方，并通過改進(jìn)測試模型中RBC處理占用參數(shù)的設(shè)置，實(shí)現(xiàn)了RBC切換過程中跨界傳遞聯(lián)鎖消息時(shí)延非確定性的一致性測試。該方法可為我國下一代列控系統(tǒng)規(guī)范的制定和系統(tǒng)開發(fā)提供一定參考。

參考文獻(xiàn)：

[1] BROY M,JONSSON B,KATOEN J P,et al. Model-based Testing of Reactive Systems, Advanced Lectures Lecture Notes in Computer Science[M]. Berlin:Springer-Verlag, 2005.

[2] 吳道華. 基于著色Petri網(wǎng)的測試用例生成及其在列控系統(tǒng)中的應(yīng)用[D].北京:北京交通大學(xué)，2010．

[3] 張勇, 王超琦. CTCS-3級列控系統(tǒng)車載設(shè)備測試序列優(yōu)化生成方法[J].中國鐵道科學(xué),2011, 32(3): 100-106.

ZHANG Yong，WANG Chaoqi. The Method for the Optimal Generation of Test Sequence for CTCS-3 on-board Equipment[J]. China Raiiway Science, 2011, 32(3): 100-106.

[4] 徐中偉, 吳芳美. 形式化故障樹分析建模和軟件安全性測試[J].同濟(jì)大學(xué)學(xué)報(bào)(自然科學(xué)版), 2001, 29(11): 1299-1302.

XU Zhongwei, WU Fangmei. Formal Fault Tree Analysis Modeling and Software Safety Testing[J].Journal of Tongji University:Nature Edition,2001, 29(11): 1299-1302.

[5] BEIZER B. Black-box Testing: Techniques for Functional Testing of Software and Systems[J].Control Engineering Practice, 1996, 8(4): 1190-1191.

[6] 趙顯瓊，唐濤. 多端口形式化測試自動(dòng)生成方法在CTCS-3車載系統(tǒng)中的應(yīng)用[J].鐵道學(xué)報(bào),2011，33(7):44-51.

ZHAO Xianqiong,TANG Tao.Multi-port Based Automatic Formal Testing Generation and Its Application in CTCS-3 Level on-board System[J]. Journal of the China Railway Society, 2011,33(7):44-51.

[7] 袁磊，呂繼東，劉雨，等.一種全覆蓋的列控車載系統(tǒng)測試用例自動(dòng)生成算法研究[J]. 鐵道學(xué)報(bào),2014,36(8):55-62.

YUAN Lei,LV Jidong, LIU Yu, et al Research on Model-based Test Case Generation Method of onboard Subsystem in CTCS-3[J].Journal of the China Railway Society, 2014,36(8):55-62.

[8] 呂繼東，朱曉琳，李開成，等. 基于模型的CTCS-3級列控系統(tǒng)測試案例自動(dòng)生成方法研究[J]. 西南交通大學(xué)學(xué)報(bào)，2015,50(5): 917-927.

LV Jidong, ZHU Xiaolin, Li Kaicheng, et al. Model-Based Test Case Generation of CTCS-3 Train Control System[J]. Journal of Southwest Jiaotong University,2015,50(5):917-927.

[9] HESSEL A, LARSEN K G, MIKUCIONIS M, et al. Testing Real-time Systems Using UPPAAL Formal Methods and Testing[M]. Berlin Heidelberg: Springer, 2008: 77-117.

[10] KRICHEN M,TRIPAKIS S.Conformance Testing for Real-time Systems[J]. Formal Methods in System Design, 2009, 34(3): 238-304.

[11] MikUCIONIS M, SaSNAUSKAITE E. On-the-fly Testing Using UPPAAL[D].Denmark:Aalborg University. Department of Computer Science, 2003.

[12] LARSEN K G, MiKUCIONIS M, NiELSEN B,et al. Testing Real-time Embedded Software Using UPPAAL-TRON: an Industrial Case Study[C]//Proceedings of the 5th ACM International Conference on Embedded software. New York: ACM, 2005: 299-306.

[13] LARSEN K G, MIKUCIONIS M, NIELSEN B.Online Testing of Real-time Systems Using UPPAAL[M]. Berlin Heidelberg:Springer, 2005.

[14] 鐵道部科學(xué)技術(shù)司，鐵道部運(yùn)輸局.科技運(yùn)[2008]127號 CTCS-3 級列控系統(tǒng)需求規(guī)范(SRS)(V1.0)[S].北京：中國鐵道出版社，2008.

[15] 中華人民共和國國家質(zhì)量監(jiān)督檢驗(yàn)檢疫總局，中國國家標(biāo)準(zhǔn)化管理委員會(huì).GB/T24339.2—2009軌道交通 通信、信號和處理系統(tǒng) 第2部分：開放式傳輸系統(tǒng)中的安全機(jī)關(guān)通信[S].北京：中國標(biāo)準(zhǔn)出版社，2009.

[16] ALUR R, DILL D L. A Theory of Timed Automata[J]. Theoretical Computer Science, 1994, 126(2): 183-235.