基于SCADE模型的車載ATP測試用例生成方法

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

(1. 北京交通大學 電子信息工程學院，北京 100044；2. 北京交通大學 軌道交通運行控制系統國家工程研究中心，北京 100044；3. 中國鐵道科學研究院集團有限公司 通信信號研究所，北京 100081；4. 廣州鐵科智控有限公司，廣東 廣州 510220)

在列控系統中，車載ATP承擔著列車自動防護、保證行車安全等關鍵任務，是列控系統的核心[1]。EN 50128標準指出，車載ATP系統的軟件安全完整性等級(SIL)為 SIL4，是一種典型的安全苛求系統。因此，非常有必要在正式投入使用前對車載ATP系統的安全性和可靠性進行滿足高覆蓋度準則的測試。

形式化方法具有嚴格的數學基礎，可以無歧義地描述系統需求，在保障軟件可靠性方面擁有極大優勢。基于模型的開發方法將形式化思想納入其中，使用形式語言對被測系統的測試環境或系統行為進行建模，可以在滿足系統需求的基礎上提高安全性，因此開始逐漸得到廣泛應用。基于模型方法的研究始于20世紀70年代，它屬于一種自動化的測試方法，以模型為基礎，可以生成滿足測試需求的測試腳本，并自動執行測試，因此可以極大地提高測試效率[2]。

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

SCADE是一個圖形化的軟件建模開發環境，其內在以形式化的同步語言為基礎，因此可以無歧義地、精確地描述系統狀態和控制邏輯，是一個可以滿足高安全性需求的開發環境。在整個軟件開發的流程中，SCADE 可以覆蓋從需求分析到生成代碼的整個過程，并且其通過KCG自動生成的C語言代碼符合EN 50128等標準的認證要求，因此適合應用于對SIL4 級的車載ATP系統進行開發和研究[8]。

在傳統方法中，對于安全苛求系統的SCADE模型，往往采用人工的方式進行檢查，工作量較大，故測試周期較長，且測試質量易受到測試人員工作經驗的影響。基于模型的自動化測試手段，不僅可以提高測試效率，而且可以通過一定的算法保證測試的完備性。但如何生成高質量的測試用例，一直是基于模型的測試應用于實際中的一大挑戰。針對這一問題，本文提出了一種基于SCADE安全狀態機模型自動生成最小具體測試用例集的方法，并對測試用例進行了評估。

1 基于模型的車載ATP測試用例框架

1.1 車載ATP系統介紹

根據IEEE對CBTC系統設計以及系統功能配置的規定，車載ATP系統主要包括速度監控、列車定位、確定安全距離點、無線通信管理、數據記錄及管理等幾個功能[9]。其功能核心是實現速度防護，及時防止列車超速或越過安全距離。ATP系統的配置共有7個部分：安全計算機、測速測距單元、應答器數據處理裝置、列車接口單元、無線通信單元、人機界面、運行數據記錄及管理單元。其中：車載安全計算機為系統核心，進行指令接收和信息處理，及時向制動設備發出制動指令；測速測距單元通過輪軸測速傳感器、雷達測速傳感器或衛星測速定位系統，測算并發送列車實際速度到安全計算機；人機界面對指令、線路信息和列車速度信息等進行顯示，在安全計算機計算出需要進行超速防護時顯示報警信息；運行數據及管理單元用于管理列車信息，例如工作模式和相應的限速等。車載ATP系統的功能結構見圖1。

圖1 車載ATP系統功能結構

在列車運行過程中，車載安全計算機通過輸入的限速信息、線路信息、列車性能參數、現場設備的相關參數等數據，綜合計算出速度控制曲線，并實時的將當前速度與控制曲線進行對比，以保證行車安全。速度控制曲線的繪制需要根據需求劃分成三大部分，對于曲線的繪制過程將在下面的章節詳細描述。

