李 耀 ,張曉霞 ,郭 進 ,張亞東
(1. 電子科技大學光電科學與工程學院, 四川 成都 611731;2. 西南交通大學信息科學與技術學院, 四川 成都611756)
截止2019年底,我國高速鐵路營業里程已達到3.5萬公里,位居世界第一. 我國已成為世界上高鐵運營里程最長、運輸密度最高、運營場景最復雜的國家. 鐵路信號系統軟件測試是保障高鐵信號系統安全運行的重要方法,能夠有效地預防列車追尾和出軌等行車事故,避免造成人員傷亡及重大財產損失[1],對保障我國高鐵的安全運行具有重要意義.
目前,高鐵信號系統軟件測試的研究熱點之一為基于形式化模型的測試案例自動編制方法,其首先建立軟件的測試模型,然后研究算法自動生成滿足特定目標的測試案例. 鐵路信號系統軟件測試中常用的建模方法包括UML狀態圖(UML statechart)、時間自動機(timed automata,TA)和有色Petri網(colored Petri net,CPN)等. 文獻[2]以CPN為測試建模理論基礎,以無線閉塞中心切換功能為例,研究基于全路徑覆蓋和序列優選的測試案例自動編制方法,降低測試案例的重復度. 文獻[3]以CTCS-3(Chinese Train Control System 3)級ATP (automatic train protection)設備模式轉換功能為例,基于CPN建模理論,解決狀態空間爆炸等問題,生成滿足全路徑覆蓋準則的測試序列. 文獻[4]以TA為基礎進行測試建模,提出一種滿足全狀態和全變遷覆蓋準則的測試案例生成方法,提高測試案例的生成效率和重用性. 文獻[5]研究CTCS-3故障特點,提出了一種基于輸入輸出時間自動機變異模型的測試案例生成方法. 文獻[6]以軌道電路編碼功能為研究對象,提出圖覆蓋、組合覆蓋和文法分析相結合的方式自動從UML狀態圖模型生成測試案例. 文獻[7]以UML順序圖為研究基礎,利用深度優先算法和網絡組合算法對計算機聯鎖系統測試案例進行組合優化,降低測試案例的重復度. 文獻[8]針對鐵路信號系統軟件的測試度量方法,提出對信號系統軟件進行風險分級,按照風險等級遞減順序進行安全性測試的測試策略,指出了以鐵路信號系統軟件風險等級為基礎測試的必要性. 文獻[9]對CTCS-3系統安全軟件進行接口危險辨識,評估危險事件的風險等級,提出列控系統安全軟件黑盒測試的危險分析方法,但未對軟件測試建模理論進行研究. 文獻[10-12]針對鐵路信號系統的形式化描述和驗證,分別從時鐘約束、風險等級和安全約束等幾個方面提出鐵路信號系統的建模方法,但這些方法結構復雜,測試模型解析和測試案例搜索算法難以展開,不易直接應用于鐵路信號系統軟件測試建模.
目前,鐵路信號系統軟件測試的研究重點是如何以既有的測試建模方法為基礎生成覆蓋全面且高效的測試案例,研究提高了測試活動的自動化程度和測試效率. 但現有測試建模方法不能完整地描述軟件所有的行為特征,如UML狀態圖和CPN等方法不能描述軟件的時間約束,導致測試案例不能反映軟件的時間特性. TA能夠描述軟件的時間約束,但不具有層次結構,對復雜功能邏輯的描述能力較差,容易出現模型難以理解,甚至錯誤的問題. 同時,UML狀態圖、CPN和TA等方法均不能描述軟件測試模型中的風險特性.
本文通過分析鐵路信號軟件的領域特點,總結鐵路信號軟件測試的建模需求,結合Z規格說明語言(簡稱Z語言)提出風險時間狀態機建模方法,滿足鐵路信號軟件測試的建模需求.
鐵路信號系統軟件測試通常采用基于模型的測試(model-based testing,MBT)[13]理論,主要包括分析軟件需求、建立測試模型、生成測試案例和執行測試4個階段,如圖1所示. 首先,基于被測軟件的需求規格等文件對軟件功能和結構進行抽象,采用形式化建模方法建立軟件的測試模型;然后,依據測試模型,采用“平坦化”和狀態組合等方法對測試模型進行解析,通過廣度優先等搜索算法自動生成測試案例;最后,將測試案例加載到測試環境中執行測試,觀察測試結果.

