鐵路信號系統(tǒng)軟件測試建模方法

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

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

截止2019年底，我國高速鐵路營業(yè)里程已達到3.5萬公里，位居世界第一. 我國已成為世界上高鐵運營里程最長、運輸密度最高、運營場景最復雜的國家. 鐵路信號系統(tǒng)軟件測試是保障高鐵信號系統(tǒng)安全運行的重要方法，能夠有效地預防列車追尾和出軌等行車事故，避免造成人員傷亡及重大財產損失[1]，對保障我國高鐵的安全運行具有重要意義.

目前，高鐵信號系統(tǒng)軟件測試的研究熱點之一為基于形式化模型的測試案例自動編制方法，其首先建立軟件的測試模型，然后研究算法自動生成滿足特定目標的測試案例. 鐵路信號系統(tǒng)軟件測試中常用的建模方法包括UML狀態(tài)圖（UML statechart）、時間自動機（timed automata，TA）和有色Petri網（colored Petri net，CPN）等. 文獻[2]以CPN為測試建模理論基礎，以無線閉塞中心切換功能為例，研究基于全路徑覆蓋和序列優(yōu)選的測試案例自動編制方法，降低測試案例的重復度. 文獻[3]以CTCS-3（Chinese Train Control System 3）級ATP （automatic train protection）設備模式轉換功能為例，基于CPN建模理論，解決狀態(tài)空間爆炸等問題，生成滿足全路徑覆蓋準則的測試序列. 文獻[4]以TA為基礎進行測試建模，提出一種滿足全狀態(tài)和全變遷覆蓋準則的測試案例生成方法，提高測試案例的生成效率和重用性. 文獻[5]研究CTCS-3故障特點，提出了一種基于輸入輸出時間自動機變異模型的測試案例生成方法. 文獻[6]以軌道電路編碼功能為研究對象，提出圖覆蓋、組合覆蓋和文法分析相結合的方式自動從UML狀態(tài)圖模型生成測試案例. 文獻[7]以UML順序圖為研究基礎，利用深度優(yōu)先算法和網絡組合算法對計算機聯鎖系統(tǒng)測試案例進行組合優(yōu)化，降低測試案例的重復度. 文獻[8]針對鐵路信號系統(tǒng)軟件的測試度量方法，提出對信號系統(tǒng)軟件進行風險分級，按照風險等級遞減順序進行安全性測試的測試策略，指出了以鐵路信號系統(tǒng)軟件風險等級為基礎測試的必要性. 文獻[9]對CTCS-3系統(tǒng)安全軟件進行接口危險辨識，評估危險事件的風險等級，提出列控系統(tǒng)安全軟件黑盒測試的危險分析方法，但未對軟件測試建模理論進行研究. 文獻[10-12]針對鐵路信號系統(tǒng)的形式化描述和驗證，分別從時鐘約束、風險等級和安全約束等幾個方面提出鐵路信號系統(tǒng)的建模方法，但這些方法結構復雜，測試模型解析和測試案例搜索算法難以展開，不易直接應用于鐵路信號系統(tǒng)軟件測試建模.

目前，鐵路信號系統(tǒng)軟件測試的研究重點是如何以既有的測試建模方法為基礎生成覆蓋全面且高效的測試案例，研究提高了測試活動的自動化程度和測試效率. 但現有測試建模方法不能完整地描述軟件所有的行為特征，如UML狀態(tài)圖和CPN等方法不能描述軟件的時間約束，導致測試案例不能反映軟件的時間特性. TA能夠描述軟件的時間約束，但不具有層次結構，對復雜功能邏輯的描述能力較差，容易出現模型難以理解，甚至錯誤的問題. 同時，UML狀態(tài)圖、CPN和TA等方法均不能描述軟件測試模型中的風險特性.

本文通過分析鐵路信號軟件的領域特點，總結鐵路信號軟件測試的建模需求，結合Z規(guī)格說明語言（簡稱Z語言）提出風險時間狀態(tài)機建模方法，滿足鐵路信號軟件測試的建模需求.

1 建模概述

