李 耀 ,張曉霞 ,郭 進(jìn) ,張亞?wèn)|
(1.電子科技大學(xué)光電科學(xué)與工程學(xué)院, 四川 成都 611731;2.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院, 四川 成都611756)
我國(guó)高鐵運(yùn)營(yíng)里程已經(jīng)超過(guò)2.9萬(wàn)公里,占世界高鐵運(yùn)營(yíng)里程的2/3以上,累計(jì)運(yùn)輸旅客超過(guò)100億人次.我國(guó)已成為世界上高鐵運(yùn)營(yíng)里程最長(zhǎng)、運(yùn)輸密度最高、運(yùn)營(yíng)場(chǎng)景最復(fù)雜的國(guó)家.高鐵信號(hào)系統(tǒng)具有SIL4級(jí)的安全需求,安全關(guān)鍵功能一旦失效可能造成列車(chē)追尾、脫軌等行車(chē)事故,導(dǎo)致人員傷亡及重大財(cái)產(chǎn)損失[1].保證高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的安全性對(duì)我國(guó)高鐵的安全運(yùn)營(yíng)、國(guó)家“高鐵走出去”具有重要意義.
基于模型的測(cè)試是目前高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能安全性測(cè)試的研究熱點(diǎn),常用的測(cè)試建模方法包括時(shí)間自動(dòng)機(jī)(timed automata,TA)、UML Statechart和 Petri網(wǎng)(Petri net)等,研究?jī)?nèi)容重點(diǎn)關(guān)注如何從安全關(guān)鍵功能的測(cè)試模型生成覆蓋全面且高效的測(cè)試用例.文獻(xiàn)[2]針對(duì) ATP (automatic train protection)系統(tǒng)模式轉(zhuǎn)換功能測(cè)試用例難以實(shí)現(xiàn)全覆蓋的問(wèn)題,采用TA建模方法建立測(cè)試模型,提出滿足全狀態(tài)和全變遷覆蓋準(zhǔn)則的測(cè)試用例生成方法,提高測(cè)試用例的生成效率和重用性.文獻(xiàn)[3]以RBC (radio block center)切換功能為例,提出基于 TA和 HCSP (hybrid communication sequential process)的測(cè)試建模方法,研究全狀態(tài)和全變遷覆蓋的測(cè)試用例自動(dòng)生成方法,列控系統(tǒng)測(cè)試用例的生成效率提高30%.文獻(xiàn)[4]以TA作為測(cè)試建模的基礎(chǔ)理論,通過(guò)在測(cè)試模型中注入故障的方式提高測(cè)試用例的全面性.文獻(xiàn)[5]基于TA建模理論,提出輸入輸出時(shí)間自動(dòng)機(jī)(timed automata with input and output,TAIO)建模方法,提出基于TAIO變異分析的列控系統(tǒng)安全關(guān)鍵功能測(cè)試框架.文獻(xiàn)[6]以有色Petri網(wǎng)(colored Petri net,CPN)作為測(cè)試建模的理論基礎(chǔ),通過(guò)狀態(tài)空間搜索自動(dòng)生成車(chē)地通信功能的測(cè)試用例,提高測(cè)試用例生成的自動(dòng)化程度.文獻(xiàn)[7]針對(duì)ATP系統(tǒng)模式轉(zhuǎn)換功能,建立CPN測(cè)試模型,解決狀態(tài)空間爆炸和搜索死循環(huán)的問(wèn)題,生成滿足全路徑覆蓋準(zhǔn)則的測(cè)試序列集.文獻(xiàn)[8]針對(duì)列控中心軌道電路編碼功能,研究UML Statechart測(cè)試建模方法,提出圖覆蓋、組合覆蓋和文法分析相結(jié)合的方式自動(dòng)生成測(cè)試用例.文獻(xiàn)[9]針對(duì)列控中心改變運(yùn)動(dòng)方向功能,建立UML Statechart測(cè)試模型,研究基于UML Statechart模型自動(dòng)生成覆蓋全面的測(cè)試用例的算法,為自動(dòng)化測(cè)試提供基礎(chǔ).
目前的研究豐富了高鐵信號(hào)系統(tǒng)的測(cè)試用例,提高了測(cè)試活動(dòng)的自動(dòng)化程度和測(cè)試效率,但對(duì)高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能測(cè)試建模理論的研究相對(duì)較少.目前主要采用的測(cè)試建模方法沒(méi)有很好地針對(duì)高鐵信號(hào)系統(tǒng)功能邏輯和時(shí)鐘約束的特點(diǎn),導(dǎo)致測(cè)試模型復(fù)雜,測(cè)試用例缺少時(shí)鐘約束.首先,詳細(xì)分析高鐵信號(hào)系統(tǒng)測(cè)試模型的建模需求;然后,在有限狀態(tài)機(jī)理論的基礎(chǔ)上從功能邏輯和時(shí)鐘約束2個(gè)方面提出時(shí)間狀態(tài)機(jī)建模方法;最后,以計(jì)算機(jī)聯(lián)鎖道岔子系統(tǒng)為例進(jìn)行了分析,為基于模型的高鐵信號(hào)系統(tǒng)測(cè)試提供新的建模理論.
基于模型的測(cè)試(model-based testing,MBT)[10]理論是高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能測(cè)試用例生成的研究重點(diǎn)內(nèi)容之一.MBT屬于基于規(guī)范的測(cè)試范疇,其編制測(cè)試用例和評(píng)判測(cè)試結(jié)果時(shí)均以被測(cè)系統(tǒng)(system under test,SUT)的測(cè)試模型作為依據(jù).MBT已經(jīng)在高鐵信號(hào)系統(tǒng)RBC、ATP和CBI (computer based interlocking)等設(shè)備的安全關(guān)鍵功能測(cè)試中得到重點(diǎn)研究[11-14].實(shí)踐表明,該方法能夠有效地發(fā)現(xiàn)系統(tǒng)問(wèn)題,提高測(cè)試效率和自動(dòng)化程度.
基于模型的測(cè)試主要包括分析被測(cè)系統(tǒng)需求、建立測(cè)試模型、生成抽象測(cè)試用例、具體化抽象測(cè)試用例、執(zhí)行測(cè)試和分析測(cè)試結(jié)果6個(gè)階段.首先,基于被測(cè)系統(tǒng)的需求規(guī)格等文件對(duì)系統(tǒng)功能和結(jié)構(gòu)進(jìn)行抽象,建立系統(tǒng)的測(cè)試模型;其次,依據(jù)測(cè)試模型,選取測(cè)試覆蓋準(zhǔn)則自動(dòng)生成抽象測(cè)試用例;然后,結(jié)合行業(yè)知識(shí)將抽象測(cè)試用例實(shí)例化為可執(zhí)行的測(cè)試用例;最后,將測(cè)試用例加載到測(cè)試環(huán)境中執(zhí)行測(cè)試,觀察、分析測(cè)試結(jié)果.
測(cè)試模型是高鐵信號(hào)系統(tǒng)測(cè)試用例編制的基礎(chǔ).目前,高鐵信號(hào)系統(tǒng)的測(cè)試建模方法不是針對(duì)信號(hào)系統(tǒng)安全關(guān)鍵功能測(cè)試的領(lǐng)域建模方法,不能很好、完整地描述高鐵信號(hào)系統(tǒng)的行為特征.模典型的高鐵信號(hào)系統(tǒng)測(cè)試建方法包括有限狀態(tài)機(jī)(finite state machine, FSM)、UML Statechart、TA 和 Petri網(wǎng)等,其中,F(xiàn)SM、UML Statechart和 Petri網(wǎng)等方法不具有描述時(shí)鐘約束的能力,導(dǎo)致該模型生成的測(cè)試用例不能反映系統(tǒng)的時(shí)間特性,不能滿足測(cè)試活動(dòng)的全面性和完備性要求.TA能夠描述系統(tǒng)的時(shí)鐘約束,但不具有層次結(jié)構(gòu),對(duì)復(fù)雜功能邏輯的描述能力較差,不易描述高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的全部行為,容易出現(xiàn)狀態(tài)數(shù)量爆炸、測(cè)試模型難以理解、甚至錯(cuò)誤的問(wèn)題.
在安全關(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ù)雜邏輯和時(shí)鐘約束的形式化描述和驗(yàn)證問(wèn)題.但針對(duì)高鐵信號(hào)系統(tǒng)測(cè)試,這些建模方法的語(yǔ)法、語(yǔ)義復(fù)雜,測(cè)試模型解析和測(cè)試用例生成難度較大,不易直接應(yīng)用在高鐵信號(hào)系統(tǒng)的測(cè)試活動(dòng)中.因此,研究適合于高鐵信號(hào)系統(tǒng)測(cè)試領(lǐng)域的形式化建模方法對(duì)高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的測(cè)試具有一定的意義.
測(cè)試模型作為高鐵信號(hào)系統(tǒng)測(cè)試?yán)碚摰闹匾A(chǔ),需要盡可能全面、清晰地呈現(xiàn)被測(cè)系統(tǒng)的行為特性.本節(jié)針對(duì)高鐵信號(hào)系統(tǒng)的特點(diǎn),分析高鐵信號(hào)系統(tǒng)測(cè)試活動(dòng)的測(cè)試建模需求.
根據(jù)高鐵信號(hào)系統(tǒng)測(cè)試活動(dòng)的過(guò)程和目標(biāo),高鐵信號(hào)系統(tǒng)測(cè)試建模包括功能建模需求和性能建模需求兩個(gè)方面.功能建模需求描述系統(tǒng)的功能邏輯(function logic),明確系統(tǒng)需要滿足的安全條件;性能建模需求指與系統(tǒng)功能相關(guān)的時(shí)鐘約束或限制(clock constraint).
1)功能邏輯
隨著計(jì)算機(jī)和通信技術(shù)的發(fā)展,高鐵信號(hào)系統(tǒng)承擔(dān)的安全功能越來(lái)越多,功能邏輯越來(lái)越復(fù)雜.如CTCS-3級(jí)列控系統(tǒng)包括9種工作模式,14個(gè)主要運(yùn)營(yíng)場(chǎng)景,206個(gè)功能特征[21].高鐵信號(hào)系統(tǒng)已構(gòu)成一個(gè)復(fù)雜的控制系統(tǒng),存在著大量的并發(fā)、競(jìng)爭(zhēng)和沖突等邏輯關(guān)系,控制狀態(tài)轉(zhuǎn)移條件復(fù)雜.高鐵信號(hào)系統(tǒng)測(cè)試模型需要滿足功能邏輯的復(fù)雜性和并發(fā)性,嚴(yán)密、準(zhǔn)確地反應(yīng)系統(tǒng)的功能需求,且具有良好的可讀性和可理解性.
2)時(shí)鐘約束
高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能運(yùn)算結(jié)果的安全性和正確性不僅取決于系統(tǒng)邏輯的處理過(guò)程,還取決于運(yùn)算過(guò)程中的時(shí)鐘約束,屬于典型的實(shí)時(shí)系統(tǒng)(real-time system).高鐵信號(hào)系統(tǒng)的時(shí)鐘約束主要指系統(tǒng)功能需要在指定的時(shí)間內(nèi)完成,或在規(guī)定的時(shí)限之后才能發(fā)生.如《CTCS-3級(jí)列控系統(tǒng)測(cè)試案例(V3.0)》[21]功能特征190的測(cè)試用例3要求“司機(jī)未在5秒內(nèi)進(jìn)行確認(rèn),實(shí)施最大常用制動(dòng)”.而且,安全關(guān)鍵功能的時(shí)鐘約束通常為硬實(shí)時(shí)性要求,如道岔轉(zhuǎn)換時(shí)間、RBC交互時(shí)間、MA (movement authority)有效時(shí)間等[22],時(shí)鐘約束錯(cuò)誤或缺失,可能造成重大安全事故.
根據(jù)以上分析,高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的測(cè)試建模方法需要能夠很好地描述系統(tǒng)復(fù)雜的功能邏輯和時(shí)鐘約束.
有限狀態(tài)機(jī)(finite state machine, FSM)是 MBT理論中經(jīng)典的測(cè)試建模方法[23-24],其通過(guò)可視化的方式描述系統(tǒng)的功能邏輯,具有清晰、直觀的優(yōu)點(diǎn).本節(jié)在FSM的基礎(chǔ)上擴(kuò)展出時(shí)間狀態(tài)機(jī)建模方法,首先介紹FSM的定義,然后在FSM的遷移中擴(kuò)展出時(shí)鐘約束,結(jié)合Z規(guī)格說(shuō)明語(yǔ)言給出時(shí)間狀態(tài)機(jī)的定義.
FSM是表示有限狀態(tài)以及狀態(tài)之間轉(zhuǎn)移和動(dòng)作等行為的數(shù)學(xué)模型,具有精確性、可推導(dǎo)性和可驗(yàn)證性.
定義1(有限狀態(tài)機(jī))一個(gè)有限狀態(tài)機(jī)M是個(gè)六元組,如式(1)[24].
式中:S為有限狀態(tài)集合;s0為初始狀態(tài),s0∈S;λ為狀態(tài)轉(zhuǎn)移函數(shù), λ :SI→S;δ為輸出函數(shù), δ:SI→O;I為有限輸入符號(hào)集合;O為有限輸出符號(hào)集合.
圖1為一個(gè)開(kāi)關(guān)的FSM模型.
圖1 有限狀態(tài)機(jī)示例Fig.1 Example of finite state machine
圖1 中包括關(guān)(soff)和開(kāi)(son)兩個(gè)狀態(tài),其中soff為初始狀態(tài).soff接收到輸入A時(shí)轉(zhuǎn)移到son狀態(tài),輸出A′,son接收到輸入B時(shí)轉(zhuǎn)移到soff狀態(tài),輸出B′.模型對(duì)應(yīng)的六元組如式(2).
根據(jù)FSM的定義,F(xiàn)SM缺少描述時(shí)鐘約束的機(jī)制.接下來(lái)結(jié)合Z規(guī)格說(shuō)明語(yǔ)言,在FSM描述功能邏輯的基礎(chǔ)上,增加層次結(jié)構(gòu),擴(kuò)展出時(shí)鐘約束,提出時(shí)間狀態(tài)機(jī)(timed finite state machine,TFSM).
TFSM包括時(shí)鐘、信號(hào)和狀態(tài)等基本元素.
1)時(shí)鐘
TFSM采用時(shí)鐘描述時(shí)間的流逝,有限時(shí)鐘集合記為C,Z語(yǔ)言描述如下:
TFSM時(shí)鐘約束集合記為Ψ,Z語(yǔ)言描述如下:
對(duì)一個(gè)時(shí)鐘變量集合C,Ψ具有如下形式:
式 中 : ψ1、 ψ2為 時(shí) 鐘 約 束 ;x∈C;d∈N ; ∝∈{≤,<,≥,>,=}.
2)信號(hào)
信號(hào)具有產(chǎn)生和不產(chǎn)生兩種狀態(tài),Z語(yǔ)言描述如下:
TFSM在某一時(shí)刻,其他正交組件產(chǎn)生的信號(hào)稱為動(dòng)作.
3)狀態(tài)
狀態(tài)是高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能在一定時(shí)期內(nèi)的存在形式.TFSM的非空、有限狀態(tài)集合記為S,Z語(yǔ)言描述如下:
狀態(tài)類(lèi)型包括簡(jiǎn)單狀態(tài)(PRIM),或狀態(tài)(OR)和與狀態(tài)(AND)3種,Z語(yǔ)言描述如下:
P::= PRIM | OR | AND
4)遷移
遷移T是TFSM從源狀態(tài)轉(zhuǎn)移到目標(biāo)狀態(tài)的方式,包括源狀態(tài)sc、信號(hào)g、時(shí)鐘約束ψ、轉(zhuǎn)移時(shí)產(chǎn)生的動(dòng)作a、重置的時(shí)鐘c及目標(biāo)狀態(tài)st.遷移的Z語(yǔ)言描述如下:
OR狀態(tài)由同層次的狀態(tài)和遷移組成,包含且僅包含一個(gè)初始狀態(tài),初始狀態(tài)為無(wú)源狀態(tài),且是任意狀態(tài)的源狀態(tài).多個(gè)并發(fā)的OR狀態(tài)組成AND狀態(tài).
本小節(jié)在TFSM基本元素的基礎(chǔ)上,采用Z規(guī)格說(shuō)明語(yǔ)言定義TFSM的層次結(jié)構(gòu),給出TFSM的定義.
TFSM的狀態(tài)層次Π包括底狀態(tài)γ、為狀態(tài)分配子狀態(tài)的有限狀態(tài)層次函數(shù)h,定義狀態(tài)類(lèi)型的有限狀態(tài)類(lèi)型函數(shù)ε,定義狀態(tài)父狀態(tài)的函數(shù)d,滿足以下性質(zhì):
1)h為非PRIM類(lèi)型的狀態(tài)分配子狀態(tài),且狀態(tài)層次不能形成循環(huán)結(jié)構(gòu);
2)γ不為PRIM狀態(tài),是唯一沒(méi)有父狀態(tài)的狀態(tài);
3)任意非γ的狀態(tài)都具有唯一的父狀態(tài),且均可以由γ通過(guò)h傳遞到達(dá).
Π的Z模式定義如下,其中: FS表示集合S的所有有限子集的集合,domh表示h的定義域,ranh表示h的值域.
TFSM由狀態(tài)層次π和遷移集ts構(gòu)成.對(duì)任意遷移,僅有一個(gè)同層次的源狀態(tài)和目標(biāo)狀態(tài).源狀態(tài)和目標(biāo)狀態(tài)可以是AND或PRIM狀態(tài).Z模式定義如下,其中: F1T表示集合T的所有非空有限子集的集合.
一個(gè)時(shí)鐘集合C的時(shí)鐘解釋v是指每個(gè)時(shí)鐘變量c到時(shí)間序列上的一個(gè)全映射.某時(shí)刻,TFSM能夠同時(shí)處于的最大的狀態(tài)集結(jié)合當(dāng)前的時(shí)鐘解釋稱為格局(configuration),記為u,格局對(duì)應(yīng)的狀態(tài)集記為u′,初始格局記為u0,初始格局對(duì)應(yīng)的狀態(tài)集記為.在任意時(shí)刻,TFSM只有一個(gè)活動(dòng)的格局,滿足以下規(guī)則:
1)u′包含γ狀態(tài);
2)u′包含 AND 狀態(tài)s,則u′包含s的每個(gè)子狀態(tài);
3)u′包含 OR 狀態(tài)s,則u′包含s的某個(gè)子狀態(tài);
4)u′包含非γ的狀態(tài)s,則u′包含s的父狀態(tài).
TFSM格局的公理描述如下:
本節(jié)給出基于TFSM自動(dòng)生成測(cè)試用例的方法.目前,針對(duì)TA和Petri網(wǎng)等測(cè)試模型,研究學(xué)者已經(jīng)提出了許多相對(duì)成熟的測(cè)試用例自動(dòng)生成算法.由于TA能夠同時(shí)描述功能邏輯和時(shí)鐘約束,本節(jié)將TFSM等價(jià)轉(zhuǎn)換為T(mén)A,利用基于TA的測(cè)試用例生成算法自動(dòng)生成TFSM的測(cè)試用例.
定義2(時(shí)間自動(dòng)機(jī))一個(gè)時(shí)間自動(dòng)機(jī)TA是一個(gè)六元組 (L,l0,Σ,X,M,E) ,其中:L為有限位置集合;l0∈L為初始位置; Σ 為有限字符集合;X為有限時(shí)鐘集合;M為將位置映射到時(shí)鐘約束的映射;E為轉(zhuǎn)移的集合,E?LΣ ×2xΦ(X)L, Φ (X) 為時(shí)鐘約束集合.
定義3(TFSM測(cè)試用例)對(duì)任意TFSM,如果從格局ui能夠到達(dá)格局uj,i,j≥0,則 TFSM中ui和uj之間存在一條路徑,稱該路徑為T(mén)FSM中以u(píng)i和uj為測(cè)試需求的測(cè)試用例.
定義4(TA測(cè)試用例)對(duì)任意TA,如果從位置li沿TA中的邊能夠到達(dá)lj,i,j≥0,則 TA中l(wèi)i和lj之間存在一條路徑,稱該路徑為T(mén)A中以li和lj節(jié)點(diǎn)為測(cè)試需求的測(cè)試用例.
定理 1設(shè) κ 為一個(gè) TFSM向一個(gè)六元組(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) 是一個(gè)與TFSM具有相同測(cè)試用例集的TA.
證明根據(jù) κ 的定義,TFSM的格局狀態(tài)集對(duì)應(yīng)TA的位置集,TFSM的初始格局狀態(tài)對(duì)應(yīng)TA的初始位置,TFSM的信號(hào)集和時(shí)鐘集分別對(duì)應(yīng)為T(mén)A的有限字符集和時(shí)鐘集,即 κ 將TFSM映射為一個(gè)所有位置均無(wú)時(shí)鐘約束的TA.對(duì)任意TA,?l1,l2∈L, (l1,l2)∈E,則TFSM 中 ?u1,u2∈u′,u1=l1,u2=l2.根據(jù) κ 的定義有u1→u2.故 TA 中的任意測(cè)試 用 例l0,l1,··· 對(duì) 應(yīng) TFSM中 的 一 條 測(cè) 試 用 例u0,u1,···.
由定理1,TFSM的測(cè)試用例與TA的測(cè)試用例一一對(duì)應(yīng),如圖2所示.
圖2 TFSM 與 TA 的測(cè)試用例的關(guān)系Fig.2 Relationship of test cases between TFSM and TA
根據(jù)以上分析,基于TFSM的高鐵信號(hào)系統(tǒng)測(cè)試用例生成的主要過(guò)程如下:首先,測(cè)試人員采用TFSM建模方法建立高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的測(cè)試模型;然后,根據(jù)TFSM和TA測(cè)試用例集之間的一致性,將TFSM模型轉(zhuǎn)化為T(mén)A模型,利用基于TA的高鐵信號(hào)系統(tǒng)測(cè)試?yán)碚?,?duì)TA模型編制測(cè)試用例;最后,將測(cè)試用例加載到測(cè)試環(huán)境中進(jìn)行測(cè)試,分析測(cè)試結(jié)果.
計(jì)算機(jī)聯(lián)鎖系統(tǒng)是高鐵信號(hào)系統(tǒng)中典型的安全關(guān)鍵系統(tǒng),具有SIL4的安全完整性要求.本節(jié)以計(jì)算機(jī)聯(lián)鎖系統(tǒng)中的道岔定位選排子系統(tǒng)為例建立TFSM測(cè)試模型,并轉(zhuǎn)換為T(mén)A模型編制測(cè)試用例.
道岔定位選排子系統(tǒng)根據(jù)道岔操作命令或進(jìn)路請(qǐng)求,檢查道岔當(dāng)前是否處于定位.當(dāng)?shù)啦頎顟B(tài)與期望不一致時(shí),選排道岔到需求位置.該系統(tǒng)涉及11個(gè)信號(hào),信號(hào)名稱及其含義如表1所示.
表1 道岔子系統(tǒng)信號(hào)的含義Tab.1 Meaning of signals in the switch subsystem
道岔定位選排子系統(tǒng)的TFSM測(cè)試模型記為DTFSM_SW,如圖3所示.
圖3 道岔定位選排測(cè)試模型Fig.3 Testing model of switch subsystem
DTFSM_SW包括1個(gè)時(shí)鐘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}.
DTFSM_SW通過(guò)11個(gè)狀態(tài)、15條遷移和11個(gè)信號(hào)描述道岔轉(zhuǎn)換過(guò)程的功能邏輯,通過(guò)時(shí)鐘約束x>1、x< 13 和x≥ 13 描述道岔轉(zhuǎn)換過(guò)程中的信號(hào)保持時(shí)間1 s和轉(zhuǎn)換超時(shí)時(shí)間13 s的時(shí)鐘約束,為測(cè)試用例生成提供了模型基礎(chǔ).
DTFSM_SW等價(jià)的TA模型DTA_SW如圖4所示.DTA_SW包括37條邊和9個(gè)節(jié)點(diǎn),為描述方便,DTA_SW的狀態(tài)名僅包括DTFSM_SW格局中的PRIM狀態(tài).
圖4 DTFSM_SW 等價(jià)的 TA 模型 DTA_SWFig.4 TA model DTA_SW equivalent to DTFSM_SW
DTA_SW的測(cè)試用例即為道岔定位選排子系統(tǒng)DTFSM_SW的測(cè)試用例.為檢測(cè)TFSM編制測(cè)試用例的效果,本節(jié)基于文獻(xiàn)[14]提出的基于模型的測(cè)試用例生成方法,以s4為測(cè)試模型的開(kāi)始節(jié)點(diǎn)和終止節(jié)點(diǎn)編制測(cè)試用例.高鐵信號(hào)系統(tǒng)測(cè)試模型典型的測(cè)試覆蓋準(zhǔn)則包括節(jié)點(diǎn)覆蓋(node coverage,NC)、邊覆蓋(edge coverage,EC)、邊對(duì)覆蓋(edge-pair coverage,EPC)、完全路徑覆蓋(complete path coverage,CPC)、主路徑覆蓋(prime path coverage,PPC)和特定路徑覆蓋(specified path coverage,SPC)等.本節(jié)以NC、EC、EPC和CPC覆蓋準(zhǔn)則為例,生成的測(cè)試用例如表2所示,其中用例總數(shù)表示DTFSM_SW的測(cè)試用例數(shù)量,時(shí)鐘約束用例數(shù)表示DTFSM_SW中測(cè)試時(shí)鐘約束的用例數(shù)量.
表2 DTFSM_SW測(cè)試用例統(tǒng)計(jì)Tab.2 Test case statistics of DTFSM_SW
為檢驗(yàn)TFSM的建模能力,對(duì)道岔定位選排的TFSM模型與TA模型進(jìn)行對(duì)比,如表3所示,其中,DTFSM_SW的狀態(tài)數(shù)為除去表示層次的OR狀態(tài)后的狀態(tài)數(shù)量.
由表3可知,DTFSM_SW與DTA_SW具有相同的狀態(tài)數(shù)和信號(hào)數(shù),但DTA_SW的變遷數(shù)超過(guò)DTFSM_SW的2倍,導(dǎo)致模型更為復(fù)雜.且隨著高鐵信號(hào)系統(tǒng)功能邏輯復(fù)雜度的增加,TA模型的變遷數(shù)急劇增加,模型的可讀性下降,容易導(dǎo)致模型錯(cuò)誤.與TA相比,TFSM更加直觀、清晰,可讀性良好,更適合描述高鐵信號(hào)系統(tǒng)復(fù)雜的功能邏輯.
表3 DTFSM_SW與DTA_SW對(duì)比Tab.3 Comparison of DTFSM_SW and DTA_SW
為檢驗(yàn)TFSM在編制測(cè)試用例方面的有效性,選擇高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能中廣泛采用的Petri網(wǎng)和UML Statechart建模方法對(duì)道岔定位選排子系統(tǒng)進(jìn)行建模,以CPC覆蓋準(zhǔn)則為例編制測(cè)試用例,對(duì)比結(jié)果如表4所示.
由表4可知,TFSM、Petri網(wǎng)和 UML Statechart建模方法在功能邏輯方面生成的測(cè)試用例數(shù)相同,但TFSM比Petri網(wǎng)和UML Statechart多生成了16條具有時(shí)鐘約束的測(cè)試用例,如表5所示.
表4 不同建模方法生成的測(cè)試用例對(duì)比Tab.4 Comparison of test cases generated by different modeling methods
表5 DTFSM_SW具有時(shí)鐘約束的測(cè)試案例Tab.5 Test cases with clock constraints of DTFSM_SW
根據(jù)以上分析,TFSM建模方法適合描述高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能復(fù)雜的邏輯,并生成全面的覆蓋功能邏輯和時(shí)鐘約束的測(cè)試用例,能夠滿足高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能在功能邏輯和時(shí)鐘約束方面的測(cè)試建模需求.
1)高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能的測(cè)試建模方法不能很好地描述系統(tǒng)特征,不具有描述時(shí)鐘約束的能力,或難以描述安全關(guān)鍵功能邏輯的復(fù)雜性.
2)本文提出的時(shí)間狀態(tài)機(jī)建模方法以有限狀態(tài)機(jī)理論為基礎(chǔ),具有嚴(yán)格的形式化定義,能夠等價(jià)轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)結(jié)構(gòu).
3)通過(guò)道岔子系統(tǒng)的案例分析,時(shí)間狀態(tài)機(jī)能夠滿足高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能在功能邏輯和時(shí)鐘約束方面的測(cè)試建模需求,為高鐵信號(hào)系統(tǒng)測(cè)試提供了形式化建模的理論基礎(chǔ).
4)本文提出的方法已在高鐵信號(hào)系統(tǒng)的計(jì)算機(jī)聯(lián)鎖和ATP設(shè)備的系統(tǒng)測(cè)試中得到應(yīng)用,實(shí)踐表明該方法能夠提高高鐵信號(hào)系統(tǒng)安全關(guān)鍵功能測(cè)試的完備性和測(cè)試效率.
致謝:本文工作得到高鐵信號(hào)工程列控系統(tǒng)第三方仿真測(cè)試技術(shù)研究(N2018G062)項(xiàng)目的資助.