基于SCADE模型的車(chē)載ATP測(cè)試用例生成方法

李蘭心，王海峰,2，齊志華，湯圣杰，張啟鶴

(1. 北京交通大學(xué) 電子信息工程學(xué)院，北京 100044；2. 北京交通大學(xué) 軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心，北京 100044；3. 中國(guó)鐵道科學(xué)研究院集團(tuán)有限公司 通信信號(hào)研究所，北京 100081；4. 廣州鐵科智控有限公司，廣東 廣州 510220)

在列控系統(tǒng)中，車(chē)載ATP承擔(dān)著列車(chē)自動(dòng)防護(hù)、保證行車(chē)安全等關(guān)鍵任務(wù)，是列控系統(tǒng)的核心[1]。EN 50128標(biāo)準(zhǔn)指出，車(chē)載ATP系統(tǒng)的軟件安全完整性等級(jí)(SIL)為 SIL4，是一種典型的安全苛求系統(tǒng)。因此，非常有必要在正式投入使用前對(duì)車(chē)載ATP系統(tǒng)的安全性和可靠性進(jìn)行滿足高覆蓋度準(zhǔn)則的測(cè)試。

形式化方法具有嚴(yán)格的數(shù)學(xué)基礎(chǔ)，可以無(wú)歧義地描述系統(tǒng)需求，在保障軟件可靠性方面擁有極大優(yōu)勢(shì)?；谀Ｐ偷拈_(kāi)發(fā)方法將形式化思想納入其中，使用形式語(yǔ)言對(duì)被測(cè)系統(tǒng)的測(cè)試環(huán)境或系統(tǒng)行為進(jìn)行建模，可以在滿足系統(tǒng)需求的基礎(chǔ)上提高安全性，因此開(kāi)始逐漸得到廣泛應(yīng)用。基于模型方法的研究始于20世紀(jì)70年代，它屬于一種自動(dòng)化的測(cè)試方法，以模型為基礎(chǔ)，可以生成滿足測(cè)試需求的測(cè)試腳本，并自動(dòng)執(zhí)行測(cè)試，因此可以極大地提高測(cè)試效率[2]。

基于模型的方法可應(yīng)用于建模、驗(yàn)證、測(cè)試、分析等各個(gè)方面，近年來(lái)開(kāi)始逐漸被應(yīng)用到鐵路系統(tǒng)中。文獻(xiàn)[3]提出了一種基于SCADE對(duì)RBC安全防護(hù)功能進(jìn)行建模的方法，這種建模方法更為直觀且能在極大程度上保證安全性。文獻(xiàn)[4]將故障樹(shù)理論和基于模型的方法相結(jié)合，對(duì)列車(chē)運(yùn)行控制系統(tǒng)的模型進(jìn)行了安全驗(yàn)證。在基于模型的測(cè)試方面，文獻(xiàn)[5]采用形式化的方法對(duì)RBC功能進(jìn)行了分析、建模和驗(yàn)證，并在UPPAAL-CoVer工具鏈中生成了可以滿足一定覆蓋度需求的測(cè)試用例。文獻(xiàn)[6]設(shè)計(jì)了一種新型的基于模型測(cè)試的工具M(jìn)TTool，并提出了一種ERE模型，設(shè)計(jì)了一種基于ERE模型自動(dòng)生成測(cè)試用例的方法。在基于模型的測(cè)試中，選擇和建立一個(gè)合適的模型是決定后續(xù)工作成敗的關(guān)鍵。早期基于模型的測(cè)試主要采用有限狀態(tài)機(jī)、Petri網(wǎng)等進(jìn)行建模，隨著研究深入發(fā)現(xiàn)，基于模型的測(cè)試可以適用于幾乎所有軟件，尤其適合嵌入式系統(tǒng)，這就需要為特定的系統(tǒng)尋求更好的建模方式[7]。車(chē)載ATP系統(tǒng)作為一個(gè)安全苛求系統(tǒng)，現(xiàn)有的大部分建模軟件難以滿足其安全性需求，因此需要為這種安全苛求系統(tǒng)尋求更合適的開(kāi)發(fā)工具。