鐵路信號系統(tǒng)軟件測試通常采用基于模型的測試（model-based testing，MBT）[13]理論，主要包括分析軟件需求、建立測試模型、生成測試案例和執(zhí)行測試4個階段，如圖1所示. 首先，基于被測軟件的需求規(guī)格等文件對軟件功能和結構進行抽象，采用形式化建模方法建立軟件的測試模型；然后，依據測試模型，采用“平坦化”和狀態(tài)組合等方法對測試模型進行解析，通過廣度優(yōu)先等搜索算法自動生成測試案例；最后，將測試案例加載到測試環(huán)境中執(zhí)行測試，觀察測試結果.

圖1 鐵路信號系統(tǒng)軟件測試主要過程Fig. 1 Main testing process of railway signal system software

測試模型是編制測試案例和評判測試結果時的重要依據，直接關系到軟件測試過程的全面性和有效性，鐵路信號軟件測試建模方法需要盡可能系統(tǒng)、全面地描述鐵路信號系統(tǒng)軟件的所有需求.

2 建模需求

鐵路信號系統(tǒng)軟件測試建模包括功能建模需求和性能建模需求兩個方面. 功能建模需求描述系統(tǒng)的功能邏輯（function logic），性能建模需求指與系統(tǒng)相關的性能約束或限制，包括時鐘約束（clock constraint）和風險等級（risk level）兩個方面.

1） 功能邏輯

隨著鐵路信號系統(tǒng)的規(guī)模越來越大，軟件承擔的功能越來越多、邏輯越來越復雜. 如CTCS-3級列控系統(tǒng)包括9種工作模式，14個主要運營場景，206個功能特征. 鐵路信號系統(tǒng)已構成一個復雜的控制系統(tǒng)，軟件存在著大量的并發(fā)、競爭、沖突等邏輯關系，控制狀態(tài)轉移條件復雜.

2） 時鐘約束

鐵路信號系統(tǒng)軟件運算結果的正確性不僅取決于系統(tǒng)邏輯處理的正確性，還取決于運算過程中的時鐘約束，要求軟件功能需要在指定時間內完成，或在規(guī)定時限之后才能發(fā)生. 如《CTCS-3級列控系統(tǒng)總體技術方案》[14]要求“當列車前端距分相區(qū)還有10秒走行距離時，車載設備向司機發(fā)出提示”. 鐵路信號系統(tǒng)軟件的時鐘約束通常為硬實時性（hard real-time）要求，如道岔轉換時間、移動授權有效時間、目視模式確認時間等，時鐘約束錯誤或缺失，可能造成重大安全事故.

3） 風險等級

鐵路信號系統(tǒng)軟件由安全功能（safety function）、安全相關功能（safety-related function）和非安全功能（non-safety function）組合構成. 如 《CTCS-3級列控系統(tǒng)測試案例（V3.0）》[15]的功能特征CTCS3-FT-71“由于超速觸發(fā)緊急制動”屬于安全功能，功能特征CTCS3-FT-116“記錄數據的下載”屬于非安全功能. 不同安全級別的功能對系統(tǒng)造成的安全影響差別較大，由風險等級進行描述. 風險等級的高低是鐵路信號系統(tǒng)軟件測試案例編制的重要基礎，對組織測試案例優(yōu)先級及分析測試需求具有重要意義.

根據以上分析，鐵路信號系統(tǒng)軟件測試建模方法需要描述系統(tǒng)復雜的功能邏輯、時鐘約束和風險等級3個方面的特點，嚴密、準確地反應軟件測試需求，且具有良好的可讀性和可理解性.

3 風險時間狀態(tài)機

為定義風險時間狀態(tài)機建模方法，首先介紹有限狀態(tài)機（finite state machine, FSM），然后在FSM基礎上，結合Z語言，在遷移元素中擴展出時鐘約束，在狀態(tài)元素中擴展出風險等級，最后給出風險時間狀態(tài)機的定義.

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

FSM采用可視化的方式描述系統(tǒng)的功能邏輯，具有清晰、直觀的優(yōu)點，其是表示有限狀態(tài)以及狀態(tài)之間轉移和動作等行為的數學模型，具有精確性、可推導性和可驗證性，是基于模型的測試理論中的經典建模方法[13-16].

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

式中：

S為有限狀態(tài)集合；

s0為初始狀態(tài)，且s0∈S；

λ為狀態(tài)轉移函數，λ:S×I→S；

δ為輸出函數，δ :S×I→O；

I為有限輸入符號集合；