圖1 鐵路信號系統軟件測試主要過程Fig. 1 Main testing process of railway signal system software
測試模型是編制測試案例和評判測試結果時的重要依據,直接關系到軟件測試過程的全面性和有效性,鐵路信號軟件測試建模方法需要盡可能系統、全面地描述鐵路信號系統軟件的所有需求.
鐵路信號系統軟件測試建模包括功能建模需求和性能建模需求兩個方面. 功能建模需求描述系統的功能邏輯(function logic),性能建模需求指與系統相關的性能約束或限制,包括時鐘約束(clock constraint)和風險等級(risk level)兩個方面.
1) 功能邏輯
隨著鐵路信號系統的規模越來越大,軟件承擔的功能越來越多、邏輯越來越復雜. 如CTCS-3級列控系統包括9種工作模式,14個主要運營場景,206個功能特征. 鐵路信號系統已構成一個復雜的控制系統,軟件存在著大量的并發、競爭、沖突等邏輯關系,控制狀態轉移條件復雜.
2) 時鐘約束
鐵路信號系統軟件運算結果的正確性不僅取決于系統邏輯處理的正確性,還取決于運算過程中的時鐘約束,要求軟件功能需要在指定時間內完成,或在規定時限之后才能發生. 如《CTCS-3級列控系統總體技術方案》[14]要求“當列車前端距分相區還有10秒走行距離時,車載設備向司機發出提示”. 鐵路信號系統軟件的時鐘約束通常為硬實時性(hard real-time)要求,如道岔轉換時間、移動授權有效時間、目視模式確認時間等,時鐘約束錯誤或缺失,可能造成重大安全事故.
3) 風險等級
鐵路信號系統軟件由安全功能(safety function)、安全相關功能(safety-related function)和非安全功能(non-safety function)組合構成. 如 《CTCS-3級列控系統測試案例(V3.0)》[15]的功能特征CTCS3-FT-71“由于超速觸發緊急制動”屬于安全功能,功能特征CTCS3-FT-116“記錄數據的下載”屬于非安全功能. 不同安全級別的功能對系統造成的安全影響差別較大,由風險等級進行描述. 風險等級的高低是鐵路信號系統軟件測試案例編制的重要基礎,對組織測試案例優先級及分析測試需求具有重要意義.
根據以上分析,鐵路信號系統軟件測試建模方法需要描述系統復雜的功能邏輯、時鐘約束和風險等級3個方面的特點,嚴密、準確地反應軟件測試需求,且具有良好的可讀性和可理解性.
為定義風險時間狀態機建模方法,首先介紹有限狀態機(finite state machine, FSM),然后在FSM基礎上,結合Z語言,在遷移元素中擴展出時鐘約束,在狀態元素中擴展出風險等級,最后給出風險時間狀態機的定義.
FSM采用可視化的方式描述系統的功能邏輯,具有清晰、直觀的優點,其是表示有限狀態以及狀態之間轉移和動作等行為的數學模型,具有精確性、可推導性和可驗證性,是基于模型的測試理論中的經典建模方法[13-16].
定義1一個有限狀態機M是一個六元組,如式(1)[17].

式中:
S為有限狀態集合;
s0為初始狀態,且s0∈S;
λ為狀態轉移函數,λ:S×I→S;
δ為輸出函數,δ :S×I→O;
I為有限輸入符號集合;
O為有限輸出符號集合.
圖2為一個FSM模型,包括s1和s2兩個狀態,其中s1為初始狀態,A、B、C為輸入,a、b、c為輸出.s1接收到輸入A時輸出a,轉移到s2狀態. 模型對應的六元組如下:


圖2 有限狀態機模型Fig. 2 Example of finite state machine
接下來結合Z語言,在FSM描述功能邏輯基礎上,增加層次結構,擴展出時鐘約束和風險等級兩個參數,提出風險時間狀態機(risk timed statechart,RTSC). 為描述方便,首先定義RTSC的基本元素,然后定義RTSC的層次結構,最后給出RTSC的形式化定義.
RTSC包括狀態、時鐘、信號表達式和遷移等基本元素.
1) 狀態
狀態是鐵路信號系統軟件在一定時期內的存在形式. 對RTSC的非空、有限狀態集合S,Z語言描述如下:

狀態包括簡單狀態(SIMPLE),或狀態(OR)和與狀態(AND)3種類型,Z語言描述如下:

OR狀態由同一層次的狀態和遷移組成,包含且僅包含一個初始狀態. 初始狀態無源狀態,且是任意狀態的源狀態. 多個并發的OR狀態組成AND狀態.
2) 時鐘
RTSC采用時鐘描述時間的流逝,有限時鐘集合記為X,Z語言描述如下:

對一個時鐘變量集合X,時間約束集合定義如式(2).

式中:σ1、σ2為時鐘約束;x∈X;g∈N ;∝∈{≤,<,≥,>,=}.
RTSC時鐘約束Σ的Z語言描述如下:

3) 信號
信號E具有產生和不產生兩種狀態,Z語言描述如下:

在某一時刻,正交組件產生的信號稱為動作.
4) 信號表達式
信號之間的與(and)關系、或(or)關系、非(not)關系構成信號表達式,記為ex如note表示未產生信號e.
用Π為表示信號永遠發生的常量.
5) 遷移
遷移是RTSC從源狀態轉移到目標狀態的方式,包括源狀態sc、時鐘約束σ、信號表達式ex、轉移時產生的信號e、重置的時鐘x及目標狀態st. 遷移的Z語言描述如下:

RTSC的狀態層次H包括底狀態γ、為狀態分配子狀態的有限狀態層次函數ω,定義狀態類型的有限狀態類型函數κ,定義狀態父狀態的ρ函數.H滿足以下性質:
1)ω為非SIMPLE類型的狀態分配子狀態;
2) 狀態之間的層次關系不能形成循環結構;
3)γ為OR狀態或AND狀態,是唯一沒有父狀態的狀態;
4) 任意非γ的狀態都具有唯一的父狀態,且均可以由γ通過ω傳遞到達.
H的Z模式定義如下:

其中:FS表示集合S的所有有限子集的集合;domω表示ω的定義域;ranρ表示ρ的值域;?si:domρ;sj: domω表示ρ定義域中的任意狀態si和ω定義域中的任意狀態sj,i,j為不為0的自然數,且i≠j.
RTSC由狀態層次和遷移集構成,采用風險等級函數η為SIMPLE狀態分配風險等級,滿足以下性質:
1)η僅為SIMPLE狀態分配風險等級;
2) OR狀態和AND狀態的風險等級為其包含的子狀態的風險等級的最大值.
3) 對任意遷移,只能有一個同層次的源狀態和目標狀態,源狀態和目標狀態可以是AND或SIMPLE狀態.
RTSC的Z模式定義如下:


其中:F1T表示集合T的所有非空有限子集的集合.
一個時鐘集合X的時鐘解釋v是指每個時鐘變量x到時間序列上的一個全映射. 某時刻,RTSC能夠同時處于最大的狀態集結合當前的時鐘解釋稱為格局(configuration),記為U. 在任意時刻,RTSC只有一個活動的格局,滿足以下規則:
1)U包含γ狀態;
2)U包含AND狀態s,則U包含s的每一個子狀態;
3)U包含OR狀態s,則U包含s的某一個子狀態;
4)U包含非γ的狀態s,則U包含s的父狀態;
5)U僅包含滿足規則1) ~ 4)的所有狀態.
格局公理描述如下:

