基于TA的等級(jí)轉(zhuǎn)換場(chǎng)景變異測(cè)試方法研究

宋 莉， 李 飛,2,3， 趙 瑜， 趙 健

(1.馬鞍山學(xué)院 人工智能創(chuàng)新學(xué)院，安徽 馬鞍山 243199; 2. 安徽工業(yè)大學(xué) 電氣與信息工程學(xué)院, 安徽 馬鞍山 243032; 3. 中國(guó)科學(xué)院合肥物質(zhì)科學(xué)研究院，安徽 合肥 230031)

宋莉，李飛，趙瑜，等.基于TA的等級(jí)轉(zhuǎn)換場(chǎng)景變異測(cè)試方法研究[J].石家莊鐵道大學(xué)學(xué)報(bào)(自然科學(xué)版),2022,35(1):57-63.

等級(jí)轉(zhuǎn)換場(chǎng)景是列控系統(tǒng)(Chinese Train Control Syetem，CTCS)典型的運(yùn)營(yíng)場(chǎng)景之一，是實(shí)現(xiàn)CTCS-2/CTCS-3級(jí)兼容的技術(shù)方法。研究等級(jí)轉(zhuǎn)換場(chǎng)景時(shí)一般需要考慮2種情況，其一是正常情況下在固定地點(diǎn)進(jìn)行的級(jí)間轉(zhuǎn)換，其二是由于特殊原因引起的降級(jí)轉(zhuǎn)換。

測(cè)試是分析驗(yàn)證系統(tǒng)正確性及可靠性的重要手段，測(cè)試用例是測(cè)試的基礎(chǔ)。近年來，基于模型的測(cè)試案例日趨成熟，文獻(xiàn)[1]結(jié)合時(shí)間自動(dòng)機(jī)和一致性關(guān)系理論，提出了一種新型列車自動(dòng)保護(hù)系統(tǒng)(Automatic Train Protection，ATP) 在線一致性測(cè)試方法，并取得了良好的效果；文獻(xiàn)[2]基于輸入輸出時(shí)間自動(dòng)機(jī)理論對(duì)列控系統(tǒng)中9種列車運(yùn)營(yíng)模式進(jìn)行變異測(cè)試分析，得到了較為完善的測(cè)試案例；文獻(xiàn)[3]針對(duì)報(bào)警系統(tǒng)構(gòu)建TA模型和變異體模型，使用增量算法技術(shù)生成測(cè)試案例，并對(duì)案例集的完備性進(jìn)行了評(píng)估。

本文對(duì)列控系統(tǒng)等級(jí)轉(zhuǎn)換場(chǎng)景構(gòu)建TA模型和變異體模型，同時(shí)借助測(cè)試輔助工具M(jìn)oMuT::TA生成測(cè)試案例，并補(bǔ)充完善原測(cè)試案例集，得到了較為完善的測(cè)試案例集。

1 基于TA變異分析的測(cè)試案例生成方法

1.1 時(shí)間自動(dòng)機(jī)理論(TA)

時(shí)間自動(dòng)機(jī)理論增加了時(shí)間約束機(jī)制，每一個(gè)系統(tǒng)時(shí)鐘均可在任意一個(gè)位置和狀態(tài)遷移時(shí)對(duì)其重置，從而可以有效表達(dá)實(shí)時(shí)系統(tǒng)的時(shí)間約束特性[4]。

時(shí)間自動(dòng)機(jī)TA可以描述為TA=，在該六元組中，S為一組有限位置，S0?S為TA的初始位置，A為一組有限事件，X為一組有限時(shí)鐘，I:SФ(х)描述映射，x∈X，任一位置s∈S都被指定Ф(х)中的時(shí)鐘約束δ，E?S×A×Ф(х)×2x×S，表示系統(tǒng)中所有狀態(tài)遷移的集合[5]。

列控系統(tǒng)等級(jí)轉(zhuǎn)換場(chǎng)景是一個(gè)復(fù)雜的場(chǎng)景，由多個(gè)構(gòu)成對(duì)象構(gòu)成，因此在建立TA模型時(shí)，單一模型是無法滿足其功能需求的，需要同時(shí)建立多個(gè)模型同步描述系統(tǒng)行為。此時(shí)將等級(jí)轉(zhuǎn)換場(chǎng)景劃分為不同模塊單獨(dú)建立TA模型，同時(shí)對(duì)各模型增加并行組合與約束條件，實(shí)現(xiàn)模型之間的同步通信，進(jìn)而構(gòu)成整個(gè)系統(tǒng)的時(shí)間自動(dòng)機(jī)模型。

