基于UPPAAL-TRON的高速鐵路列控系統非確定性時延一致性測試研究

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

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

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

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

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

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

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

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

1 RBC切換邊界聯鎖信息不同步場景非確定性時延分析

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

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

TDelay_min=t0+t1+t2+t3

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

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

① 若RBC收到邊界內(MA范圍內)的進路占用狀態，應立刻向車載設備發送CEM(有條件緊急停車)消息，該消息無需車載設備應答；

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

③ 若RBC收到邊界后其他(非第1段)進路的占用狀態信息，則RBC立刻向列車發送SMA消息，并需在Tack時間內由車載設備響應該消息；

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

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

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

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

(2) 模型層：將系統層的輸入/輸出行為抽象成數學模型的過程。具體為實際環境抽象成環境模型，被測設備抽象成設備模型，環境模型和設備模型之間通過可觀測接口形成1個并發的系統模型。針對環境模型的每個輸入信息，其對應期望的輸出信息均在系統模型的行為中進行描述，并作為測試過程中的評判標準；

(3) 測試層：通過設計模型層和測試層之間的接口適配，將模型層中環境模型的每個輸入信息同時發給設備模型和真實設備；同理，真實設備也通過接口適配將輸出信息發送給環境模型。系統模型根據環境模型的輸入和真實設備的輸出，結合模型層中的評判標準，給出一致性測試的結論：通過或失敗。

UPPAAL-TRON (簡稱TRON)實現了上述測試理念，它從實際IUT及虛擬外界環境模型中產生和執行在線測試[13]。取代了圖4中的測試工具，測試規范由時間自動機模型工具UPPAAL完成，被測設備SUT和測試規范之間由TRON和適配器Adapter連接(具體應用過程后述)，其在線測試框架見圖5。

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

3 基于TRON的RBC切換場景一致性在線測試設計

3.1 環境和被測系統

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

(1) 測試環境

測試環境包含除RBC2設備相關的測試規范(由自動機模型表示)和測試工具UPPAAL-TRON工具，其中,

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

② 2UPPAAL-TRON：如前節介紹，該工具用來執行測試規范(自動機網絡模型，一般為XML文件)，接收環境時間自動機網絡模型與設備的時間自動機網絡模型之間輸入輸出信息流，并發送給實際被測設備，反之亦然。

(2) 被測系統

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

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

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

3.2 測試規范的接口定義

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

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

① RBC2與CBI2的可觀測接口

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

② RBC2與EVC的可觀測接口

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

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

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

上述周期消息模型和非周期消息模型統稱為無線消息模型，描述了無線消息通過GSM-R無線信道進行傳輸到達接收端的過程。

③ RBC2的延遲可觀測接口

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

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

由于該場景模型未涉及RBC之間的消息交互，測試規范中的非可觀測接口主要包括：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(發送列車信息)。

3.3 跨界聯鎖信息傳遞的環境時間自動機模型

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

(1) CBI自動機

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

(2) EVC自動機

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

(3) RBC自動機

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

(4) Delay自動機

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

(5) QUEUE自動機

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

首先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發送MA請求信息，等待回復。

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

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

當EVC1機車進入RBC1控制區域后，CBI2通過rocc_req消息向CBI1請求RBC邊界的第1個軌道區段占用信息，并通過occ_info得到相關占用信息。此時，RBC2根據CBI2的軌道區段占用信息(包含CBI1提供的邊界外第1個軌道區段占用信息)，計算混合MA并發送給RBC2。

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

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

3.4 RBC2被測系統設計

被測系統為RBC2設備，由Adapter和仿真功能組成，其中，

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

(2) 邏輯功能設計

RBC仿真軟件主要完成測試規范中規定的功能。其中接收CBI的占用信息(通過地面網絡)由Occ_Process(·)函數完成；接收EVC的無線消息由EVC_Process(·)函數完成；向EVC發送移動授權(MA)消息(通過無線網絡)由MA_Send(·)函數完成；

(3) 延遲功能

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

4 結果分析

(1) 系統模型參數配置

該場景模型中涉及如下參數

① 線路參數：每段線路長度均為500 m，RBC邊界為s7和s8, 切換預告點為s5；

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

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

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

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

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

⑦ 仿真步長設置：當EVC1控制的列車運行到5 100 m(s9)時，重置模型的狀態和變量。

值得說明的是：RBC軟件的執行時間與模型的執行時間對應關系為：1 mtu=1 s。

(2) 仿真結果分析

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

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

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

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

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

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

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

5 結束語

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

參考文獻：

[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網的測試用例生成及其在列控系統中的應用[D].北京:北京交通大學，2010．

[3] 張勇, 王超琦. CTCS-3級列控系統車載設備測試序列優化生成方法[J].中國鐵道科學,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].同濟大學學報(自然科學版), 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] 趙顯瓊，唐濤. 多端口形式化測試自動生成方法在CTCS-3車載系統中的應用[J].鐵道學報,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] 袁磊，呂繼東，劉雨，等.一種全覆蓋的列控車載系統測試用例自動生成算法研究[J]. 鐵道學報,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級列控系統測試案例自動生成方法研究[J]. 西南交通大學學報，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] 鐵道部科學技術司，鐵道部運輸局.科技運[2008]127號 CTCS-3 級列控系統需求規范(SRS)(V1.0)[S].北京：中國鐵道出版社，2008.

[15] 中華人民共和國國家質量監督檢驗檢疫總局，中國國家標準化管理委員會.GB/T24339.2—2009軌道交通 通信、信號和處理系統 第2部分：開放式傳輸系統中的安全機關通信[S].北京：中國標準出版社，2009.

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