SCADE是一個(gè)圖形化的軟件建模開(kāi)發(fā)環(huán)境，其內(nèi)在以形式化的同步語(yǔ)言為基礎(chǔ)，因此可以無(wú)歧義地、精確地描述系統(tǒng)狀態(tài)和控制邏輯，是一個(gè)可以滿足高安全性需求的開(kāi)發(fā)環(huán)境。在整個(gè)軟件開(kāi)發(fā)的流程中，SCADE 可以覆蓋從需求分析到生成代碼的整個(gè)過(guò)程，并且其通過(guò)KCG自動(dòng)生成的C語(yǔ)言代碼符合EN 50128等標(biāo)準(zhǔn)的認(rèn)證要求，因此適合應(yīng)用于對(duì)SIL4 級(jí)的車(chē)載ATP系統(tǒng)進(jìn)行開(kāi)發(fā)和研究[8]。

在傳統(tǒng)方法中，對(duì)于安全苛求系統(tǒng)的SCADE模型，往往采用人工的方式進(jìn)行檢查，工作量較大，故測(cè)試周期較長(zhǎng)，且測(cè)試質(zhì)量易受到測(cè)試人員工作經(jīng)驗(yàn)的影響?；谀Ｐ偷淖詣?dòng)化測(cè)試手段，不僅可以提高測(cè)試效率，而且可以通過(guò)一定的算法保證測(cè)試的完備性。但如何生成高質(zhì)量的測(cè)試用例，一直是基于模型的測(cè)試應(yīng)用于實(shí)際中的一大挑戰(zhàn)。針對(duì)這一問(wèn)題，本文提出了一種基于SCADE安全狀態(tài)機(jī)模型自動(dòng)生成最小具體測(cè)試用例集的方法，并對(duì)測(cè)試用例進(jìn)行了評(píng)估。

1 基于模型的車(chē)載ATP測(cè)試用例框架

1.1 車(chē)載ATP系統(tǒng)介紹

根據(jù)IEEE對(duì)CBTC系統(tǒng)設(shè)計(jì)以及系統(tǒng)功能配置的規(guī)定，車(chē)載ATP系統(tǒng)主要包括速度監(jiān)控、列車(chē)定位、確定安全距離點(diǎn)、無(wú)線通信管理、數(shù)據(jù)記錄及管理等幾個(gè)功能[9]。其功能核心是實(shí)現(xiàn)速度防護(hù)，及時(shí)防止列車(chē)超速或越過(guò)安全距離。ATP系統(tǒng)的配置共有7個(gè)部分：安全計(jì)算機(jī)、測(cè)速測(cè)距單元、應(yīng)答器數(shù)據(jù)處理裝置、列車(chē)接口單元、無(wú)線通信單元、人機(jī)界面、運(yùn)行數(shù)據(jù)記錄及管理單元。其中：車(chē)載安全計(jì)算機(jī)為系統(tǒng)核心，進(jìn)行指令接收和信息處理，及時(shí)向制動(dòng)設(shè)備發(fā)出制動(dòng)指令；測(cè)速測(cè)距單元通過(guò)輪軸測(cè)速傳感器、雷達(dá)測(cè)速傳感器或衛(wèi)星測(cè)速定位系統(tǒng)，測(cè)算并發(fā)送列車(chē)實(shí)際速度到安全計(jì)算機(jī)；人機(jī)界面對(duì)指令、線路信息和列車(chē)速度信息等進(jìn)行顯示，在安全計(jì)算機(jī)計(jì)算出需要進(jìn)行超速防護(hù)時(shí)顯示報(bào)警信息；運(yùn)行數(shù)據(jù)及管理單元用于管理列車(chē)信息，例如工作模式和相應(yīng)的限速等。車(chē)載ATP系統(tǒng)的功能結(jié)構(gòu)見(jiàn)圖1。

圖1 車(chē)載ATP系統(tǒng)功能結(jié)構(gòu)

在列車(chē)運(yùn)行過(guò)程中，車(chē)載安全計(jì)算機(jī)通過(guò)輸入的限速信息、線路信息、列車(chē)性能參數(shù)、現(xiàn)場(chǎng)設(shè)備的相關(guān)參數(shù)等數(shù)據(jù)，綜合計(jì)算出速度控制曲線，并實(shí)時(shí)的將當(dāng)前速度與控制曲線進(jìn)行對(duì)比，以保證行車(chē)安全。速度控制曲線的繪制需要根據(jù)需求劃分成三大部分，對(duì)于曲線的繪制過(guò)程將在下面的章節(jié)詳細(xì)描述。

