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

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

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

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

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

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

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

1.1 時間自動機理論(TA)

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

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

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

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

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

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

表1 BNF語句及其含義

1.2 TA變異

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

表2 變異算子

1.3 TA變異分析與評估

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

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

2 等級轉(zhuǎn)換場景變異測試

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

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

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

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

圖1 RODB時間自動機模型

2.2 RODB變異體模型建立

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

“從Onboard向RBC建立聯(lián)系”的時間自動機模型為TA_A0,其表示“在輸入行為Link后，系統(tǒng)從位置idle遷移到q1，在T_trainto rbc≤10的約束條件下輸出行為Connect，進而遷移到位置q2，最后經(jīng)輸出CommInfo行為將位置遷移到WaitTrainInfo”。對TA_A0進行改變約束，即將約束條件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 測試輔助工具 MoMuT: : TA

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

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

3 等級轉(zhuǎn)換變異測試與完備性評估

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

3.1 測試案例的篩選歸并

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

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

3.2 變異體的生成

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

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

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

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

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

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

4 測試案例集的完善

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

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

5 結(jié)論

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