車載ATP的另一個主要功能為模式轉換。根據CTCS-3級列控系統技術規范中的規定，車載ATP共有 9種不同的工作狀態。為能夠有效地應對各種客運、貨運需要，鐵路上的作業往往復雜且涉及面廣，因此車載ATP需要根據不同作業內容的需要，適時轉變工作狀態，并遵循規定的觸發條件。

1.2 基于模型的測試用例生成

本文利用形式化建模工具SCADE對被測系統進行建模，并探索一種基于SCADE模型生成測試用例的方法。基于模型的測試用例生成主要有3個步驟，見圖2[10]，下面對其流程做詳細說明。

圖2 基于模型的測試步驟

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

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

(3)測試用例實例化。由于模型不包括被測系統的所有細節，故從模型生成的測試用例是抽象的，并不能直接執行。根據一定的準則，結合系統運行過程中可能產生的具體數據，設計出可以在被測系統上執行的測試腳本，這一過程即為測試用例的實例化。

在基于模型的測試中，測試用例的生成是一個全自動的過程，生成的測試用例包括每個事件的操作或者輸入參數，以及預期的輸出結果。現有的一些基于模型測試的工具包括自動生成測試用例的功能，但大都不適合應用于對安全苛求系統的測試。故本文在SCADE中對車載ATP系統進行研究，并采用基于模型的方法生成可在SCADE上執行的具體測試用例。

2 基于SCADE的車載ATP系統功能建模

2.1 SCADE建模方法

車載ATP系統由輸入驅動，且需要根據外部的環境對列車運行進行實時監控，是一種典型的反應式系統。對于這樣的系統的描述，不僅需要考慮轉換關系，對于指定輸入的輸出，還需考慮在同一步驟中狀態和環境之間復雜的約束關系。因此，對軟件或硬件反應式系統的行為進行規范相當復雜，普通的建模方法極容易造成錯誤。

SCADE是一個耦合了數據處理和狀態機的圖形化的開發環境，SCADE語言以擁有同步數據流風格的同步語言Lustre和Esterel為基礎[11]，可以基于模型來說明、模擬、驗證和自動生成認證級C代碼。針對離散控制系統和連續控制系統，SCADE分別設計了安全狀態機和數據流圖兩種建模方法。數據流圖體現了輸入到輸出的控制流，用戶可以利用SCADE提供的基礎操作符進行設計。安全狀態機(SSM)則通過遷移和狀態描述離散系統中不同的觸發條件下系統狀態的變化。狀態機內必須定義一個初始狀態，任一遷移都有確定的優先級。在任一執行周期，安全狀態機中的狀態和行為都是確定的。

SCADE可以自行檢查并發狀態和遷移之間的關系，并對模型安全性進行驗證，設計者只需關注業務邏輯本身。本文以車載ATP的兩大核心功能為例，綜合運用SCADE中的建模方式建立模型，重點研究可執行測試用例的生成算法。

2.2 速度監控功能建模

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

圖3 速度監控曲線示意

其中，在EB速度曲線模型的建立過程中，主要考慮列車制動為理想情況，即加速度恒定。EB曲線的限速值計算為

(1)

式中：Be為制動加速度；S為目標距離；ls為當前情況下的安全距離。

取列車的目標距離與最大安全距離的差值，以制動加速度作為系數，將變量看成連續的控制流，通過底層運算符的組合描述控制邏輯，便可得到EB速度曲線計算的數據流圖模型。

在CSM區，速度監控曲線的繪制主要和目標速度、頂棚速度相關。在此區域列車的運行模式有4種，分別為NOMAL，WARNING，EMER_BRAKE和SERVICE_BRAKE。對于每一種工作模式都有其工作時的速度要求范圍。在列車速度超過閾值時，車載ATP需要及時轉換工作模式，實現安全防護。本文使用SCADE安全狀態機模型對頂棚速度監控區的監控邏輯進行建模，得到的模型見圖5。其中，狀態之間的遷移采用強遷移，即轉移可以在同一運算周期發生，保證了實時性。