車(chē)載ATP的另一個(gè)主要功能為模式轉(zhuǎn)換。根據(jù)CTCS-3級(jí)列控系統(tǒng)技術(shù)規(guī)范中的規(guī)定，車(chē)載ATP共有 9種不同的工作狀態(tài)。為能夠有效地應(yīng)對(duì)各種客運(yùn)、貨運(yùn)需要，鐵路上的作業(yè)往往復(fù)雜且涉及面廣，因此車(chē)載ATP需要根據(jù)不同作業(yè)內(nèi)容的需要，適時(shí)轉(zhuǎn)變工作狀態(tài)，并遵循規(guī)定的觸發(fā)條件。

1.2 基于模型的測(cè)試用例生成

本文利用形式化建模工具SCADE對(duì)被測(cè)系統(tǒng)進(jìn)行建模，并探索一種基于SCADE模型生成測(cè)試用例的方法。基于模型的測(cè)試用例生成主要有3個(gè)步驟，見(jiàn)圖2[10]，下面對(duì)其流程做詳細(xì)說(shuō)明。

圖2 基于模型的測(cè)試步驟

(1)建模。形式化建模是基于模型測(cè)試的第一步，需根據(jù)測(cè)試需求及測(cè)試計(jì)劃，選擇合適的模型。建立的模型需要抽象、完整并且精確，只需描述出想要測(cè)試的關(guān)鍵部分，而一些細(xì)節(jié)則可以忽略。對(duì)于安全苛求系統(tǒng)，建模過(guò)程不僅需要符合需求，還需對(duì)安全性進(jìn)行檢查，以保證語(yǔ)義的嚴(yán)謹(jǐn)性。

(2)生成測(cè)試用例。測(cè)試用例是整個(gè)測(cè)試過(guò)程的基礎(chǔ)和關(guān)鍵，需要滿足一定的覆蓋度準(zhǔn)則，才能保證測(cè)試的質(zhì)量和效率。結(jié)構(gòu)覆蓋度準(zhǔn)則是一種常見(jiàn)的、基本的覆蓋度準(zhǔn)則，目前公認(rèn)的能在最大程度上保證測(cè)試完備性的覆蓋度準(zhǔn)則為全遷移覆蓋，即模型中的每條遷移都至少被遍歷一次。

(3)測(cè)試用例實(shí)例化。由于模型不包括被測(cè)系統(tǒng)的所有細(xì)節(jié)，故從模型生成的測(cè)試用例是抽象的，并不能直接執(zhí)行。根據(jù)一定的準(zhǔn)則，結(jié)合系統(tǒng)運(yùn)行過(guò)程中可能產(chǎn)生的具體數(shù)據(jù)，設(shè)計(jì)出可以在被測(cè)系統(tǒng)上執(zhí)行的測(cè)試腳本，這一過(guò)程即為測(cè)試用例的實(shí)例化。

在基于模型的測(cè)試中，測(cè)試用例的生成是一個(gè)全自動(dòng)的過(guò)程，生成的測(cè)試用例包括每個(gè)事件的操作或者輸入?yún)?shù)，以及預(yù)期的輸出結(jié)果。現(xiàn)有的一些基于模型測(cè)試的工具包括自動(dòng)生成測(cè)試用例的功能，但大都不適合應(yīng)用于對(duì)安全苛求系統(tǒng)的測(cè)試。故本文在SCADE中對(duì)車(chē)載ATP系統(tǒng)進(jìn)行研究，并采用基于模型的方法生成可在SCADE上執(zhí)行的具體測(cè)試用例。

2 基于SCADE的車(chē)載ATP系統(tǒng)功能建模

2.1 SCADE建模方法

車(chē)載ATP系統(tǒng)由輸入驅(qū)動(dòng)，且需要根據(jù)外部的環(huán)境對(duì)列車(chē)運(yùn)行進(jìn)行實(shí)時(shí)監(jiān)控，是一種典型的反應(yīng)式系統(tǒng)。對(duì)于這樣的系統(tǒng)的描述，不僅需要考慮轉(zhuǎn)換關(guān)系，對(duì)于指定輸入的輸出，還需考慮在同一步驟中狀態(tài)和環(huán)境之間復(fù)雜的約束關(guān)系。因此，對(duì)軟件或硬件反應(yīng)式系統(tǒng)的行為進(jìn)行規(guī)范相當(dāng)復(fù)雜，普通的建模方法極容易造成錯(cuò)誤。

