李 耀 ，張曉霞 ，郭 進(jìn) ，張亞東

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

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

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

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

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

1 建模概述

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

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

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

2 建模需求

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

1） 功能邏輯

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

2） 時鐘約束

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

3） 風(fēng)險等級

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

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

3 風(fēng)險時間狀態(tài)機(jī)

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

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

FSM采用可視化的方式描述系統(tǒng)的功能邏輯，具有清晰、直觀的優(yōu)點，其是表示有限狀態(tài)以及狀態(tài)之間轉(zhuǎn)移和動作等行為的數(shù)學(xué)模型，具有精確性、可推導(dǎo)性和可驗證性，是基于模型的測試?yán)碚撝械慕?jīng)典建模方法[13-16].

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

式中：

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

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

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

δ為輸出函數(shù)，δ :S×I→O；

I為有限輸入符號集合；

O為有限輸出符號集合.

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

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

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

3.2 RTSC的基本元素

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

1） 狀態(tài)

狀態(tài)是鐵路信號系統(tǒng)軟件在一定時期內(nèi)的存在形式. 對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具有產(chǎn)生和不產(chǎn)生兩種狀態(tài)，Z語言描述如下：

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

4） 信號表達(dá)式

信號之間的與（and）關(guān)系、或（or）關(guān)系、非（not）關(guān)系構(gòu)成信號表達(dá)式，記為ex如note表示未產(chǎn)生信號e.

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

5） 遷移

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

3.3 RTSC的層次結(jié)構(gòu)

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

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

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

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

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

H的Z模式定義如下：

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

RTSC由狀態(tài)層次和遷移集構(gòu)成，采用風(fēng)險等級函數(shù)η為SIMPLE狀態(tài)分配風(fēng)險等級，滿足以下性質(zhì)：

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

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

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

RTSC的Z模式定義如下：

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

4 RTSC的格局轉(zhuǎn)移機(jī)制

4.1 格局

一個時鐘集合X的時鐘解釋v是指每個時鐘變量x到時間序列上的一個全映射. 某時刻，RTSC能夠同時處于最大的狀態(tài)集結(jié)合當(dāng)前的時鐘解釋稱為格局（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的自然數(shù).

4.2 格局轉(zhuǎn)移機(jī)制

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

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

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

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

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

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

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

4.3 RTSC的操作語義

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

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

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

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

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

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

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

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

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

RTSC從初始格局開始，通過動作轉(zhuǎn)移或時延轉(zhuǎn)移實現(xiàn)格局變化.

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

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

5 案例分析

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

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

道岔定位選排子系統(tǒng)根據(jù)道岔操作命令或進(jìn)路請求，檢查道岔當(dāng)前是否處于定位. 當(dāng)?shù)啦頎顟B(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}，分別對應(yīng)EN 50128定義的5個安全完整度等級SIL 0～4.DRTSC包括1個時鐘x1，最高風(fēng)險等級為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中：遷移的表現(xiàn)形式為[e] [σ] / [a] [x]；e為觸發(fā)轉(zhuǎn)移的信號；σ為時鐘約束；a為轉(zhuǎn)移時產(chǎn)生的動作；x為重置的時鐘，記為. 如表示狀態(tài)s14激活時，當(dāng)檢測到信號e7，并滿足時間約束x1<13，DRTSC遷移到s13，同時產(chǎn)生信號e8，并重置時鐘x1.

5.2 DRTSC格局轉(zhuǎn)移

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

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

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

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)，根據(jù)規(guī)則 2，s0當(dāng)前激活狀態(tài)為s2.s2為AND狀態(tài)，根據(jù)規(guī)則 1，s2并行計算s3,s4,s5，計算過程為

e7和v(x)=3 滿 足s14遷 移 到s13的 信 號 表 達(dá) 式和時鐘約束，遷移時重置時鐘x1，同時產(chǎn)生信號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，并轉(zhuǎn)移到狀態(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計算結(jié)束后，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） 計算結(jié)束，DRTSC格局更新為 ( (s0，s1),(0)).

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

5.3 DRTSC模型分析

DRTSC描述了道岔定位轉(zhuǎn)移過程中的功能邏輯、時鐘約束和風(fēng)險等級.

5.3.1 測試需求覆蓋

1） 功能邏輯

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

2） 時鐘約束

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

3） 風(fēng)險等級

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

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

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

5.3.2 與TA對比

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

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

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

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

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

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

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

表3 RTSC與測試需求的關(guān)系Tab. 3 Relationship between RTSC and test requirements

6 結(jié) 論

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

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

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

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