高鐵信號系統安全關鍵功能測試建模方法

李 耀 ，張曉霞 ，郭 進 ，張亞東

（1.電子科技大學光電科學與工程學院, 四川 成都 611731；2.西南交通大學信息科學與技術學院, 四川 成都611756）

我國高鐵運營里程已經超過2.9萬公里，占世界高鐵運營里程的2/3以上，累計運輸旅客超過100億人次.我國已成為世界上高鐵運營里程最長、運輸密度最高、運營場景最復雜的國家.高鐵信號系統具有SIL4級的安全需求，安全關鍵功能一旦失效可能造成列車追尾、脫軌等行車事故，導致人員傷亡及重大財產損失[1].保證高鐵信號系統安全關鍵功能的安全性對我國高鐵的安全運營、國家“高鐵走出去”具有重要意義.

基于模型的測試是目前高鐵信號系統安全關鍵功能安全性測試的研究熱點，常用的測試建模方法包括時間自動機（timed automata，TA）、UML Statechart和 Petri網（Petri net）等，研究內容重點關注如何從安全關鍵功能的測試模型生成覆蓋全面且高效的測試用例.文獻[2]針對 ATP （automatic train protection）系統模式轉換功能測試用例難以實現全覆蓋的問題，采用TA建模方法建立測試模型，提出滿足全狀態和全變遷覆蓋準則的測試用例生成方法，提高測試用例的生成效率和重用性.文獻[3]以RBC （radio block center）切換功能為例，提出基于 TA和 HCSP （hybrid communication sequential process）的測試建模方法，研究全狀態和全變遷覆蓋的測試用例自動生成方法，列控系統測試用例的生成效率提高30%.文獻[4]以TA作為測試建模的基礎理論，通過在測試模型中注入故障的方式提高測試用例的全面性.文獻[5]基于TA建模理論，提出輸入輸出時間自動機（timed automata with input and output,TAIO）建模方法，提出基于TAIO變異分析的列控系統安全關鍵功能測試框架.文獻[6]以有色Petri網（colored Petri net，CPN）作為測試建模的理論基礎，通過狀態空間搜索自動生成車地通信功能的測試用例，提高測試用例生成的自動化程度.文獻[7]針對ATP系統模式轉換功能，建立CPN測試模型，解決狀態空間爆炸和搜索死循環的問題，生成滿足全路徑覆蓋準則的測試序列集.文獻[8]針對列控中心軌道電路編碼功能，研究UML Statechart測試建模方法，提出圖覆蓋、組合覆蓋和文法分析相結合的方式自動生成測試用例.文獻[9]針對列控中心改變運動方向功能，建立UML Statechart測試模型，研究基于UML Statechart模型自動生成覆蓋全面的測試用例的算法，為自動化測試提供基礎.

目前的研究豐富了高鐵信號系統的測試用例，提高了測試活動的自動化程度和測試效率，但對高鐵信號系統安全關鍵功能測試建模理論的研究相對較少.目前主要采用的測試建模方法沒有很好地針對高鐵信號系統功能邏輯和時鐘約束的特點，導致測試模型復雜，測試用例缺少時鐘約束.首先，詳細分析高鐵信號系統測試模型的建模需求；然后，在有限狀態機理論的基礎上從功能邏輯和時鐘約束2個方面提出時間狀態機建模方法；最后，以計算機聯鎖道岔子系統為例進行了分析，為基于模型的高鐵信號系統測試提供新的建模理論.

1 問題描述

1.1 高鐵信號系統測試用例生成方法概述

基于模型的測試（model-based testing，MBT）[10]理論是高鐵信號系統安全關鍵功能測試用例生成的研究重點內容之一.MBT屬于基于規范的測試范疇，其編制測試用例和評判測試結果時均以被測系統（system under test，SUT）的測試模型作為依據.MBT已經在高鐵信號系統RBC、ATP和CBI （computer based interlocking）等設備的安全關鍵功能測試中得到重點研究[11-14].實踐表明，該方法能夠有效地發現系統問題，提高測試效率和自動化程度.

基于模型的測試主要包括分析被測系統需求、建立測試模型、生成抽象測試用例、具體化抽象測試用例、執行測試和分析測試結果6個階段.首先，基于被測系統的需求規格等文件對系統功能和結構進行抽象，建立系統的測試模型；其次，依據測試模型，選取測試覆蓋準則自動生成抽象測試用例；然后，結合行業知識將抽象測試用例實例化為可執行的測試用例；最后，將測試用例加載到測試環境中執行測試，觀察、分析測試結果.