SCADE是一個(gè)耦合了數(shù)據(jù)處理和狀態(tài)機(jī)的圖形化的開(kāi)發(fā)環(huán)境，SCADE語(yǔ)言以擁有同步數(shù)據(jù)流風(fēng)格的同步語(yǔ)言Lustre和Esterel為基礎(chǔ)[11]，可以基于模型來(lái)說(shuō)明、模擬、驗(yàn)證和自動(dòng)生成認(rèn)證級(jí)C代碼。針對(duì)離散控制系統(tǒng)和連續(xù)控制系統(tǒng)，SCADE分別設(shè)計(jì)了安全狀態(tài)機(jī)和數(shù)據(jù)流圖兩種建模方法。數(shù)據(jù)流圖體現(xiàn)了輸入到輸出的控制流，用戶(hù)可以利用SCADE提供的基礎(chǔ)操作符進(jìn)行設(shè)計(jì)。安全狀態(tài)機(jī)(SSM)則通過(guò)遷移和狀態(tài)描述離散系統(tǒng)中不同的觸發(fā)條件下系統(tǒng)狀態(tài)的變化。狀態(tài)機(jī)內(nèi)必須定義一個(gè)初始狀態(tài)，任一遷移都有確定的優(yōu)先級(jí)。在任一執(zhí)行周期，安全狀態(tài)機(jī)中的狀態(tài)和行為都是確定的。

SCADE可以自行檢查并發(fā)狀態(tài)和遷移之間的關(guān)系，并對(duì)模型安全性進(jìn)行驗(yàn)證，設(shè)計(jì)者只需關(guān)注業(yè)務(wù)邏輯本身。本文以車(chē)載ATP的兩大核心功能為例，綜合運(yùn)用SCADE中的建模方式建立模型，重點(diǎn)研究可執(zhí)行測(cè)試用例的生成算法。

2.2 速度監(jiān)控功能建模

車(chē)載ATP系統(tǒng)對(duì)于速度的監(jiān)控以及監(jiān)控曲線的生成需要實(shí)時(shí)進(jìn)行，故其更適合于采用數(shù)據(jù)流圖的方式進(jìn)行建模。速度監(jiān)控曲線示意見(jiàn)圖3。對(duì)于速度監(jiān)控曲線的計(jì)算有一定的規(guī)范：在CSM區(qū)，需要綜合考慮最大列車(chē)速度、線路允許速度、臨時(shí)限速等信息，故需要將速度限定在一個(gè)常數(shù)值，得到的曲線即最限制速度曲線(MRSP)，其計(jì)算模型見(jiàn)圖4(a)；在TSM區(qū)，各個(gè)監(jiān)控曲線模型的建立分別見(jiàn)圖4(b)、圖4(c)和圖4(d)。

圖3 速度監(jiān)控曲線示意

其中，在EB速度曲線模型的建立過(guò)程中，主要考慮列車(chē)制動(dòng)為理想情況，即加速度恒定。EB曲線的限速值計(jì)算為

(1)

式中：Be為制動(dòng)加速度；S為目標(biāo)距離；ls為當(dāng)前情況下的安全距離。

取列車(chē)的目標(biāo)距離與最大安全距離的差值，以制動(dòng)加速度作為系數(shù)，將變量看成連續(xù)的控制流，通過(guò)底層運(yùn)算符的組合描述控制邏輯，便可得到EB速度曲線計(jì)算的數(shù)據(jù)流圖模型。

在CSM區(qū)，速度監(jiān)控曲線的繪制主要和目標(biāo)速度、頂棚速度相關(guān)。在此區(qū)域列車(chē)的運(yùn)行模式有4種，分別為NOMAL，WARNING，EMER_BRAKE和SERVICE_BRAKE。對(duì)于每一種工作模式都有其工作時(shí)的速度要求范圍。在列車(chē)速度超過(guò)閾值時(shí)，車(chē)載ATP需要及時(shí)轉(zhuǎn)換工作模式，實(shí)現(xiàn)安全防護(hù)。本文使用SCADE安全狀態(tài)機(jī)模型對(duì)頂棚速度監(jiān)控區(qū)的監(jiān)控邏輯進(jìn)行建模，得到的模型見(jiàn)圖5。其中，狀態(tài)之間的遷移采用強(qiáng)遷移，即轉(zhuǎn)移可以在同一運(yùn)算周期發(fā)生，保證了實(shí)時(shí)性。

