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

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

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

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

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

1 問題描述

1.1 高鐵信號系統(tǒng)測試用例生成方法概述

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

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

1.2 高鐵信號系統(tǒng)測試建模的問題

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

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

2 高鐵信號系統(tǒng)測試建模需求

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

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

1）功能邏輯

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

2）時鐘約束

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

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

3 時間狀態(tài)機測試建模方法

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

3.1 有限狀態(tài)機概述

FSM是表示有限狀態(tài)以及狀態(tài)之間轉(zhuǎn)移和動作等行為的數(shù)學(xué)模型，具有精確性、可推導(dǎo)性和可驗證性.

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

式中：S為有限狀態(tài)集合；s0為初始狀態(tài)，s0∈S；λ為狀態(tài)轉(zhuǎn)移函數(shù)， λ :SI→S；δ為輸出函數(shù)， δ:SI→O；I為有限輸入符號集合；O為有限輸出符號集合.

圖1為一個開關(guān)的FSM模型.

圖1 有限狀態(tài)機示例Fig.1 Example of finite state machine

圖1 中包括關(guān)（soff）和開（son）兩個狀態(tài)，其中soff為初始狀態(tài).soff接收到輸入A時轉(zhuǎn)移到son狀態(tài)，輸出A′，son接收到輸入B時轉(zhuǎn)移到soff狀態(tài)，輸出B′.模型對應(yīng)的六元組如式（2）.

根據(jù)FSM的定義，F(xiàn)SM缺少描述時鐘約束的機制.接下來結(jié)合Z規(guī)格說明語言，在FSM描述功能邏輯的基礎(chǔ)上，增加層次結(jié)構(gòu)，擴展出時鐘約束，提出時間狀態(tài)機（timed finite state machine，TFSM）.

3.2 TFSM基本元素

TFSM包括時鐘、信號和狀態(tài)等基本元素.

1）時鐘

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

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

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

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

2）信號

信號具有產(chǎn)生和不產(chǎn)生兩種狀態(tài)，Z語言描述如下：

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

3）狀態(tài)

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

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

P::= PRIM | OR | AND

4）遷移

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

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

3.3 TFSM定義

本小節(jié)在TFSM基本元素的基礎(chǔ)上，采用Z規(guī)格說明語言定義TFSM的層次結(jié)構(gòu)，給出TFSM的定義.

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

1）h為非PRIM類型的狀態(tài)分配子狀態(tài)，且狀態(tài)層次不能形成循環(huán)結(jié)構(gòu)；

2）γ不為PRIM狀態(tài)，是唯一沒有父狀態(tài)的狀態(tài)；

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

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

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

3.4 TFSM格局

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

1）u′包含γ狀態(tài)；

2）u′包含 AND 狀態(tài)s，則u′包含s的每個子狀態(tài)；

3）u′包含 OR 狀態(tài)s，則u′包含s的某個子狀態(tài)；

4）u′包含非γ的狀態(tài)s，則u′包含s的父狀態(tài).

TFSM格局的公理描述如下：

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

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

定義2（時間自動機）一個時間自動機TA是一個六元組 (L,l0,Σ,X,M,E) ，其中：L為有限位置集合；l0∈L為初始位置； Σ 為有限字符集合；X為有限時鐘集合；M為將位置映射到時鐘約束的映射；E為轉(zhuǎn)移的集合，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中l(wèi)i和lj之間存在一條路徑，稱該路徑為TA中以li和lj節(jié)點為測試需求的測試用例.

定理 1設(shè) κ 為一個 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.

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

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

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

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

5 案例分析

計算機聯(lián)鎖系統(tǒng)是高鐵信號系統(tǒng)中典型的安全關(guān)鍵系統(tǒng)，具有SIL4的安全完整性要求.本節(jié)以計算機聯(lián)鎖系統(tǒng)中的道岔定位選排子系統(tǒng)為例建立TFSM測試模型，并轉(zhuǎn)換為TA模型編制測試用例.

5.1 基于TFSM的道岔轉(zhuǎn)換測試模型

道岔定位選排子系統(tǒng)根據(jù)道岔操作命令或進路請求，檢查道岔當前是否處于定位.當?shù)啦頎顟B(tài)與期望不一致時，選排道岔到需求位置.該系統(tǒng)涉及11個信號，信號名稱及其含義如表1所示.

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

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

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

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

5.2 測試用例生成

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

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

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

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

表2 DTFSM_SW測試用例統(tǒng)計Tab.2 Test case statistics of DTFSM_SW

5.3 TFSM建模方法對比

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

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

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

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

由表4可知，TFSM、Petri網(wǎng)和 UML Statechart建模方法在功能邏輯方面生成的測試用例數(shù)相同，但TFSM比Petri網(wǎng)和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

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

6 結(jié) 論

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

2）本文提出的時間狀態(tài)機建模方法以有限狀態(tài)機理論為基礎(chǔ)，具有嚴格的形式化定義，能夠等價轉(zhuǎn)化為時間自動機結(jié)構(gòu).

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

4）本文提出的方法已在高鐵信號系統(tǒng)的計算機聯(lián)鎖和ATP設(shè)備的系統(tǒng)測試中得到應(yīng)用，實踐表明該方法能夠提高高鐵信號系統(tǒng)安全關(guān)鍵功能測試的完備性和測試效率.

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