1.2 高鐵信號系統測試建模的問題

測試模型是高鐵信號系統測試用例編制的基礎.目前，高鐵信號系統的測試建模方法不是針對信號系統安全關鍵功能測試的領域建模方法，不能很好、完整地描述高鐵信號系統的行為特征.模典型的高鐵信號系統測試建方法包括有限狀態機（finite state machine, FSM）、UML Statechart、TA 和 Petri網等，其中，FSM、UML Statechart和 Petri網等方法不具有描述時鐘約束的能力，導致該模型生成的測試用例不能反映系統的時間特性，不能滿足測試活動的全面性和完備性要求.TA能夠描述系統的時鐘約束，但不具有層次結構，對復雜功能邏輯的描述能力較差，不易描述高鐵信號系統安全關鍵功能的全部行為，容易出現狀態數量爆炸、測試模型難以理解、甚至錯誤的問題.

在安全關鍵系統形式化建模和分析領域，研究學 者 提 出 了 timed color Petri nets[15]、 Safecharts[16]、SyncCharts[17]、 RTSC[18]、 UML RT-Statechart[19]和TSSM[20]等建模方法，解決了安全關鍵功能復雜邏輯和時鐘約束的形式化描述和驗證問題.但針對高鐵信號系統測試，這些建模方法的語法、語義復雜，測試模型解析和測試用例生成難度較大，不易直接應用在高鐵信號系統的測試活動中.因此，研究適合于高鐵信號系統測試領域的形式化建模方法對高鐵信號系統安全關鍵功能的測試具有一定的意義.

2 高鐵信號系統測試建模需求

測試模型作為高鐵信號系統測試理論的重要基礎，需要盡可能全面、清晰地呈現被測系統的行為特性.本節針對高鐵信號系統的特點，分析高鐵信號系統測試活動的測試建模需求.

根據高鐵信號系統測試活動的過程和目標，高鐵信號系統測試建模包括功能建模需求和性能建模需求兩個方面.功能建模需求描述系統的功能邏輯（function logic），明確系統需要滿足的安全條件；性能建模需求指與系統功能相關的時鐘約束或限制（clock constraint）.

1）功能邏輯

隨著計算機和通信技術的發展，高鐵信號系統承擔的安全功能越來越多，功能邏輯越來越復雜.如CTCS-3級列控系統包括9種工作模式，14個主要運營場景，206個功能特征[21].高鐵信號系統已構成一個復雜的控制系統，存在著大量的并發、競爭和沖突等邏輯關系，控制狀態轉移條件復雜.高鐵信號系統測試模型需要滿足功能邏輯的復雜性和并發性，嚴密、準確地反應系統的功能需求，且具有良好的可讀性和可理解性.

2）時鐘約束

高鐵信號系統安全關鍵功能運算結果的安全性和正確性不僅取決于系統邏輯的處理過程，還取決于運算過程中的時鐘約束，屬于典型的實時系統（real-time system）.高鐵信號系統的時鐘約束主要指系統功能需要在指定的時間內完成，或在規定的時限之后才能發生.如《CTCS-3級列控系統測試案例（V3.0）》[21]功能特征190的測試用例3要求“司機未在5秒內進行確認，實施最大常用制動”.而且，安全關鍵功能的時鐘約束通常為硬實時性要求，如道岔轉換時間、RBC交互時間、MA （movement authority）有效時間等[22]，時鐘約束錯誤或缺失，可能造成重大安全事故.

根據以上分析，高鐵信號系統安全關鍵功能的測試建模方法需要能夠很好地描述系統復雜的功能邏輯和時鐘約束.

3 時間狀態機測試建模方法

有限狀態機（finite state machine, FSM）是 MBT理論中經典的測試建模方法[23-24]，其通過可視化的方式描述系統的功能邏輯，具有清晰、直觀的優點.本節在FSM的基礎上擴展出時間狀態機建模方法，首先介紹FSM的定義，然后在FSM的遷移中擴展出時鐘約束，結合Z規格說明語言給出時間狀態機的定義.

3.1 有限狀態機概述