O為有限輸出符號集合.

圖2為一個FSM模型，包括s1和s2兩個狀態(tài)，其中s1為初始狀態(tài)，A、B、C為輸入，a、b、c為輸出.s1接收到輸入A時輸出a，轉移到s2狀態(tài). 模型對應的六元組如下：

圖2 有限狀態(tài)機模型Fig. 2 Example of finite state machine

接下來結合Z語言，在FSM描述功能邏輯基礎上，增加層次結構，擴展出時鐘約束和風險等級兩個參數，提出風險時間狀態(tài)機（risk timed statechart，RTSC）. 為描述方便，首先定義RTSC的基本元素，然后定義RTSC的層次結構，最后給出RTSC的形式化定義.

3.2 RTSC的基本元素

RTSC包括狀態(tài)、時鐘、信號表達式和遷移等基本元素.

1） 狀態(tài)

狀態(tài)是鐵路信號系統(tǒng)軟件在一定時期內的存在形式. 對RTSC的非空、有限狀態(tài)集合S，Z語言描述如下：

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

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

2） 時鐘

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

對一個時鐘變量集合X，時間約束集合定義如式（2）.

式中：σ1、σ2為時鐘約束；x∈X；g∈N ；∝∈{≤,<,≥,>,=}.

RTSC時鐘約束Σ的Z語言描述如下：

3） 信號

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

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

4） 信號表達式

信號之間的與（and）關系、或（or）關系、非（not）關系構成信號表達式，記為ex如note表示未產生信號e.

用Π為表示信號永遠發(fā)生的常量.

5） 遷移

遷移是RTSC從源狀態(tài)轉移到目標狀態(tài)的方式，包括源狀態(tài)sc、時鐘約束σ、信號表達式ex、轉移時產生的信號e、重置的時鐘x及目標狀態(tài)st. 遷移的Z語言描述如下：

3.3 RTSC的層次結構

RTSC的狀態(tài)層次H包括底狀態(tài)γ、為狀態(tài)分配子狀態(tài)的有限狀態(tài)層次函數ω，定義狀態(tài)類型的有限狀態(tài)類型函數κ，定義狀態(tài)父狀態(tài)的ρ函數.H滿足以下性質：

1）ω為非SIMPLE類型的狀態(tài)分配子狀態(tài)；

2） 狀態(tài)之間的層次關系不能形成循環(huán)結構；

3）γ為OR狀態(tài)或AND狀態(tài)，是唯一沒有父狀態(tài)的狀態(tài)；

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

H的Z模式定義如下：

其中：FS表示集合S的所有有限子集的集合；domω表示ω的定義域；ranρ表示ρ的值域；?si:domρ;sj: domω表示ρ定義域中的任意狀態(tài)si和ω定義域中的任意狀態(tài)sj，i，j為不為0的自然數，且i≠j.

RTSC由狀態(tài)層次和遷移集構成，采用風險等級函數η為SIMPLE狀態(tài)分配風險等級，滿足以下性質：

1）η僅為SIMPLE狀態(tài)分配風險等級；

2） OR狀態(tài)和AND狀態(tài)的風險等級為其包含的子狀態(tài)的風險等級的最大值.

3） 對任意遷移，只能有一個同層次的源狀態(tài)和目標狀態(tài)，源狀態(tài)和目標狀態(tài)可以是AND或SIMPLE狀態(tài).

RTSC的Z模式定義如下：

其中：F1T表示集合T的所有非空有限子集的集合.

4 RTSC的格局轉移機制

4.1 格局

一個時鐘集合X的時鐘解釋v是指每個時鐘變量x到時間序列上的一個全映射. 某時刻，RTSC能夠同時處于最大的狀態(tài)集結合當前的時鐘解釋稱為格局（configuration），記為U. 在任意時刻，RTSC只有一個活動的格局，滿足以下規(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)；

5）U僅包含滿足規(guī)則1） ~ 4）的所有狀態(tài).

格局公理描述如下：

其中：k表示不為0的自然數.

4.2 格局轉移機制

RTSC格 局 轉 移 過 程 記 為 (us,v(X),E)，其 中us表示當前格局包含的狀態(tài)集，v(X)表示時鐘解釋，E表示轉移過程中產生的動作集，具體過程如下：