圖4 速度監(jiān)控計(jì)算模型

圖5 CSM區(qū)速度控制模型

在TSM區(qū)，列車(chē)已運(yùn)行在一個(gè)限制速度，因此在計(jì)算防護(hù)曲線時(shí)需要著重考慮列車(chē)制動(dòng)性能以及一些線路參數(shù)信息，監(jiān)控邏輯與CSM區(qū)有一定區(qū)別。因此TSM區(qū)在 CSM區(qū)制動(dòng)防護(hù)的基礎(chǔ)上又在首尾分別增加了兩級(jí)制動(dòng)，控制邏輯的SSM模型見(jiàn)圖6。

圖6 TSM區(qū)速度控制模型

2.3 模式轉(zhuǎn)換功能建模

CTCS-3級(jí)列控車(chē)載系統(tǒng)的模式轉(zhuǎn)換功能由外部環(huán)境或內(nèi)部輸入觸發(fā)，屬于一種離散控制，適合用SSM模型建模。本文針對(duì)模式轉(zhuǎn)換功能規(guī)范進(jìn)行模型設(shè)計(jì)，首先根據(jù)觸發(fā)的條件設(shè)計(jì)輸入變量，然后將車(chē)載ATP工作模式抽象為狀態(tài)，將轉(zhuǎn)換條件抽象為遷移。在建模過(guò)程中進(jìn)行如下定義：狀態(tài)機(jī)之間的連接方式采用強(qiáng)連接，模型中的每個(gè)狀態(tài)都可以通過(guò)其他狀態(tài)抵達(dá)；狀態(tài)機(jī)可以嵌套，遷移條件觸發(fā)時(shí)，在同一計(jì)算周期，狀態(tài)發(fā)生相應(yīng)轉(zhuǎn)換，并執(zhí)行轉(zhuǎn)換后狀態(tài)機(jī)內(nèi)部嵌套的狀態(tài)或數(shù)據(jù)流；遷移時(shí)的行為在遷移進(jìn)行時(shí)瞬時(shí)發(fā)生，不影響計(jì)算周期或狀態(tài)內(nèi)部的行為。通過(guò)以上定義建立的模式轉(zhuǎn)換功能的安全狀態(tài)機(jī)模型見(jiàn)圖7。其中每一個(gè)安全狀態(tài)機(jī)(例如FS、CO、TR等)代表一個(gè)ATP工作模式，部分主要輸入變量的含義見(jiàn)表1。

圖7 模式轉(zhuǎn)換模型

表1 模式轉(zhuǎn)換功能模型部分輸入變量含義

3 測(cè)試用例生成方法

對(duì)于生成的測(cè)試用例的質(zhì)量，需要通過(guò)一定的標(biāo)準(zhǔn)進(jìn)行評(píng)判，即覆蓋度準(zhǔn)則。本文從滿足測(cè)試用例完備性的角度出發(fā)，針對(duì)SSM模型提出了一種測(cè)試用例的生成方法。根據(jù)圖論思想，SSM模型可以抽象為點(diǎn)和邊構(gòu)成的有向圖，并可以設(shè)計(jì)算法從圖中生成測(cè)試用例。由于遷移條件均可寫(xiě)成布爾邏輯表達(dá)式的形式，故本文提出可以依據(jù)MC/DC覆蓋準(zhǔn)則，從抽象的測(cè)試用例生成測(cè)試腳本，得到可執(zhí)行的最小測(cè)試用例集。

3.1 模型轉(zhuǎn)換