FSM是表示有限狀態以及狀態之間轉移和動作等行為的數學模型，具有精確性、可推導性和可驗證性.

定義1（有限狀態機）一個有限狀態機M是個六元組，如式（1）[24].

式中：S為有限狀態集合；s0為初始狀態，s0∈S；λ為狀態轉移函數， λ :SI→S；δ為輸出函數， δ:SI→O；I為有限輸入符號集合；O為有限輸出符號集合.

圖1為一個開關的FSM模型.

圖1 有限狀態機示例Fig.1 Example of finite state machine

圖1 中包括關（soff）和開（son）兩個狀態，其中soff為初始狀態.soff接收到輸入A時轉移到son狀態，輸出A′，son接收到輸入B時轉移到soff狀態，輸出B′.模型對應的六元組如式（2）.

根據FSM的定義，FSM缺少描述時鐘約束的機制.接下來結合Z規格說明語言，在FSM描述功能邏輯的基礎上，增加層次結構，擴展出時鐘約束，提出時間狀態機（timed finite state machine，TFSM）.

3.2 TFSM基本元素

TFSM包括時鐘、信號和狀態等基本元素.

1）時鐘

TFSM采用時鐘描述時間的流逝，有限時鐘集合記為C，Z語言描述如下：

TFSM時鐘約束集合記為Ψ，Z語言描述如下：

對一個時鐘變量集合C，Ψ具有如下形式：

式 中 ： ψ1、 ψ2為 時 鐘 約 束 ；x∈C；d∈N ； ∝∈{≤,＜,≥,＞,=}.

2）信號

信號具有產生和不產生兩種狀態，Z語言描述如下：

TFSM在某一時刻，其他正交組件產生的信號稱為動作.

3）狀態

狀態是高鐵信號系統安全關鍵功能在一定時期內的存在形式.TFSM的非空、有限狀態集合記為S，Z語言描述如下：

狀態類型包括簡單狀態（PRIM），或狀態（OR）和與狀態（AND）3種，Z語言描述如下：

P::= PRIM | OR | AND

4）遷移

遷移T是TFSM從源狀態轉移到目標狀態的方式，包括源狀態sc、信號g、時鐘約束ψ、轉移時產生的動作a、重置的時鐘c及目標狀態st.遷移的Z語言描述如下：

OR狀態由同層次的狀態和遷移組成，包含且僅包含一個初始狀態，初始狀態為無源狀態，且是任意狀態的源狀態.多個并發的OR狀態組成AND狀態.

3.3 TFSM定義

本小節在TFSM基本元素的基礎上，采用Z規格說明語言定義TFSM的層次結構，給出TFSM的定義.

TFSM的狀態層次Π包括底狀態γ、為狀態分配子狀態的有限狀態層次函數h，定義狀態類型的有限狀態類型函數ε，定義狀態父狀態的函數d，滿足以下性質：

1）h為非PRIM類型的狀態分配子狀態，且狀態層次不能形成循環結構；

2）γ不為PRIM狀態，是唯一沒有父狀態的狀態；

3）任意非γ的狀態都具有唯一的父狀態，且均可以由γ通過h傳遞到達.

Π的Z模式定義如下，其中： FS表示集合S的所有有限子集的集合，domh表示h的定義域，ranh表示h的值域.

TFSM由狀態層次π和遷移集ts構成.對任意遷移，僅有一個同層次的源狀態和目標狀態.源狀態和目標狀態可以是AND或PRIM狀態.Z模式定義如下，其中： F1T表示集合T的所有非空有限子集的集合.

3.4 TFSM格局

一個時鐘集合C的時鐘解釋v是指每個時鐘變量c到時間序列上的一個全映射.某時刻，TFSM能夠同時處于的最大的狀態集結合當前的時鐘解釋稱為格局（configuration），記為u，格局對應的狀態集記為u′，初始格局記為u0，初始格局對應的狀態集記為.在任意時刻，TFSM只有一個活動的格局，滿足以下規則：

1）u′包含γ狀態；

2）u′包含 AND 狀態s，則u′包含s的每個子狀態；

3）u′包含 OR 狀態s，則u′包含s的某個子狀態；

4）u′包含非γ的狀態s，則u′包含s的父狀態.

TFSM格局的公理描述如下：

4 基于TFSM的測試用例生成方法