UPPAAL是基于時(shí)間自動(dòng)機(jī)的建模驗(yàn)證工具，通過在UPPAAL的編輯器中聲明通道和共享變量實(shí)現(xiàn)等級(jí)轉(zhuǎn)換場(chǎng)景中不同模塊間的通信，進(jìn)而構(gòu)成一個(gè)完整的TA模型[6]。任意時(shí)刻，并行模塊之間的發(fā)送器和接收器由通道聲明(Chanb)聯(lián)系在一起，“b!”表示發(fā)送事件b后位置遷移，“b?”表示接收事件b后位置遷移，“b!”和“b?”是同時(shí)發(fā)生的，有發(fā)送動(dòng)作“b!”就一定有接收動(dòng)作“b?”。此外，UPPAAL還用broadcast chan聲明廣播通道，可以實(shí)現(xiàn)一發(fā)多收的功能，以broadcast chand為例，發(fā)生“d!”后，系統(tǒng)中

所有子模型的“d?”都可能發(fā)生。設(shè)置通道聲明實(shí)現(xiàn)了不同子模型之間的信息交互，將復(fù)雜系統(tǒng)有機(jī)建立起來。

UPPAAL的驗(yàn)證器使用了BNF(Backus-Naur Form)語(yǔ)言驗(yàn)證模型的性質(zhì)，BNF是一種簡(jiǎn)潔、方便的描述語(yǔ)言，其定義如下：Prop::=E<>p|A[]p|E[]p|A<>p|p→q。各語(yǔ)句的含義如表1所示。

表1 BNF語(yǔ)句及其含義

1.2 TA變異

模型變異通過對(duì)系統(tǒng)中某些特定部分做微小改動(dòng)來充分模擬系統(tǒng)所有的潛在危險(xiǎn)，是一種基于缺陷的軟件技術(shù)。在變異測(cè)試中，針對(duì)時(shí)間自動(dòng)機(jī)模型，通過設(shè)計(jì)2類變異算子生成變異體：時(shí)間性變異算子(Timed Mutation Operator，TMO)和功能性變異算子(Functional Mutation Operator，F(xiàn)MO)。時(shí)間性變異算子通過改變系統(tǒng)時(shí)鐘約束使其發(fā)生時(shí)間性錯(cuò)誤，繼而構(gòu)造變異模型。功能性變異算子通過改變系統(tǒng)模型中的位置、遷移、函數(shù)等使其發(fā)生功能性故障，繼而構(gòu)造變異模型[7]。在列控系統(tǒng)等級(jí)轉(zhuǎn)換場(chǎng)景中，設(shè)置15種變異算子，包括5種時(shí)間性變異算子和10種功能性變異算子。表2列舉了這15種變異算子。

表2 變異算子

1.3 TA變異分析與評(píng)估

(1)若?i∈[1,n]，使得Execute(TA,tci)≠Execute(M,tci)，即執(zhí)行測(cè)試案例后，TA與變異體M之間不存在一致的路徑交集，稱作殺死變異體M，此時(shí)在測(cè)試集中就可以刪除該測(cè)試案例以節(jié)省測(cè)試成本。

(2)若?i∈[1,n]，都有Execute(M,tci)=Execute(TA,tci),稱作未殺死變異體M，此時(shí)需要對(duì)變異體M做非法判斷和等價(jià)判斷；若判斷結(jié)果為非法變異體和等價(jià)變異體，則稱作無效變異體。

2 等級(jí)轉(zhuǎn)換場(chǎng)景變異測(cè)試