圖4 速度監控計算模型

圖5 CSM區速度控制模型

在TSM區，列車已運行在一個限制速度，因此在計算防護曲線時需要著重考慮列車制動性能以及一些線路參數信息，監控邏輯與CSM區有一定區別。因此TSM區在 CSM區制動防護的基礎上又在首尾分別增加了兩級制動，控制邏輯的SSM模型見圖6。

圖6 TSM區速度控制模型

2.3 模式轉換功能建模

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

圖7 模式轉換模型

表1 模式轉換功能模型部分輸入變量含義

3 測試用例生成方法

對于生成的測試用例的質量，需要通過一定的標準進行評判，即覆蓋度準則。本文從滿足測試用例完備性的角度出發，針對SSM模型提出了一種測試用例的生成方法。根據圖論思想，SSM模型可以抽象為點和邊構成的有向圖，并可以設計算法從圖中生成測試用例。由于遷移條件均可寫成布爾邏輯表達式的形式，故本文提出可以依據MC/DC覆蓋準則，從抽象的測試用例生成測試腳本，得到可執行的最小測試用例集。

3.1 模型轉換

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

圖8 模式轉換功能模型的狀態轉換

根據全遷移覆蓋準則，系統應首先到達一個狀態，即當前狀態。系統未開始運行時，當前狀態為規定的初始狀態。若遷移被觸發，則系統轉換到下一狀態。相較于其他覆蓋度準則，全遷移覆蓋所需的測試用例較少。由于二元圖中節點的可達性[12]，為實現上述目標，將狀態轉換圖中的t0～t37轉換成節點，即T0～T37，將S0～S8根據狀態轉換圖中的遷移關系添加為T0～T37之間的有向邊，則可以將狀態轉換圖轉化為遷移路徑圖，遍歷遷移路徑圖則可以生成全遷移覆蓋準則下的抽象測試用例。

算法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 全遷移覆蓋測試用例生成

抽象測試用例的生成是本文提出的測試用例生成方法中的第一步，但并不是最關鍵的一步，只需確保滿足對全部遷移的覆蓋性，因此，采取圖的遍歷算法中常用的深度優先搜索算法對遷移路徑圖進行遍歷。直到搜索到的節點為終止節點，則表明一條測試用例生成成功。經過試驗得到的抽象測試用例結果見表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的具體測試用例集生成

基于模型生成的測試用例并不能直接輸入到被測系統中執行，還需要基于數據將其轉換成可執行的測試腳本。為確保轉換過程中測試腳本的覆蓋度依然可以滿足測試過程中對于完備性的要求，在轉換過程中同樣需要滿足一定的覆蓋度準則。MC/DC覆蓋準則是一種結構覆蓋方法，但其更注重每個條件對結果產生影響的獨立性，可以保證覆蓋每個可能的結果，并且每個條件對結果的獨立影響作用都能得到體現，因此采取MC/DC覆蓋準則的思想進行下一步的算法設計。

快速生成算法專門針對MC/DC覆蓋度準則設計，直接對布爾表達式進行處理，是一種快速高效的MC/DC覆蓋度算法。將任意布爾表達式抽象成一個條件為葉節點、判定為根節點的語法樹。為體現影響條件的獨立性，限制右子樹的節點，將可以影響判定結果的條件置于最左側子葉的位置，對語法樹的左右子樹進行置換，這樣不會影響判定的結果[13]，但可以讓每個條件獨立影響判定結果一次。

表2 抽象測試用例

算法中主要有當前條件、直接判定、前置條件、默認數據以及自由條件等幾個概念[13]。針對任一布爾邏輯表達式，首先設計一個結構體，用于存放布爾表達式中每一元素的屬性、默認值以及當前值。數組ArrayList用于存放指向結構體的指針，遍歷此數組則可以得到當前條件。在初始狀態時設置第一個條件為當前條件，其測試數據取0、1兩種情況，其余條件的測試數據取默認值。

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