其中:k表示不為0的自然數.
RTSC格 局 轉 移 過 程 記 為 (us,v(X),E),其 中us表示當前格局包含的狀態集,v(X)表示時鐘解釋,E表示轉移過程中產生的動作集,具體過程如下:
1) 激勵. 當RTSC接受到新的時鐘解釋或信號時開始格局轉移:(us,v(X),?)→(us,v′(X),e).
2) 計算. 格局轉移過程以SIMPLE狀態為基礎,從γ狀態,通過OR狀態和AND狀態向下分解,包括以下2個規則:
規則1AND狀態并行地計算其所包含的OR狀態的轉移.
規則2OR狀態計算當前激活的SIMPLE狀態的變遷t上的信號,產生t上的動作,重置t的時鐘,離開變遷源狀態τ.sc到達變遷狀態t.st,滿足:us=us .sc∪t.st,G=G∪t.e,v(t.x)=0.
3) 結束. RTSC根據狀態類型迭代相應規則直至轉移穩定,保留時鐘解釋,清空轉移期間的信號.
RTSC從初始格局開始,根據產生的信號或時鐘的更新激活格局轉移過程;依據層次結構,迭代AND狀態和OR狀態的規則,直到計算出下一組穩定的狀態. 格局轉移時,遷移的觸發信號均發生,且時鐘解釋滿足遷移上的時鐘約束,同時產生遷移上的動作,重置遷移上的時鐘變量.
RTSC的語義可以由其對應的時間標記遷移系統(timed transition system,TTS)進行定義.
定義2一個時間標記遷移系統TTS是一個4元組:

式中:L為狀態集合;
l0為初始狀態,l0∈L;
→?L×(Σ∪R)×L為轉移關系,且滿足:1) 如果,則l=l′; 2) 如果,且,d,d′∈R,則; 3) 如果則0 ≤d′≤d,則有l′′∈L,滿足且
在時鐘解釋v下,如果時鐘約束σ為真,則稱時鐘解釋v滿足時鐘約束σ,記為v|=σ.
定義3對任意RTSC,其語義可以通過時間標記遷移系統 Ω=(L,l0,→,Σ)進行定義,其中:

l0=(us0,v0) ,us0為RTSC的初始狀態集,且對任意x∈X,v0(x)=0;
轉 移 關 系 → 滿 足:1) 對 (us,v)和 一 個 遷 移且v|=σ ,則對和時間增量
RTSC從初始格局開始,通過動作轉移或時延轉移實現格局變化.
1) 動作轉移. 當前激活的信號和時鐘解釋滿足變遷的信號表達式和時鐘約束,觸發動作遷移,激活變遷上的動作,重置變遷時鐘為0.
2) 時延轉移. 時延轉移保持格局狀態不變,對所有時鐘增加相同的時間增量.
計算機聯鎖系統是鐵路信號系統中典型的安全關鍵系統. 以計算機聯鎖系統的道岔定位選排子系統為例建立RTSC測試模型,解釋RTSC的格局轉移機制.
道岔定位選排子系統根據道岔操作命令或進路請求,檢查道岔當前是否處于定位. 當道岔狀態與期望不一致時,選排道岔到需求位置[18]. 該系統涉及11個信號,主要信號名稱及其含義見表1.

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

圖3 道岔子系統RTSC模型Fig. 3 RTSC model of switch subsystem
DRTSC中:遷移的表現形式為[e] [σ] / [a] [x];e為觸發轉移的信號;σ為時鐘約束;a為轉移時產生的動作;x為重置的時鐘,記為. 如表示狀態s14激活時,當檢測到信號e7,并滿足時間約束x1<13,DRTSC遷移到s13,同時產生信號e8,并重置時鐘x1.
DRTSC模型中,s3、s4、s5分別表示道岔轉換的“安全請求”,“道岔轉換”和轉換的“時鐘約束”狀態.DRTSC主要描述以下過程:
道岔“安全請求”狀態檢測到定位需求后,在道岔未鎖閉、無反位請求、未處于定位時,進一步檢查道岔轉換狀態,未處于轉換過程中或轉換超時時,判定定位請求安全. “道岔轉換”狀態接受到“定位請求”信號后,如果道岔未鎖閉則重置時鐘x1;條件保持1 s后,請求道岔轉換. “時鐘約束”狀態接受道岔轉換動作后,重置時鐘x1并開始計時,13 s內檢測到道岔轉換到定位則轉換成功,否則轉換超時. 當“道岔轉換”狀態接受到“時鐘約束”狀態的“轉換成功”信號后判定道岔轉換成功. 當同時處于“定位請求”和“轉換成功”狀態時,判定“選排一致”. 轉換過程中任意時刻,道岔子系統接受到反位請求信號立即重置時鐘,返回初始狀態.
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狀態,根據規則 2,s0當前激活狀態為s2.s2為AND狀態,根據規則 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信號觸發s4的子狀態s11,并轉移到狀態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的狀態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格局轉移過程記為表示道岔在處于“定位安全請求”,“道岔轉換”,“道岔轉換計時中”狀態時,檢測到道岔在第3 s轉移到定位,判定道岔選排一致.
DRTSC描述了道岔定位轉移過程中的功能邏輯、時鐘約束和風險等級.
5.3.1 測試需求覆蓋
1) 功能邏輯
DRTSC采用16個狀態,19條遷移和11個信號描述道岔轉換過程的功能邏輯.
2) 時鐘約束
DRTSC通過時鐘x1描述道岔轉換過程中信號保持時間1 s和轉換超時判斷時間13 s,包括時鐘約束x1>1,x1<13和x1≥ 13. 如描述道岔轉換超過13 s后進入超時狀態s15.
3) 風險等級
DRTSC描述了道岔轉換過程中風險等級的變化情況,包括風險等級升高、降低以及保持不變,風險轉移矩陣如圖4所示. 其中,正數表示風險等級升高,負數表示風險等級降低,0表示風險等級不變,“?”表示狀態之間無轉移關系.