在列控系統(tǒng)中，等級(jí)轉(zhuǎn)換場(chǎng)景是實(shí)現(xiàn)CTCS-2級(jí)和CTCS-3級(jí)兼容的技術(shù)方法，研究等級(jí)轉(zhuǎn)換場(chǎng)景時(shí)一般需要考慮2種情況，其一是正常情況下在固定地點(diǎn)進(jìn)行的級(jí)間轉(zhuǎn)換，其二是由于特殊原因引起的降級(jí)轉(zhuǎn)換[8]。下面詳細(xì)介紹在等級(jí)轉(zhuǎn)換場(chǎng)景下時(shí)間自動(dòng)機(jī)建模及變異分析和測(cè)試案例集完備研究。

2.1 基于TA的等級(jí)轉(zhuǎn)換場(chǎng)景建模

基于時(shí)間自動(dòng)機(jī)理論和等級(jí)轉(zhuǎn)換場(chǎng)景的工作流程，建立列控系統(tǒng)等級(jí)轉(zhuǎn)換TA模型。主要涉及4個(gè)模塊，無限閉塞中心(RBC)、車載系統(tǒng)(Onboard)、司機(jī)(Driver)和應(yīng)答器(Balise)。利用時(shí)間自動(dòng)機(jī)積的定義構(gòu)建網(wǎng)絡(luò)自動(dòng)機(jī)的模型，記為RODB模型，如圖1所示。

設(shè)RODB模型的事件集合為∑，則有：∑=∑RBC&Onboard∪∑Onboard&Driver∪∑Balise&Onboard

圖1 RODB時(shí)間自動(dòng)機(jī)模型

2.2 RODB變異體模型建立

借助15種變異算子對(duì)已建立的RODB模型進(jìn)行變異，形成相應(yīng)的變異體模型。此處以“從Onboard向RBC建立聯(lián)系”為例，通過改變約束時(shí)間，說明變異體模型的形式。

“從Onboard向RBC建立聯(lián)系”的時(shí)間自動(dòng)機(jī)模型為TA_A0,其表示“在輸入行為L(zhǎng)ink后，系統(tǒng)從位置idle遷移到q1，在T_trainto rbc≤10的約束條件下輸出行為Connect，進(jìn)而遷移到位置q2，最后經(jīng)輸出CommInfo行為將位置遷移到WaitTrainInfo”。對(duì)TA_A0進(jìn)行改變約束，即將約束條件T_trainto rbc≤10分別變異為取消約束條件、T_trainto rbc≥10、T_trainto rbc>10、T_trainto rbc≤20，產(chǎn)生的變異體分別為TA_M1、TA_M2、TA_M3、TA_M4，如圖2所示。

圖2 變異體模型

2.3 測(cè)試輔助工具 MoMuT: : TA

MoMuT::TA是一種支持時(shí)間自動(dòng)機(jī)建模語(yǔ)言，研究實(shí)時(shí)系統(tǒng)而開發(fā)的黑盒測(cè)試案例生成工具，能夠自主完成TA模型的變異及生成基于變異模型的測(cè)試用例。首先,MoMuT: : TA通過輸入U(xiǎn)PPAAL中的原始模型XML文件，并分析XML文件中的基本因子，形成啟用模型，添加變異算子使得模型變異，得到變異體。其次，通過一致性檢查/k界模型檢驗(yàn)方法將生成的變異體模型與TA模型反復(fù)判定得到有效變異體，最終將獲取的有效變異體應(yīng)用于測(cè)試案例生成算法中，得到測(cè)試案例。圖3為借助測(cè)試輔助工具M(jìn)oMuT: : TA生成變異體和測(cè)試案例的工作流程。

圖3 MoMuT: : TA生成變異體和測(cè)試案例的工作流程

3 等級(jí)轉(zhuǎn)換變異測(cè)試與完備性評(píng)估

基于對(duì)等級(jí)轉(zhuǎn)換場(chǎng)景的工作流程及信息交互的分析，構(gòu)建了RODB模型。結(jié)合15種變異算子，對(duì)無限閉塞中心RBC、車載系統(tǒng)、司機(jī)操作和地面應(yīng)答器4個(gè)子模塊分析構(gòu)建變異體模型，基于RODB模型和變異體模型，評(píng)估測(cè)試案例的完備性。

3.1 測(cè)試案例的篩選歸并