本節給出基于TFSM自動生成測試用例的方法.目前，針對TA和Petri網等測試模型，研究學者已經提出了許多相對成熟的測試用例自動生成算法.由于TA能夠同時描述功能邏輯和時鐘約束，本節將TFSM等價轉換為TA，利用基于TA的測試用例生成算法自動生成TFSM的測試用例.

定義2（時間自動機）一個時間自動機TA是一個六元組 (L,l0,Σ,X,M,E) ，其中：L為有限位置集合；l0∈L為初始位置； Σ 為有限字符集合；X為有限時鐘集合；M為將位置映射到時鐘約束的映射；E為轉移的集合，E?LΣ ×2xΦ(X)L， Φ (X) 為時鐘約束集合.

定義3（TFSM測試用例）對任意TFSM，如果從格局ui能夠到達格局uj，i,j≥0，則 TFSM中ui和uj之間存在一條路徑，稱該路徑為TFSM中以ui和uj為測試需求的測試用例.

定義4（TA測試用例）對任意TA，如果從位置li沿TA中的邊能夠到達lj，i,j≥0，則 TA中li和lj之間存在一條路徑，稱該路徑為TA中以li和lj節點為測試需求的測試用例.

定理 1設 κ 為一個 TFSM向一個六元組(L,l0,Σ,X,M,E)的映射，且

?l1,l2∈L， ? ∈ Σ ，x?X， φ ∈ Φ(X) ，(l1,?,x,φ,l2)∈且?u1,(l1,g,c,ψ,l2)∈E，則 (L,l0,Σ,X,M,E) 是一個與TFSM具有相同測試用例集的TA.

證明根據 κ 的定義，TFSM的格局狀態集對應TA的位置集，TFSM的初始格局狀態對應TA的初始位置，TFSM的信號集和時鐘集分別對應為TA的有限字符集和時鐘集，即 κ 將TFSM映射為一個所有位置均無時鐘約束的TA.對任意TA，?l1,l2∈L， (l1,l2)∈E，則TFSM 中 ?u1,u2∈u′，u1=l1，u2=l2.根據 κ 的定義有u1→u2.故 TA 中的任意測試 用 例l0,l1,··· 對 應 TFSM中 的 一 條 測 試 用 例u0,u1,···.

由定理1，TFSM的測試用例與TA的測試用例一一對應，如圖2所示.

圖2 TFSM 與 TA 的測試用例的關系Fig.2 Relationship of test cases between TFSM and TA

根據以上分析，基于TFSM的高鐵信號系統測試用例生成的主要過程如下：首先，測試人員采用TFSM建模方法建立高鐵信號系統安全關鍵功能的測試模型；然后，根據TFSM和TA測試用例集之間的一致性，將TFSM模型轉化為TA模型，利用基于TA的高鐵信號系統測試理論，對TA模型編制測試用例；最后，將測試用例加載到測試環境中進行測試，分析測試結果.

5 案例分析

計算機聯鎖系統是高鐵信號系統中典型的安全關鍵系統，具有SIL4的安全完整性要求.本節以計算機聯鎖系統中的道岔定位選排子系統為例建立TFSM測試模型，并轉換為TA模型編制測試用例.

5.1 基于TFSM的道岔轉換測試模型

道岔定位選排子系統根據道岔操作命令或進路請求，檢查道岔當前是否處于定位.當道岔狀態與期望不一致時，選排道岔到需求位置.該系統涉及11個信號，信號名稱及其含義如表1所示.

表1 道岔子系統信號的含義Tab.1 Meaning of signals in the switch subsystem

道岔定位選排子系統的TFSM測試模型記為DTFSM_SW，如圖3所示.

圖3 道岔定位選排測試模型Fig.3 Testing model of switch subsystem

DTFSM_SW包括1個時鐘x，初始狀態為{s1,s2,s4}，γ={s0}，ε(s4)為PRIM狀態， ε (s1) 為OR 狀態，d(s2)=s1，h(s1)={s2,s10,s11}，h(s2)={s4,s5,s6,s7,s8,s9}.

5.2 測試用例生成

DTFSM_SW通過11個狀態、15條遷移和11個信號描述道岔轉換過程的功能邏輯，通過時鐘約束x＞1、x＜ 13 和x≥ 13 描述道岔轉換過程中的信號保持時間1 s和轉換超時時間13 s的時鐘約束，為測試用例生成提供了模型基礎.