安全狀態(tài)機(jī)可以被定義為一個(gè)七元組(Q,q0,Vi,Vo,I,f,T)[11]。其中：Q代表車(chē)載ATP的各個(gè)工作模式；q0∈Q為初始狀態(tài)，即SB模式；Vi和Vo分別為輸入和輸出變量集；I為各狀態(tài)默認(rèn)情況下的輸入值；f:Q×Vi→Q為輸入變量Vi使車(chē)載ATP系統(tǒng)轉(zhuǎn)換到新的工作模式的一個(gè)遷移。由于在模式轉(zhuǎn)換功能測(cè)試中，重點(diǎn)關(guān)心的是車(chē)載ATP的各個(gè)狀態(tài)能不能在觸發(fā)條件發(fā)生時(shí)進(jìn)行相應(yīng)的轉(zhuǎn)換，因此本文首先進(jìn)行了模型的解析和轉(zhuǎn)化。只保留SSM模型中的狀態(tài)和遷移，將SSM模型圖抽象為一個(gè)有序二元組G=(V,E)。其中：V表示一組節(jié)點(diǎn)；E表示一組邊[12]。簡(jiǎn)化后的狀態(tài)轉(zhuǎn)換圖見(jiàn)圖8。圖8中：S0～S8為車(chē)載ATP的9種工作狀態(tài)；t0～t37為狀態(tài)之間的遷移條件。

圖8 模式轉(zhuǎn)換功能模型的狀態(tài)轉(zhuǎn)換

根據(jù)全遷移覆蓋準(zhǔn)則，系統(tǒng)應(yīng)首先到達(dá)一個(gè)狀態(tài)，即當(dāng)前狀態(tài)。系統(tǒng)未開(kāi)始運(yùn)行時(shí)，當(dāng)前狀態(tài)為規(guī)定的初始狀態(tài)。若遷移被觸發(fā)，則系統(tǒng)轉(zhuǎn)換到下一狀態(tài)。相較于其他覆蓋度準(zhǔn)則，全遷移覆蓋所需的測(cè)試用例較少。由于二元圖中節(jié)點(diǎn)的可達(dá)性[12]，為實(shí)現(xiàn)上述目標(biāo)，將狀態(tài)轉(zhuǎn)換圖中的t0～t37轉(zhuǎn)換成節(jié)點(diǎn)，即T0～T37，將S0～S8根據(jù)狀態(tài)轉(zhuǎn)換圖中的遷移關(guān)系添加為T(mén)0～T37之間的有向邊，則可以將狀態(tài)轉(zhuǎn)換圖轉(zhuǎn)化為遷移路徑圖，遍歷遷移路徑圖則可以生成全遷移覆蓋準(zhǔn)則下的抽象測(cè)試用例。

算法1：遷移路徑圖生成算法

1: Path(v)

2: visited[v]=true

3: Stacksta=MakeStack(MAX_SIZE);

4: push(sta,v);

5: while (!Empty(sta)) do

6:n=Pop(sta)

7: for eachnextNodeinn

8: if (!visit[nextNode])

9: visit[nextNode]=true;

10: push(sta,nextNode);

11: end if

12: end for

13: end while

3.2 全遷移覆蓋測(cè)試用例生成

抽象測(cè)試用例的生成是本文提出的測(cè)試用例生成方法中的第一步，但并不是最關(guān)鍵的一步，只需確保滿足對(duì)全部遷移的覆蓋性，因此，采取圖的遍歷算法中常用的深度優(yōu)先搜索算法對(duì)遷移路徑圖進(jìn)行遍歷。直到搜索到的節(jié)點(diǎn)為終止節(jié)點(diǎn)，則表明一條測(cè)試用例生成成功。經(jīng)過(guò)試驗(yàn)得到的抽象測(cè)試用例結(jié)果見(jiàn)表2。

算法2：深度搜索算法偽代碼

1: DFS(v)

2: visited[v]=true

3: Stacksta=MakeStack(MAX_SIZE);

4: Push(sta,v);

5: while (!Empty(sta)) do

6:w=Pop(sta)

7: for eachnextNodeinwdo

8: if (!visit[nextNode]) then

9: visit[nextNode]=true;

10: Push(sta,nextNode);

11: end if

12: end for

3.3 基于MC/DC的具體測(cè)試用例集生成