圖4 道岔子系統風險矩陣Fig. 4 Risk matrix of switch subsystem
如R78= 1描 述 了 遷 移(s8,4),表示道岔由SIL 3的狀態s7轉移到SIL 4的s8,風險等級升高1個等級,軟件測試時需要重點對此類變遷進行測試.
5.3.2 與TA對比
為檢測RTSC模型的描述能力,選取鐵路信號系統軟件測試中廣泛采用的TA建模方法進行對比.道岔定位選排的TA模型如圖5所示,記為DTA.DTA由4個TA構件組成TA網絡實現道岔定位選排的測試需求,其中,為描述DRTSC的否定信號,如未接收到信號e5,在DTA中增加en5.DTA和DRTSC均包括1個時鐘,狀態、變遷和信號數量方面的比較如表2所示,DRTSC比DTA節省62%的變遷數,節省54%的狀態數. 其中,DRTSC的狀態數為除去層次結構后的SIMPLE狀態的數量.

圖5 道岔子系統TA模型Fig. 5 TA model of switch subsystem
進一步,隨機選取計算機聯鎖系統軟件中的4個子功能,分別采用RTSC和TA進行建模,RTSC模型和TA模型在構件、狀態和變遷3個方面的對比如圖6所示.

圖6 RTSC模型與TA模型對比Fig. 6 Comparison between RTSC model and TA model
通過表2和圖6,相對TA建模方法,RTSC模型具有更少的構件數、狀態數、變遷數和信號數. 且隨著功能邏輯復雜度的增加,RTSC節省的狀態數和變遷數越多,RTSC模型更為簡潔、清晰,表達能力更強,可讀性更高,適合描述鐵路信號系統軟件復雜的功能邏輯.

表2 DRTSC與DTA 對比Tab. 2 Comparison betweenDRTSC andDTA
RTSC繼承了FSM可視化、直觀和簡介的特點,其狀態轉移、層次性和并發性能夠描述軟件的功能邏輯,時鐘約束能夠描述軟件的時間關系,風險等級能夠描述軟件不同功能之間的安全性關系. 具體的,RTSC與鐵路信號系統軟件測試建模需求之間的關系如表3所示.

表3 RTSC與測試需求的關系Tab. 3 Relationship between RTSC and test requirements
1) 鐵路信號系統軟件測試建模方法不能很好地描述鐵路信號系統軟件測試的建模需求,不能同時描述軟件的功能邏輯、時鐘約束和風險等級3個方面的特征.
2) 以有限狀態機理論為基礎,擴展出時鐘約束和風險等級屬性,提出風險時間狀態機建模方法,采用Z語言給出了風險時間狀態機的定義,闡述了風險時間狀態機的格局轉移規則,滿足鐵路信號系統軟件測試在功能邏輯、時鐘約束和風險等級方面的建模需求.
3) 以計算機聯鎖系統中的道岔子系統為例,利用風險時間狀態機建立了道岔子系統軟件的測試模型,并選取TA建模方法進行對比,結果表明風險時間狀態機描述能力更強.
4) 文章提出的方法已在計算機聯鎖系統的軟件測試中得到應用,實踐表明該方法能夠滿足鐵路信號系統軟件測試的建模需求,為鐵路信號系統軟件測試提供了形式化建模的理論基礎.