DTFSM_SW等價的TA模型DTA_SW如圖4所示.DTA_SW包括37條邊和9個節點，為描述方便，DTA_SW的狀態名僅包括DTFSM_SW格局中的PRIM狀態.

圖4 DTFSM_SW 等價的 TA 模型 DTA_SWFig.4 TA model DTA_SW equivalent to DTFSM_SW

DTA_SW的測試用例即為道岔定位選排子系統DTFSM_SW的測試用例.為檢測TFSM編制測試用例的效果，本節基于文獻[14]提出的基于模型的測試用例生成方法，以s4為測試模型的開始節點和終止節點編制測試用例.高鐵信號系統測試模型典型的測試覆蓋準則包括節點覆蓋（node coverage，NC）、邊覆蓋（edge coverage，EC）、邊對覆蓋（edge-pair coverage，EPC）、完全路徑覆蓋（complete path coverage，CPC）、主路徑覆蓋（prime path coverage，PPC）和特定路徑覆蓋（specified path coverage，SPC）等.本節以NC、EC、EPC和CPC覆蓋準則為例，生成的測試用例如表2所示，其中用例總數表示DTFSM_SW的測試用例數量，時鐘約束用例數表示DTFSM_SW中測試時鐘約束的用例數量.

表2 DTFSM_SW測試用例統計Tab.2 Test case statistics of DTFSM_SW

5.3 TFSM建模方法對比

為檢驗TFSM的建模能力，對道岔定位選排的TFSM模型與TA模型進行對比，如表3所示，其中，DTFSM_SW的狀態數為除去表示層次的OR狀態后的狀態數量.

由表3可知，DTFSM_SW與DTA_SW具有相同的狀態數和信號數，但DTA_SW的變遷數超過DTFSM_SW的2倍，導致模型更為復雜.且隨著高鐵信號系統功能邏輯復雜度的增加，TA模型的變遷數急劇增加，模型的可讀性下降，容易導致模型錯誤.與TA相比，TFSM更加直觀、清晰，可讀性良好，更適合描述高鐵信號系統復雜的功能邏輯.

表3 DTFSM_SW與DTA_SW對比Tab.3 Comparison of DTFSM_SW and DTA_SW

為檢驗TFSM在編制測試用例方面的有效性，選擇高鐵信號系統安全關鍵功能中廣泛采用的Petri網和UML Statechart建模方法對道岔定位選排子系統進行建模，以CPC覆蓋準則為例編制測試用例，對比結果如表4所示.

由表4可知，TFSM、Petri網和 UML Statechart建模方法在功能邏輯方面生成的測試用例數相同，但TFSM比Petri網和UML Statechart多生成了16條具有時鐘約束的測試用例，如表5所示.

表4 不同建模方法生成的測試用例對比Tab.4 Comparison of test cases generated by different modeling methods

表5 DTFSM_SW具有時鐘約束的測試案例Tab.5 Test cases with clock constraints of DTFSM_SW

根據以上分析，TFSM建模方法適合描述高鐵信號系統安全關鍵功能復雜的邏輯，并生成全面的覆蓋功能邏輯和時鐘約束的測試用例，能夠滿足高鐵信號系統安全關鍵功能在功能邏輯和時鐘約束方面的測試建模需求.

6 結 論

1）高鐵信號系統安全關鍵功能的測試建模方法不能很好地描述系統特征，不具有描述時鐘約束的能力，或難以描述安全關鍵功能邏輯的復雜性.

2）本文提出的時間狀態機建模方法以有限狀態機理論為基礎，具有嚴格的形式化定義，能夠等價轉化為時間自動機結構.

3）通過道岔子系統的案例分析，時間狀態機能夠滿足高鐵信號系統安全關鍵功能在功能邏輯和時鐘約束方面的測試建模需求，為高鐵信號系統測試提供了形式化建模的理論基礎.

4）本文提出的方法已在高鐵信號系統的計算機聯鎖和ATP設備的系統測試中得到應用，實踐表明該方法能夠提高高鐵信號系統安全關鍵功能測試的完備性和測試效率.

致謝：本文工作得到高鐵信號工程列控系統第三方仿真測試技術研究（N2018G062）項目的資助.