基于模型生成的測(cè)試用例并不能直接輸入到被測(cè)系統(tǒng)中執(zhí)行，還需要基于數(shù)據(jù)將其轉(zhuǎn)換成可執(zhí)行的測(cè)試腳本。為確保轉(zhuǎn)換過(guò)程中測(cè)試腳本的覆蓋度依然可以滿足測(cè)試過(guò)程中對(duì)于完備性的要求，在轉(zhuǎn)換過(guò)程中同樣需要滿足一定的覆蓋度準(zhǔn)則。MC/DC覆蓋準(zhǔn)則是一種結(jié)構(gòu)覆蓋方法，但其更注重每個(gè)條件對(duì)結(jié)果產(chǎn)生影響的獨(dú)立性，可以保證覆蓋每個(gè)可能的結(jié)果，并且每個(gè)條件對(duì)結(jié)果的獨(dú)立影響作用都能得到體現(xiàn)，因此采取MC/DC覆蓋準(zhǔn)則的思想進(jìn)行下一步的算法設(shè)計(jì)。

快速生成算法專(zhuān)門(mén)針對(duì)MC/DC覆蓋度準(zhǔn)則設(shè)計(jì)，直接對(duì)布爾表達(dá)式進(jìn)行處理，是一種快速高效的MC/DC覆蓋度算法。將任意布爾表達(dá)式抽象成一個(gè)條件為葉節(jié)點(diǎn)、判定為根節(jié)點(diǎn)的語(yǔ)法樹(shù)。為體現(xiàn)影響條件的獨(dú)立性，限制右子樹(shù)的節(jié)點(diǎn)，將可以影響判定結(jié)果的條件置于最左側(cè)子葉的位置，對(duì)語(yǔ)法樹(shù)的左右子樹(shù)進(jìn)行置換，這樣不會(huì)影響判定的結(jié)果[13]，但可以讓每個(gè)條件獨(dú)立影響判定結(jié)果一次。

表2 抽象測(cè)試用例

算法中主要有當(dāng)前條件、直接判定、前置條件、默認(rèn)數(shù)據(jù)以及自由條件等幾個(gè)概念[13]。針對(duì)任一布爾邏輯表達(dá)式，首先設(shè)計(jì)一個(gè)結(jié)構(gòu)體，用于存放布爾表達(dá)式中每一元素的屬性、默認(rèn)值以及當(dāng)前值。數(shù)組ArrayList用于存放指向結(jié)構(gòu)體的指針，遍歷此數(shù)組則可以得到當(dāng)前條件。在初始狀態(tài)時(shí)設(shè)置第一個(gè)條件為當(dāng)前條件，其測(cè)試數(shù)據(jù)取0、1兩種情況，其余條件的測(cè)試數(shù)據(jù)取默認(rèn)值。

算法3：快速生成算法偽代碼

輸入: Str value //將布爾邏輯表達(dá)式及其默認(rèn)值寫(xiě)成string類(lèi)型的數(shù)據(jù)

輸出: TestCases[] //輸出為一個(gè)由bool數(shù)據(jù)構(gòu)成的二維數(shù)組

1：ArrayList[]=getArray(Str)

2：PresentValue=getDefauleValue()

3：getTestCase()

4：fori

5： if Condition then

6： PresentValue=!getDefaultValue() //默認(rèn)數(shù)據(jù)取反設(shè)為當(dāng)前條件值

setPreCondition(getDefaultValue()) //當(dāng)前條件的默認(rèn)值傳遞給前置條件

7： addTestCaseto TestCases[]

8： end if

9：end for

算法3中涉及的主要函數(shù)見(jiàn)表3，其中setPreCondition()函數(shù)為該算法中的一個(gè)核心步驟，用于尋找前置條件。顧名思義，前置條件即位于當(dāng)前條件之前的條件，但如果當(dāng)前條件之前為右括號(hào)，則需要尋找到與其對(duì)應(yīng)的左括號(hào)之后的一個(gè)條件，并將其設(shè)置為前置條件；若當(dāng)前條件之前為左括號(hào)或數(shù)組盡頭，則搜索過(guò)程結(jié)束。

表3 快速生成算法子函數(shù)

對(duì)于表2中的抽象測(cè)試用例，均可通過(guò)快速生成算法進(jìn)行處理，最終可以得到滿足全遷移覆蓋和MC/DC覆蓋準(zhǔn)則的可執(zhí)行測(cè)試用例集。

4 測(cè)試用例分析評(píng)估

根據(jù)以上算法設(shè)計(jì)的測(cè)試用例集生成工具，通過(guò)計(jì)算機(jī)語(yǔ)言C#進(jìn)行了編程實(shí)現(xiàn)，將生成的測(cè)試腳本導(dǎo)入SCADE中，通過(guò)SCADE配套的測(cè)試分析環(huán)境SCADE QTE對(duì)覆蓋度進(jìn)行分析，并采用變異分析的方式對(duì)測(cè)試用例的完備性進(jìn)行了評(píng)估。