1） 激勵. 當RTSC接受到新的時鐘解釋或信號時開始格局轉移：(us,v(X),?)→(us,v′(X),e).

2） 計算. 格局轉移過程以SIMPLE狀態(tài)為基礎，從γ狀態(tài)，通過OR狀態(tài)和AND狀態(tài)向下分解，包括以下2個規(guī)則：

規(guī)則1AND狀態(tài)并行地計算其所包含的OR狀態(tài)的轉移.

規(guī)則2OR狀態(tài)計算當前激活的SIMPLE狀態(tài)的變遷t上的信號，產生t上的動作，重置t的時鐘，離開變遷源狀態(tài)τ.sc到達變遷狀態(tài)t.st，滿足：us=us .sc∪t.st，G=G∪t.e，v(t.x)=0.

3） 結束. RTSC根據狀態(tài)類型迭代相應規(guī)則直至轉移穩(wěn)定，保留時鐘解釋，清空轉移期間的信號.

RTSC從初始格局開始，根據產生的信號或時鐘的更新激活格局轉移過程；依據層次結構，迭代AND狀態(tài)和OR狀態(tài)的規(guī)則，直到計算出下一組穩(wěn)定的狀態(tài). 格局轉移時，遷移的觸發(fā)信號均發(fā)生，且時鐘解釋滿足遷移上的時鐘約束，同時產生遷移上的動作，重置遷移上的時鐘變量.

4.3 RTSC的操作語義

RTSC的語義可以由其對應的時間標記遷移系統(tǒng)（timed transition system，TTS）進行定義.

定義2一個時間標記遷移系統(tǒng)TTS是一個4元組：

式中：L為狀態(tài)集合；

l0為初始狀態(tài)，l0∈L；

→?L×(Σ∪R)×L為轉移關系，且滿足：1） 如果，則l=l′； 2） 如果，且，d,d′∈R，則； 3） 如果則0 ≤d′≤d，則有l(wèi)′′∈L，滿足且

在時鐘解釋v下，如果時鐘約束σ為真，則稱時鐘解釋v滿足時鐘約束σ，記為v|=σ.

定義3對任意RTSC，其語義可以通過時間標記遷移系統(tǒng) Ω=(L,l0,→,Σ)進行定義，其中：

l0=(us0,v0) ，us0為RTSC的初始狀態(tài)集，且對任意x∈X，v0(x)=0；

轉 移 關 系 → 滿 足：1） 對 (us,v)和 一 個 遷 移且v|=σ ，則對和時間增量

RTSC從初始格局開始，通過動作轉移或時延轉移實現格局變化.

1） 動作轉移. 當前激活的信號和時鐘解釋滿足變遷的信號表達式和時鐘約束，觸發(fā)動作遷移，激活變遷上的動作，重置變遷時鐘為0.

2） 時延轉移. 時延轉移保持格局狀態(tài)不變，對所有時鐘增加相同的時間增量.

5 案例分析

計算機聯鎖系統(tǒng)是鐵路信號系統(tǒng)中典型的安全關鍵系統(tǒng). 以計算機聯鎖系統(tǒng)的道岔定位選排子系統(tǒng)為例建立RTSC測試模型，解釋RTSC的格局轉移機制.

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

道岔定位選排子系統(tǒng)根據道岔操作命令或進路請求，檢查道岔當前是否處于定位. 當道岔狀態(tài)與期望不一致時，選排道岔到需求位置[18]. 該系統(tǒng)涉及11個信號，主要信號名稱及其含義見表1.

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

道岔定位選排子系統(tǒng)的RTSC模型如圖3所示，記為DRTSC，其中ranη= {0, 1, 2, 3, 4}，分別對應EN 50128定義的5個安全完整度等級SIL 0～4.DRTSC包括1個時鐘x1，最高風險等級為SIL 4，最低為SIL 2，底狀態(tài)為s0，初始狀態(tài)為 {s3,s4,s5,s6,s9,s11}，s1、s2、s3分別為SIMPLE狀態(tài)、AND狀態(tài)和OR狀態(tài) ，η (s1)=4 ，η (s3)=max(η(s6),η(s7),η(s8))=4，ρ(s2)=s0，ω(s2)={s3,s4,s5}.

圖3 道岔子系統(tǒng)RTSC模型Fig. 3 RTSC model of switch subsystem