輸入: Str value //將布爾邏輯表達式及其默認值寫成string類型的數據

輸出: TestCases[] //輸出為一個由bool數據構成的二維數組

1：ArrayList[]=getArray(Str)

2：PresentValue=getDefauleValue()

3：getTestCase()

4：fori

5： if Condition then

6： PresentValue=!getDefaultValue() //默認數據取反設為當前條件值

setPreCondition(getDefaultValue()) //當前條件的默認值傳遞給前置條件

7： addTestCaseto TestCases[]

8： end if

9：end for

算法3中涉及的主要函數見表3，其中setPreCondition()函數為該算法中的一個核心步驟，用于尋找前置條件。顧名思義，前置條件即位于當前條件之前的條件，但如果當前條件之前為右括號，則需要尋找到與其對應的左括號之后的一個條件，并將其設置為前置條件；若當前條件之前為左括號或數組盡頭，則搜索過程結束。

表3 快速生成算法子函數

對于表2中的抽象測試用例，均可通過快速生成算法進行處理，最終可以得到滿足全遷移覆蓋和MC/DC覆蓋準則的可執行測試用例集。

4 測試用例分析評估

根據以上算法設計的測試用例集生成工具，通過計算機語言C#進行了編程實現，將生成的測試腳本導入SCADE中，通過SCADE配套的測試分析環境SCADE QTE對覆蓋度進行分析，并采用變異分析的方式對測試用例的完備性進行了評估。

SCADE中的認證級測試環境(Qualified Test Environment, QTE)，可以支持在主機上的功能測試，以及模型和代碼的覆蓋分析。SCADE QTE支持在主機上仿真目標機上的測試執行過程，可以對測試用例質量的評估提供強有力的支撐，并且方便后續在目標機上執行測試。在SCADE QTE上生成的覆蓋度分析報告表明，測試用例對模型的狀態覆蓋率與結構覆蓋率都達到了100%，MC/DC覆蓋率為74.3%，這是由于為保證全遷移測試的完備性，在基于MC/DC覆蓋準則生成測試數據時，選擇剔除了不能使每條測試用例完整執行的情況。

變異分析是一種通過評估測試用例檢測出錯誤的能力，來評價測試用例好壞的分析方法。首先對待檢測的模型進行變異，產生一系列的變異模型，然后在模型中運行測試用例，若能夠檢驗出變異模型和原始模型的差異，則證明測試用例是有效的。在本文用于生成測試用例的SSM模型中，通過增加、減少狀態、遷移，以及改變邏輯運算符等方式產生變異模型。變異評分的計算公式為

(2)

式中：MS(P,T)為變異評分；DM(P,T)為被發現的變異體數目；M(P)為變異體總數；EM(P)為等效變異體數。

在試驗中，通過對車載ATP模式轉換功能模型進行改變邏輯運算符、遷移條件等變異，可以得到102個變異體。具體變異類型與數量見表4。

對變異測試結果進行變異評分的計算結果見表5。從表5可知，生成的測試用例在檢測邏輯運算符變異以及遷移條件變異時評分均為1，這說明發現了絕大多數的變異，檢測效果較好，結果具有很強借鑒意義。

表 4 變異類型及數量

表5 變異結果

5 結束語

本文針對SCADE模型，提出了一種生成具體可執行測試用例集的方法。首先，被測系統的模型要在可以滿足安全苛求系統可靠性要求的開發環境SCADE中進行建立；其次，由于基于模型生成的滿足全遷移覆蓋度準則的測試用例是抽象的，不能直接應用于測試，因此本文結合滿足MC/DC覆蓋度準則的算法，將其轉化為可執行的測試用例集。以CTCS-3級車載ATP系統模式轉換功能為例，對此方法進行了驗證實驗，并在SCADE中運行測試腳本，采用變異分析的方法對測試用例的質量進行了評估。最終證明該方法可以滿足覆蓋度需求，測試完備度較高，可以提升測試自動化水平。