SCADE中的認(rèn)證級(jí)測(cè)試環(huán)境(Qualified Test Environment, QTE)，可以支持在主機(jī)上的功能測(cè)試，以及模型和代碼的覆蓋分析。SCADE QTE支持在主機(jī)上仿真目標(biāo)機(jī)上的測(cè)試執(zhí)行過(guò)程，可以對(duì)測(cè)試用例質(zhì)量的評(píng)估提供強(qiáng)有力的支撐，并且方便后續(xù)在目標(biāo)機(jī)上執(zhí)行測(cè)試。在SCADE QTE上生成的覆蓋度分析報(bào)告表明，測(cè)試用例對(duì)模型的狀態(tài)覆蓋率與結(jié)構(gòu)覆蓋率都達(dá)到了100%，MC/DC覆蓋率為74.3%，這是由于為保證全遷移測(cè)試的完備性，在基于MC/DC覆蓋準(zhǔn)則生成測(cè)試數(shù)據(jù)時(shí)，選擇剔除了不能使每條測(cè)試用例完整執(zhí)行的情況。

變異分析是一種通過(guò)評(píng)估測(cè)試用例檢測(cè)出錯(cuò)誤的能力，來(lái)評(píng)價(jià)測(cè)試用例好壞的分析方法。首先對(duì)待檢測(cè)的模型進(jìn)行變異，產(chǎn)生一系列的變異模型，然后在模型中運(yùn)行測(cè)試用例，若能夠檢驗(yàn)出變異模型和原始模型的差異，則證明測(cè)試用例是有效的。在本文用于生成測(cè)試用例的SSM模型中，通過(guò)增加、減少狀態(tài)、遷移，以及改變邏輯運(yùn)算符等方式產(chǎn)生變異模型。變異評(píng)分的計(jì)算公式為

(2)

式中：MS(P,T)為變異評(píng)分；DM(P,T)為被發(fā)現(xiàn)的變異體數(shù)目；M(P)為變異體總數(shù)；EM(P)為等效變異體數(shù)。

在試驗(yàn)中，通過(guò)對(duì)車(chē)載ATP模式轉(zhuǎn)換功能模型進(jìn)行改變邏輯運(yùn)算符、遷移條件等變異，可以得到102個(gè)變異體。具體變異類(lèi)型與數(shù)量見(jiàn)表4。

對(duì)變異測(cè)試結(jié)果進(jìn)行變異評(píng)分的計(jì)算結(jié)果見(jiàn)表5。從表5可知，生成的測(cè)試用例在檢測(cè)邏輯運(yùn)算符變異以及遷移條件變異時(shí)評(píng)分均為1，這說(shuō)明發(fā)現(xiàn)了絕大多數(shù)的變異，檢測(cè)效果較好，結(jié)果具有很強(qiáng)借鑒意義。

表 4 變異類(lèi)型及數(shù)量

表5 變異結(jié)果

5 結(jié)束語(yǔ)

本文針對(duì)SCADE模型，提出了一種生成具體可執(zhí)行測(cè)試用例集的方法。首先，被測(cè)系統(tǒng)的模型要在可以滿足安全苛求系統(tǒng)可靠性要求的開(kāi)發(fā)環(huán)境SCADE中進(jìn)行建立；其次，由于基于模型生成的滿足全遷移覆蓋度準(zhǔn)則的測(cè)試用例是抽象的，不能直接應(yīng)用于測(cè)試，因此本文結(jié)合滿足MC/DC覆蓋度準(zhǔn)則的算法，將其轉(zhuǎn)化為可執(zhí)行的測(cè)試用例集。以CTCS-3級(jí)車(chē)載ATP系統(tǒng)模式轉(zhuǎn)換功能為例，對(duì)此方法進(jìn)行了驗(yàn)證實(shí)驗(yàn)，并在SCADE中運(yùn)行測(cè)試腳本，采用變異分析的方法對(duì)測(cè)試用例的質(zhì)量進(jìn)行了評(píng)估。最終證明該方法可以滿足覆蓋度需求，測(cè)試完備度較高，可以提升測(cè)試自動(dòng)化水平。