列控系統(tǒng)是一個(gè)復(fù)雜且龐大的系統(tǒng)，通過查閱《CTCS-3級(jí)列控系統(tǒng)測(cè)試案例(V3.0)》可知，共包含469個(gè)測(cè)試案例，主要研究等級(jí)轉(zhuǎn)換場(chǎng)景下變異測(cè)試分析，故首先需從這469個(gè)測(cè)試案例中篩選出與等級(jí)轉(zhuǎn)換相關(guān)的測(cè)試案例。

根據(jù)設(shè)定的等級(jí)轉(zhuǎn)換場(chǎng)景和已建立的RODB模型，共篩選出與之相關(guān)的44個(gè)測(cè)試案例。為了減少測(cè)試案例的數(shù)量，降低變異測(cè)試的成本，根據(jù)測(cè)試的性質(zhì)和目的將部分相似度較高的測(cè)試案例進(jìn)行分類歸并，簡(jiǎn)化測(cè)試案例集。

3.2 變異體的生成

生成RODB模型的變異體之前，基于變異算子的規(guī)則對(duì)原模型進(jìn)行變異分析，借助輔助工具M(jìn)oMuT::TA對(duì)變異對(duì)象進(jìn)行分析并生成變異體。在進(jìn)行變異測(cè)試之前，通過一致性檢查/k界模型檢驗(yàn)篩除測(cè)試中的非法變異體和等價(jià)變異體，分析研究的主體為剩余的有效變異體[9]。表3為變異體模型信息統(tǒng)計(jì)結(jié)果。

表3 變異體模型信息統(tǒng)計(jì)結(jié)果

3.3 變異分析的執(zhí)行和結(jié)果

將測(cè)試案例集的參數(shù)信息分別反復(fù)輸入到RODB原模型和變異體中，比較兩者的輸出，統(tǒng)計(jì)各類變異體的個(gè)數(shù)，結(jié)合變異分?jǐn)?shù)公式，評(píng)估測(cè)試案例集的完備性，為完善測(cè)試案例集提供依據(jù)。

表4給出了RODB模型變異測(cè)試的數(shù)據(jù)，表中M為生成的總變異體數(shù)，E為等價(jià)變異體數(shù)，N為非法變異體數(shù)，L為活變異體數(shù)，K為模型中殺死的變異體數(shù)，P表示計(jì)算的變異分?jǐn)?shù)，α表示變異算子的序號(hào)，α=1,2,…,15。

表4 變異測(cè)試數(shù)據(jù)

4 測(cè)試案例集的完善

為了研究等級(jí)轉(zhuǎn)換場(chǎng)景中變異測(cè)試和完備性評(píng)估存在的問題，對(duì)測(cè)試中的37個(gè)未殺死變異體進(jìn)行分析，找出變異體未被殺死的原因，其中有33個(gè)未殺死變異體指向測(cè)試案例“超速制動(dòng)防護(hù)處理”覆蓋不全，4個(gè)未殺死變異體指向測(cè)試案例對(duì)模型遍歷不全，根據(jù)分析結(jié)果，補(bǔ)充完善相關(guān)的測(cè)試案例，基于對(duì)變異模型的分析研究，再次借助輔助工具M(jìn)oMuT: : TA驗(yàn)證可得到，NCR、WCR和SCR均獲取了有效測(cè)試數(shù)據(jù)且變異分?jǐn)?shù)達(dá)到了1.00。除此之外，表中的CGC、NUF變異算子的變異分?jǐn)?shù)均提高到了0.95以上，其余變異算子的變異分?jǐn)?shù)也得到了相應(yīng)提高。表明現(xiàn)有的測(cè)試案例集完備性較好。

表5 補(bǔ)充和完善后的變異測(cè)試數(shù)據(jù)

5 結(jié)論

對(duì)等級(jí)轉(zhuǎn)換場(chǎng)景下的變異測(cè)試方法進(jìn)行研究。首先，基于時(shí)間自動(dòng)機(jī)理論，利用UPPAAL工具對(duì)等級(jí)轉(zhuǎn)換場(chǎng)景建立TA模型；其次，對(duì)所建立的TA模型進(jìn)行變異測(cè)試并依據(jù)加權(quán)變異分?jǐn)?shù)定量評(píng)估其完備性；最后，分析完善原測(cè)試案例集，使所有的變異分?jǐn)?shù)均提高到了0.95以上，從而得到了較為完善的測(cè)試案例集。