基于模型的CTCS-3 級列控系統測試案例自動生成方法

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

(1. 北京交通大學軌道交通運行控制系統國家工程研究中心，北京100044;2. 中國鐵道科學研究院通信信號研究所，北京100044;3. 北京交通大學軌道交通控制與安全國家重點實驗室，北京100044)

作為典型的安全苛求系統，列控系統功能的任何故障都可能造成巨大的生命和財產損失［1］. 形式化方法和測試方法是保證列控系統功能正確性的兩個重要途徑，在列控系統開發生命周期中起著不同的作用.

形式化方法一般用于列控系統開發的前期，已廣泛用于列控系統需求規范的功能正確性研究［2］.早期列控系統的形式化研究主要使用時段演算方法(duration calculus，DC)［3］. 然而，時段演算不能完全滿足列控系統的形式化建模要求，隨著列控系統復雜度的提高，系統中諸如期限(deadline)、直到…才(wait until)、超時(time out)等形式化描述存在一 定 的 不足［4］. 進程代 數(process algebra)通過描述并發和通信系統為分析離散事件系統提供了結構化方法［5］，其中，HCSP(hybrid communication sequential process)方法是對CSP(communication sequential process)的一種擴展，廣泛應用于列控系統功能正確性研究［6］. 一致性測試是保證系統功能正確性的另一個重要手段，一般用于列控系統開發的后期.通過分析被測系統(system under test，SUT)與其需求規范之間的關系，驗證系統的功能是否與需求規范一致［7］. 國內外列控系統功能一致性測試的研究主要集中在測試案例生成方法上［8-10］.

CTCS-3 級列控系統功能復雜，涵蓋了注冊與啟動、注銷、等級轉換、行車許可、RBC(radio block center)切換、自動過分相、重聯與摘解、臨時限速、降級情況、調車作業和特殊進路等14 個典型的運營場景.運營場景之間具有順序和并發等特點(例如，行車許可場景和注冊與啟動場景之間是順序關系，但與RBC 切換場景是并發關系).運營場景需求規范中包含了若干個并發執行和交互的實時計算構件，規定了車載設備和RBC 設備接口信息時序約束［11］.上述研究主要集中在列控系統單個運營場景時序約束行為的正確性上，對整個列控系統層次的建模描述鮮有研究;并且不同運營場景存在不同的時序約束(例如超時(TimeOut)、期限(deadline)、直到…才(wait until)等等)，針對這些時序約束的建模與驗證也存在不足.形式化方法應既能在列控系統層次上描述不同運營場景之間的關系，又能在運營場景層次上描述接口信息交互行為的時序約束，因此，結合運營場景需求規范的特征和特點選擇合適的形式化方法是研究的難點.

另一方面，列控系統具有實時性、混雜性等特點，系統功能的正確性不僅要求邏輯功能的正確性，而且要求在規定的時間約束內做出正確的邏輯響應.不同的運營場景、不同的測試目的和不同的時間約束都對應不同的測試案例，功能測試面臨著狀態空間爆炸和時間特性測試的問題. 例如，在列控系統運營場景中，RBC 根據接收到車載設備發送消息的時間，結合運營場景中的時間約束要求，在規定的時間內必須輸出對應的邏輯功能(正常的移動授權或緊急制動).針對運營場景接口信息交互的時序特點，選擇恰當的測試目的，進行高效的測試案例自動生成，并形成涵蓋列控系統所有運營場景的測試套，是研究的另一個難點.

本文基于HCSP 和TA(timed automata)理論［12］，提出了一種基于模型的列控系統測試案例生成方法.首先，結合列控系統運營場景之間的執行特點，利用HCSP 的順序和并發操作進行了列控系統功能的形式化建模;其次，利用HCSP 支持中斷機制(通訊中斷、時間中斷等)的特點，針對相關運營場景內部組件交互的時序約束(例如延遲、超時、中斷等)進行了形式化建模，并通過引入轉換規則，將HCSP 的一個子集轉換成TA 網絡模型，從而進行相關屬性的驗證;再次，基于時間自動機網絡模型，給出了列控系統在單一運營場景執行下不同覆蓋準則下(全狀態、全變遷和自定義-使用)的測試案例生成算法，以及涵蓋所有列控系統運營場景的測試案例套優化算法，并在此基礎上，結合模型檢驗工具Uppaal 和CoVer，提出了一條適合于列控系統測試案例自動生成的工具鏈;最后，結合典型的CTCS-3 級列控系統RBC 切換運營場景，建立場景的HCSP 模型，驗證了場景中時序約束的屬性.結合不同的測試覆蓋準則，生成了相關的測試案例套，并進行了比較分析.