DRTSC中：遷移的表現形式為[e] [σ] / [a] [x]；e為觸發(fā)轉移的信號；σ為時鐘約束；a為轉移時產生的動作；x為重置的時鐘，記為. 如表示狀態(tài)s14激活時，當檢測到信號e7，并滿足時間約束x1<13，DRTSC遷移到s13，同時產生信號e8，并重置時鐘x1.

5.2 DRTSC格局轉移

DRTSC模型中，s3、s4、s5分別表示道岔轉換的“安全請求”，“道岔轉換”和轉換的“時鐘約束”狀態(tài).DRTSC主要描述以下過程：

道岔“安全請求”狀態(tài)檢測到定位需求后，在道岔未鎖閉、無反位請求、未處于定位時，進一步檢查道岔轉換狀態(tài)，未處于轉換過程中或轉換超時時，判定定位請求安全. “道岔轉換”狀態(tài)接受到“定位請求”信號后，如果道岔未鎖閉則重置時鐘x1；條件保持1 s后，請求道岔轉換. “時鐘約束”狀態(tài)接受道岔轉換動作后，重置時鐘x1并開始計時，13 s內檢測到道岔轉換到定位則轉換成功，否則轉換超時. 當“道岔轉換”狀態(tài)接受到“時鐘約束”狀態(tài)的“轉換成功”信號后判定道岔轉換成功. 當同時處于“定位請求”和“轉換成功”狀態(tài)時，判定“選排一致”. 轉換過程中任意時刻，道岔子系統(tǒng)接受到反位請求信號立即重置時鐘，返回初始狀態(tài).

DRTSC的初始格局為 ((s0,s2,s3,s4,s5,s6,s9,s13),(0)) . 下面以格局 ( (s0,s3,s4,s5,s8,s11,s14),(2))，產生信號e7，v(x)=3為例，分析DRTSC的格局轉移過程.

1）DRTSC接受激勵信號和更新的時鐘解釋：((s0,s2,s3,s4,s5,s8,s11,s14),(2),(?))→ ((s0,s2,s3,s4,s5,s8,s11,s14),(3),(e7)).

2） 由于s0為OR狀態(tài)，根據規(guī)則 2，s0當前激活狀態(tài)為s2.s2為AND狀態(tài)，根據規(guī)則 1，s2并行計算s3,s4,s5，計算過程為

e7和v(x)=3 滿 足s14遷 移 到s13的 信 號 表 達 式和時鐘約束，遷移時重置時鐘x1，同時產生信號e8: ((s0,s2,s3,s4,s5,s8,s11,s14),(3),(e7))→((s0,s2,s3,s4,s5,s8,s11,s13),(0),(e7,e8));

e8信號觸發(fā)s4的子狀態(tài)s11，并轉移到狀態(tài)s12：((s0,s2,s3,s4,s5,s8,s11,s13),(0),(e7,e8))→((s0,s2,s3,s4,s5,s8,s12,s13),(0),(e7,e8,e11));

s3的狀態(tài)s8滿足自遷移變遷：((s0,s2,s3,s4,s5,s8,s12,s13),(0),(e7,e8,e11))→((s0,s2,s3,s4,s5,s8,s12,s13), ( 0),(e7,e8,e11,e1)).

s3，s4和s5計算結束后，DRTSC激活的信號包括 (e7,e8,e11,e1) ，激活s2至s1的遷移：((s0,s2,s3,s4,s5,s8,s12,s13),(0),(e7,e8,e11,e1)).+→ ((s0,s1),(0),(e7,e8,e11,e1)).

3） 計算結束，DRTSC格局更新為 ( (s0，s1),(0)).

根據以上分析，DRTSC格局轉移過程記為表示道岔在處于“定位安全請求”，“道岔轉換”，“道岔轉換計時中”狀態(tài)時，檢測到道岔在第3 s轉移到定位，判定道岔選排一致.

5.3 DRTSC模型分析

DRTSC描述了道岔定位轉移過程中的功能邏輯、時鐘約束和風險等級.

5.3.1 測試需求覆蓋

1） 功能邏輯

DRTSC采用16個狀態(tài)，19條遷移和11個信號描述道岔轉換過程的功能邏輯.

2） 時鐘約束