1 列控系統運營場景的建模與驗證方法

HCSP［13-14］是一種以CSP 為基礎，引入描述混成系統中連續動態行為的微分方程，以及各種中斷機制(通信中斷、時間中斷、事件中斷等)，以期實現對外部事件引發進程遷移行為進行描述的形式化建模語言.

1.1 列控系統功能的HCSP 模型

根據CTCS-3 級列控系統總體技術方案［11］，定義一列列車從“注冊與啟動”到“注銷”的某種運營過程，如圖1 所示.

假設以上整個系統層的每個運營場景都由一個HCSP 的原子公式來描述，注冊與啟動場景:PS0;級間轉換場景:PS1;行車許可場景:PS2;臨時限速場景:PS3;自動過分相場景:PS4;RBC 切換場景:PS5;降級場景:PS6;注銷場景:PS7.

利用HCSP 的順序操作和并發操作算子，定義整個列控系統功能的HCSP 模型為

SYS?PS0;PS1;PS2(PS3;PS4;PS5);PS6;PS7.

圖1 列控系統運營場景過程Fig.1 Operation scenario process of the train control system

1.2 基于HCSP 子集的運營場景建模方法

主要研究集中在列控系統運營場景內部組件交互的時序約束行為描述上，結合列控系統運營場景的描述特點，提出了6 種更適合于列控系統場景描述的時序模型:周期性、延遲、時間等待、超時、截止期限和時間中斷，并給出了適合于列控系統場景時序描述的一個HCSP 子集HCSPsub(僅考慮時間t是唯一的連續變量)，如表1 所示. 假設P 和Q 為兩個進程，其HCSPsub進程的定義見表1.

表1 HCSPsub的進程定義Tab.1 Process definition of HCSPsub

1.3 基于TA 的驗證方法

規則1 Stop

Stop 指系統永遠不會終止的idle 進程，記作Astop，Astop=({i}，i，φ，φ，φ，{(i，true)}，φ).

規則2 Skip

Skip 指系統立即終止的進程，記作Askip，Askip=({i，f}，i，{f}，{τ}，φ，{i，urgent)，(f，true)}，{(i，τ，φ，true，f)}).

規則3 事件前綴

如圖2 所示，事件前綴是指事件a 發生在時間自動機A 的任何變遷之前，記作eventprefix(a，A).

圖2 事件前綴Fig.2 Event prefix

規則4 尾遞歸

如圖3 所示，尾遞歸指系統永遠不會終止的進程，記作recur(A，S0).

(SS0，init，FS0，Σ，C，Inv，T')，

其中:

圖3 尾遞歸Fig.3 Tail recursion

規則5 延遲

如圖4 所示，延遲主要用于描述系統執行某一段延遲時間單元的進程，記作delay(t)，

其中:

圖4 延遲Fig.4 Delay

規則6 期限

如圖5 所示，期限指系統執行完成進程必須在一定時間單元內，記作deadline(A，t)，

圖5 期限Fig.5 Deadline

規則7 時間等待

如圖6 所示，時間等待(WaitUntil)表示系統在等待某段時間后終止的進程，記作waitunitl(A，t)，

圖6 時間等待Fig.6 Wait until

規則8 外部選擇

如圖7 所示，外部選擇表示系統根據外部的事件進行動作變遷選擇的進程，記作extchoice(A1，A2)，

圖7 外部選擇Fig.7 External choice

規則9 順序組合

如圖8 所示，順序組合表示系統執行任務先后順序的進程，記作seq(A1，A2)，

圖8 順序組合Fig.8 Sequential composition

規則10 超時

如圖9 所示，超時描述系統通過時間段切換控制權的進程，記作timeout(A1，A2，t)，

圖9 超時Fig.9 Time out

規則11 時間中斷

圖10 所示，時間中斷描述系統通過時間點中斷切換控制權的進程，記作timeinter(A1，A2，t)，

圖10 時間中斷Fig.10 Time interrupt

規則12 事件中斷

如圖11 所示，時間中斷描述系統通過事件中斷切換控制權的進程，記作evtinter(A1，A2，a)，

圖11 事件中斷Fig.11 Event interrupt

更多定義詳見文獻［13］.假設P 為HCSPsub的進程，A 為一個時間自動機，定義轉換函數Φ:P→A為HCSPsub到時間自動機A 的映射，從而有以下轉換規則:

基于上述轉換規則，可以利用典型的模型檢驗工具Uppaal［15］進行TA 模型相關屬性的自動驗證分析，相關研究可參考文獻［13］.

2 基于TA 模型的測試案例生成方法

在模型轉換規則的基礎上，利用典型的模型檢驗工具(Uppaal 和CoVer［16］)，給出了一條適合于列控系統測試案例自動生成的工具鏈. 如圖12 所示，整個測試方法包括4 個步驟.

圖12 基于模型的測試案例生成方法Fig.12 Model-based test case generation method

第1 步 規范分析階段

通過分析列控系統運營場景規范，提取列控系統建模對象和驗證屬性. 例如，CTCS-3 級列控系統“行車許可”運營場景(PS2)中規定:

(1)RBC 能夠發送移動授權信息給車載;

(2)車載能夠發送給RBC 位置報告信息;

(3)車載如果在［0，T］內接收不到移動授權信息則實施緊急制動操作，其中，T 是一個大于0的常數.

第2 步 模型抽象階段

通過對列控系統規范的分析，基于HCSPsub和TA 理論，抽象出列控系統場景規范的形式化模型.

(1)通過定義列控系統運營場景中相關對象的進程，建立列控系統運營場景的時序模型. 上述“行車許可”運營場景(PS2)的時序模型定義如下:

式中:Prbc和Pevc分別為“行車許可”運營場景中的RBC 和車載的進程;PEB為緊急制動進程(這里用stop 表示);MA 和pos 分別為移動授權信息和位置報告信息.

(2)結合1.3 節的轉換規則，將列控系統的HCSPsub模型轉換成TA 網絡模型.上述行車許可場景的HCSPsub模型可轉換成如下自動機網絡模型:

Φ(PrbcPevc)=para(Φ(Prbc)，Φ(Pevc)).

由規則3、4 和9，得到RBC 的TA 模型，如圖13 所示.

圖13 RBC 模型Fig.13 RBC model

由規則3、4、9 和12，得到EVC 的TA 模型，如圖14 所示.

結合TA 理論，RBC 和EVC 自動機時序模型的行為可以描述成:

圖14 EVC 模型Fig.14 European vital computer (EVC)model

第3 步 模型建立階段

利用UPPAAL 和CoVer 兩個TA 模型檢驗工具，進行測試案例自動生成研究.

(1)利用建模工具Uppaal 建立TA 網絡模型，并驗證相關屬性(安全相關屬性和時間相關屬性).結合上述的“行車許可”運營場景TA 模型，定義該自動機網絡Uppaal 模型為R-E:

RBC EVC.

R-E 的UPPAAL 模型如下圖15 所示.

圖15 R-E 模型Fig.15 R-E model

(2)利用測試案例生成工具CoVer，結合不同測試準則，進行測試套的自動生成.

典型的測試案例tc(test case)可以表示成一個三元組＜input，step，output ＞，即測試輸入、執行步驟和期望輸出. 測試序列ts(test sequence)則為運行測試案例過程中執行的行為序列.假設被測設備為EVC，上述例子中，測試執行序列ts 可以通過時間自動機時序模型run(rbc)變遷上的輸入或輸出序列:

該測試序列ts 表示RBC 執行了3 條相同的測試案例tc:＜MA，NULL，pos ＞. RBC 首先執行第1條測試案例tc，向被測設備EVC 接口輸入消息MA，等待期望輸出消息pos，一旦收到pos，繼續執行第2 條測試案例tc，直到所有測試案例執行完為止.

CoVer 利用觀測器原理［16］，提供了3 種領域功能無關的覆蓋準則(全狀態、全變遷或者自定義-使用)，如圖16(a)～(c)所示. 根據不同的測試目的，針對運營場景的自動機時序模型，給出全狀態、全變遷和自定義-使用3 種測試案例自動生成算法.

圖16 測試案例覆蓋準則Fig.16 Test case coverage criteria

圖16(a)定義了全狀態覆蓋準則，其包含被測進程TA 模型中所有狀態的覆蓋準則.

圖16(b)定義了全變遷覆蓋準則，其包含被測進程TA 模型中所有變遷的覆蓋準則.

圖16(c)定義了自定義-使用全覆蓋準則，其包含被測進程TA 模型中所有自定義變量的覆蓋準則.

結合本節實例，僅給出滿足被測設備EVC 自動機全狀態和全變遷覆蓋準則下的測試序列(自定義-使用覆蓋準則在第3 節介紹).

(1)全狀態覆蓋測試序列

根據R-E 自動機時序行為模型run(rbc evc)，構造1 條測試序列，使之在執行測試序列的過程中，被測EVC 的行為run(evc)能夠經過所有EVC的狀態.可直觀地定義:

(2)全變遷覆蓋測試序列

同理，構造1 條測試序列，使之經過所有EVC的變遷，可直觀地定義:

式中:d1＜T，d2≥T，d3≥0.

第4 步 列控系統測試案例自動生成階段

由于列控系統不同的運營場景具有不同的時序模型，通過簡單疊加各個運營場景測試案例的方式，能夠得到整個系統的測試案例套，然而這會造成大量重復的測試案例.為了得到在某種測試準則條件下，100%覆蓋整個列控系統運營場景時序模型的測試案例集，設計了如下優化算法:

算法描述如下:

對于任何一個給定的運營場景時序模型M0和S0，定義i=0，并給定一個測試準則?.

(1)進入循環，針對初始的運營場景時序模型，進行測試案例自動生成操作Total_TestCase，并將結果存儲在ts 中;

(2)判斷測試案例套Sts中是否含有ts.如果含有，則執行i=i+1，并且跳轉至循環;

(3)如果不含有ts，存儲ts 到Sts中;

(4)執行change_initial(Mi，Si)操作，得到下一個運營場景時序模型，執行i=i+1;

(5)循環執行步驟(1)，直到i=N 為止.

3 案例分析

3.1 RBC 切換場景

RBC 切換是指RBC 間在指定區域(切換應答器)實現對列車無縫切換［11］，如圖17 所示.

根據CTCS-3 級列控系統總體技術方案內容，以兩部電臺的RBC 切換過程為例，HRBC 表示移交RBC，TRBC 表示接管RBC，整個切換流程如圖18 所示.

圖17 RBC 切換場景原理Fig.17 Principle of RBC transition scenario

圖18 RBC 切換場景流程Fig.18 Process of RBC handover scenario

3.2 RBC 切換的HCSP 模型

(1)Timer 進程

Timer 進程通過通道circle 來控制HRBC、TRBC 與EVC 進程之間消息的交互.

(2)Speed 進程

Speed 進程由speed0 進程、speed1 進程、speed2進程和speed3 進程組成，通過通道acc 和Dec 模擬列車的加速和減速過程，其HCSP 模型如下:

(3)Queue 進程

Queue 進程是一個由add 進程和shift 進程組成的尾遞歸進程，主要完成HRBC 和TRBC 對EVC的管理功能.對應的HCSP 模型如下:

(4)HRBC 進程

HRBC 進程描述的HRBC 與EVC 之間的周期性信息交互過程，由建立鏈接start、建立通信會晤buildconnect、控制control、MA 計算computeMA、切換預通告pre、進路信息請求req、混合MA 計算comPmixMA、注銷logout 和刪除列車delete 共9 個進程組成.對應的HCSP 模型如下:

(5)EVC 進程

EVC 進程描述EVC 與HRBC 和TRBC 之間的周期性信息交互過程，由建立鏈接start、建立通信會晤buildconnect、發送位置報告reportPos、MA 請求MAreq、速度控制ControlSpeed、切換handover、建立鏈接start1、建立通信會晤buildconnect1、注銷logout 和鏈接失敗disconnect 等10 個進程組成.對應的HCSP 模型如下:

(6)TRBC 進程

TRBC 進程描述TRBC 與HRBC 和EVC 之間的周期性信息交互過程，由切換預通告pre、進路信息Routeinfo、建立鏈接 start、建立通信會晤buildconnect、控制control、MA 計算compMA、切換handover 等7 個進程組成.對應的HCSP 模型如下:

通過1.3 節的轉換規則，將RBC 的切換HCSP模型轉換成TA 網絡模型，定義為TSQ-HET:

其中各個進程的轉換關系如下:

如圖19 所示，利用Uppaal 工具對TSQ-HET進行了仿真和驗證.模型中，“!”和“?”表示自動機網絡模型間信息交互的發生.

3.3 自動測試案例生成

在TSQ-HET 模型的基礎上，以TSQ-HET 模型中的EVC 為被測對象(SUT)，針對3 種不同的測試案例覆蓋準則(全狀態、全變遷和MA(消息M3)相關的測試案例)進行了自動測試案例的生成.圖20 描述了M3 相關的測試案例生成算法，依據該算法可以通過模型自動生成M3 相關的測試案例套.

如圖21 所示，整個M3 相關的測試案例套包含3 部分:路徑trace(trace #1)、測試案例覆蓋項test case item 以及轉移條件transitions.

本文給出以下3 個指標來衡量測試案例自動生成的有效性.

(1)測試套:滿足相關覆蓋準則的測試案例數量，以及測試案例覆蓋的事件執行(EdgeN)數量.測試套的數量越大，表明測試越充分，反之亦然;

圖19 TSQ-HET 時間網絡自動機Fig.19 Network of TSQ-HET timed automata

圖20 M3 相關的測試案例生成準則Fig.20 Test case generation criterion about M3

(2)測試時間:滿足相關覆蓋準則條件下，測試案例自動生成的時間. 時間越短，表明測試案例生成效率越高，反之亦然;

(3)內存消耗:滿足相關覆蓋準則條件下，CoVer 軟件消耗的內存大小. 內存消耗越小，表明測試案例生成效率越高，反之亦然.不同測試準則下的測試套比較見表2.

圖21 EVC 的測試套Fig.21 Test suites of EVC

表2 從測試套(案例數量、測試案例覆蓋項)、測試時間和內存消耗3 個方面，對3 種不同的測試案例覆蓋準則(全狀態、全變遷和MA(消息M3)相關的測試案例)進行了對比分析. 結論表明，全狀態覆蓋的測試套執行時間和內存消耗均大于全變遷和自定義-使用，自定義-使用的測試時間和內存消耗最小，能夠有效的提高測試的效率.

表2 不同測試準則下的測試套比較Tab.2 Comparison of test suites under different criteria

4 結束語

本文基于HCSP 和TA 理論，提出了一種基于模型的列控系統測試案例生成方法.針對HCSP 的一個子集，提出了HCSP 的子集模型轉換成TA 網絡模型的轉換規則，實現了列控系統HCSP 安全屬性和時間相關屬性的自動驗證. 基于TA 網絡模型，提出了全狀態、全變遷和自定義-使用3 種覆蓋準則下的測試案例自動生成算法，優化了列控系統測試案例套的自動生成. 在此基礎上，給出了一個基于Uppaal＆CoVer 模型檢驗工具鏈，實現了列控系統測試案例自動生成. 最后，結合實際CTCS-3級列控系統RBC 切換場景進行了案例分析，生成了不同覆蓋準則的測試套，并進行了比較分析，測試結果表明了方法的有效性.

［1］ 呂繼東. 列車運行控制系統分層形式化建模與驗證分析［D］. 北京:北京交通大學，2011.

［2］ 古天龍. 軟件開發的形式化方法［M］. 北京:高等教育出版社，2005:6-8.

［3］ CHAOCHEN Z，HANSEN M. Duration calculus a formal approach to real-time systems［M］. ［S. l.］:Springer-Verlag，2003:14-16.

［4］ DONG Jinsong，HAO Ping，QIN Shengchao，et al.Timed automata patterns［J］. IEEE Transactions on Software Engineering，34，2008:844-845.

［5］ HOARE C A R. Communicating sequential processes［J］.Communications of the ACM，1978，21(8):666-677.

［6］ LIU Jiang，Lü Jidong，ZHAO Quan. Programming languages and systems:a calculus for hybrid CSP［M］.Berlin:Springer，2010:1-15.

［7］ BEIZER B. Black-box testing，techniques for functional testing of software and systems［M］. New York:Wiley，1995:39-41.

［8］ 張勇，王超琦. 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 Railway Science，2011，32(3):100-106.

［9］ 徐中偉，吳芳美. 形式化故障樹分析建模和軟件安全性測試［J］. 同濟大學學報:自然科學版，2001，29(11):1299-1302.XU Zhongwei，WU Fangmei. Formal fault tree analysis modeling and software safety testing［J］. Journal of Tongji University:Natural Science，2001，29(11):1299-1302.

［10］ 趙顯瓊，唐濤. 多端口形式化測試自動生成方法在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.

［11］ 張曙光. CTCS-3 級列控系統總體技術方案［M］. 北京.中國鐵道出版社，2008:49-50.

［12］ ALUR R，DILL D L. A theory of timed automata［J］.Theoretical Computer Science，1994，126:183-235.

［13］ 呂繼東，唐濤. 高速鐵路列控系統運營場景實時性建模與驗證［J］. 鐵道學報，2011，33(6):54-61.Lü Jidong，TANG Tao. Modeling and verification of time constraints of operation scenarios of high-speed train control system［J］. Journal of the China Railway Society，2011，33(6):54-61.

［14］ ZHOU Chaochen，WANG Ji，ANDERS P. Ravn a formal description of hybrid systems［C］∥Proc. of the DIMACS/SYCON Workshop on Hybrid Systems III:Verification and Control. New York:Springer-Verlag，1996:511-530.

［15］ BEHRMANN G，LARSEN K G，MOLLER O，et al.UPPAAL-present and future［C］∥Proc. of the 40th IEEE Conference on Decision and Control. Orlando:［s. n.］，2001:2881-2886.

［16］ HESSEL A，PETTERSSON P. CoVer:a real-time test case generation tool［C］∥19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software. Berlin:Springer，2007:73-77.