DRTSC通過時鐘x1描述道岔轉換過程中信號保持時間1 s和轉換超時判斷時間13 s，包括時鐘約束x1>1，x1<13和x1≥ 13. 如描述道岔轉換超過13 s后進入超時狀態(tài)s15.

3） 風險等級

DRTSC描述了道岔轉換過程中風險等級的變化情況，包括風險等級升高、降低以及保持不變，風險轉移矩陣如圖4所示. 其中，正數表示風險等級升高，負數表示風險等級降低，0表示風險等級不變，“?”表示狀態(tài)之間無轉移關系.

圖4 道岔子系統(tǒng)風險矩陣Fig. 4 Risk matrix of switch subsystem

如R78= 1描 述 了 遷 移(s8,4)，表示道岔由SIL 3的狀態(tài)s7轉移到SIL 4的s8，風險等級升高1個等級，軟件測試時需要重點對此類變遷進行測試.

5.3.2 與TA對比

為檢測RTSC模型的描述能力，選取鐵路信號系統(tǒng)軟件測試中廣泛采用的TA建模方法進行對比.道岔定位選排的TA模型如圖5所示，記為DTA.DTA由4個TA構件組成TA網絡實現道岔定位選排的測試需求，其中，為描述DRTSC的否定信號，如未接收到信號e5，在DTA中增加en5.DTA和DRTSC均包括1個時鐘，狀態(tài)、變遷和信號數量方面的比較如表2所示，DRTSC比DTA節(jié)省62%的變遷數，節(jié)省54%的狀態(tài)數. 其中，DRTSC的狀態(tài)數為除去層次結構后的SIMPLE狀態(tài)的數量.

圖5 道岔子系統(tǒng)TA模型Fig. 5 TA model of switch subsystem

進一步，隨機選取計算機聯鎖系統(tǒng)軟件中的4個子功能，分別采用RTSC和TA進行建模，RTSC模型和TA模型在構件、狀態(tài)和變遷3個方面的對比如圖6所示.

圖6 RTSC模型與TA模型對比Fig. 6 Comparison between RTSC model and TA model

通過表2和圖6，相對TA建模方法，RTSC模型具有更少的構件數、狀態(tài)數、變遷數和信號數. 且隨著功能邏輯復雜度的增加，RTSC節(jié)省的狀態(tài)數和變遷數越多，RTSC模型更為簡潔、清晰，表達能力更強，可讀性更高，適合描述鐵路信號系統(tǒng)軟件復雜的功能邏輯.

表2 DRTSC與DTA 對比Tab. 2 Comparison betweenDRTSC andDTA

RTSC繼承了FSM可視化、直觀和簡介的特點，其狀態(tài)轉移、層次性和并發(fā)性能夠描述軟件的功能邏輯，時鐘約束能夠描述軟件的時間關系，風險等級能夠描述軟件不同功能之間的安全性關系. 具體的，RTSC與鐵路信號系統(tǒng)軟件測試建模需求之間的關系如表3所示.

表3 RTSC與測試需求的關系Tab. 3 Relationship between RTSC and test requirements

6 結 論

1） 鐵路信號系統(tǒng)軟件測試建模方法不能很好地描述鐵路信號系統(tǒng)軟件測試的建模需求，不能同時描述軟件的功能邏輯、時鐘約束和風險等級3個方面的特征.

2） 以有限狀態(tài)機理論為基礎，擴展出時鐘約束和風險等級屬性，提出風險時間狀態(tài)機建模方法，采用Z語言給出了風險時間狀態(tài)機的定義，闡述了風險時間狀態(tài)機的格局轉移規(guī)則，滿足鐵路信號系統(tǒng)軟件測試在功能邏輯、時鐘約束和風險等級方面的建模需求.

3） 以計算機聯鎖系統(tǒng)中的道岔子系統(tǒng)為例，利用風險時間狀態(tài)機建立了道岔子系統(tǒng)軟件的測試模型，并選取TA建模方法進行對比，結果表明風險時間狀態(tài)機描述能力更強.

4） 文章提出的方法已在計算機聯鎖系統(tǒng)的軟件測試中得到應用，實踐表明該方法能夠滿足鐵路信號系統(tǒng)軟件測試的建模需求，為鐵路信號系統(tǒng)軟件測試提供了形式化建模的理論基礎.