基于變異模型的CTCS-3級列控系統測試用例自動生成方法研究

劉曉亮，袁 磊，呂繼東，魏國棟，富德佶

（1.北京交通大學 軌道交通控制與安全國家重點實驗室，北京 100044；2.北京交通大學 軌道交通運行控制系統國家工程研究中心，北京 100044）

計算機與通信信號

基于變異模型的CTCS-3級列控系統測試用例自動生成方法研究

劉曉亮1，袁 磊1，呂繼東2，魏國棟2，富德佶1

（1.北京交通大學 軌道交通控制與安全國家重點實驗室，北京 100044；2.北京交通大學 軌道交通運行控制系統國家工程研究中心，北京 100044）

本文提出一種基于變異模型的CTCS-3級列控系統測試用例自動生成方法。根據列控系統需求規范，建立它的SMV（Symbolic Model Verif i er）模型，對此模型進行變異，將變異之后的模型輸入到模型檢驗器SMV中，利用模型檢驗生成反例的技術，自動生成測試用例，提高了測試用例的生成效率。并以CTCS-3級列控系統的無線閉塞中心（RBC）切換場景為例，驗證了該方法的有效性。

變異模型；列控系統；測試用例；模型檢驗；SMV

列車運行控制系統（以下簡稱：列控系統）是確保列車運行安全、提高運輸效率的鐵路基礎設備[1]，只有其功能和性能都符合系統需求規范的要求，才能保證列車的安全運行，因此在系統投入使用前，要對其進行全面的測試。

測試用例是測試的基礎，傳統的高速鐵路信號系統測試用例生成主要由手工完成，然而手工生成測試用例效率低、耗時長、工作量大。隨著計算機技術的發展，基于模型的測試用例自動生成逐漸成為一種趨勢，該技術可以提供可選擇的、自動化的測試用例，能夠有效的避免手工生成測試用例所帶來的問題，提高測試用例的測試效率[2]。

變異測試是一種行之有效的軟件測試方法，可用來生成完備的測試用例集[3]，基于模型檢驗的測試是形式化方法的一種，其可以避免人工失誤，提高測試效率[4]。因此，本文將變異和模型檢驗相結合，提出一種基于變異模型的CTCS-3級列控系統測試用例自動生成方法。并以CTCS-3級列控系統RBC切換場景為例，使用該方法生成系統的測試用例。

1 變異測試概述

變異測試是一種基于錯誤的軟件測試技術。在變異測試中，通過將小錯誤人為地引入源程序，生成程序的錯誤版本，這些錯誤版本被稱為源程序的變異體，而且每個變異體都只包含一個錯誤，而這樣引入錯誤的行為被稱為變異，而這些變異操作的規則被稱作變異操作符（Mutation Operator），每個變異操作符對應于一類簡單的錯誤[5]。

變異測試始于20世紀70年代，最早是由Hamlet和DeMillo等人提出[6]，在近幾十年得到國內外學者的廣泛關注，并且研究人員對此領域進行了深入的研究并發表了大量的研究論文[6～8]。隨著變異測試的發展，它可以用來生成測試用例，例如文獻[8]利用變異為系統規范生成測試用例。

2 基于變異模型的測試用例自動生成方法

基于變異模型的測試用例自動生成方法框架如圖1所示，為4步：（1）根據系統需求規范，建立系統的SMV模型；（2）提取變異操作符，應用到模型中，得到系統的變異模型；（3）利用模型檢驗器SMV，自動生成反例；（4）從反例中提取測試用例。

圖1 基于變異模型的測試用例自動生成方法

本文提出的基于變異模型的CTCS-3級列控系統測試用例自動生成方法的第2、3步是本文的研究重點，即如何提取變異操作符、生成系統的變異模型，以及如何利用模型檢驗器（SMV，Symbolic Model Verifier）生成反例。

2.1 列控系統的SMV模型

由于本文要利用SMV產生反例，因此利用SMV語言來建立列控系統需求規范的模型。

SMV語言描述的系統由若干模塊（MODULE）構成，其中有且僅有一個main模塊，它是SMV中的主模塊，也是程序執行的入口點。其他模塊可以根據需求進行創建和命名，由main模塊調用[9]。

SMV語言中用計算樹邏輯（CTL，Computation Tree Logic）公式描述系統待驗證的性質，系統性質說明在SMV中以關鍵詞SPEC開始，其一般形式為：SPEC CTL公式。

2.2 變異操作符與變異模型

變異測試的關鍵環節就是定義變異操作符。變異操作符定義了從原有模型到變異模型的規則，從而將原有模型轉化為變異模型，決定了變異模型的好壞，是基于變異模型的測試基礎。因此變異操作符的選取直接決定著變異測試的測試效率。

列控系統的需求規范規定了系統在運行過程中，需要做出一些條件判斷，從而選擇執行相應的分支。所以本文主要考慮列控系統需求規范分支處條件判斷的錯誤的情況。這里的條件可以是一個布爾變量，也可以是一個關系表達式。本文根據列控系統的特點，以及結合文獻[10～12]提出的變異操作符，提取了以下幾個變異操作符：

（1）布爾運算符替代操作符（BOR，Bool Operator Replacement），一個運算符被另一個運算符替代。

（2）表達式取反操作符（ENO，Expression Negation Operator），將一個表達式取反。

（3）布爾值替代操作符（BRO，Boolean-value Repa-lcement Operator），用True（1）或False（0）代替一個表達式。

（4）常量替換操作符（CRO，Constant Repalcement Operator)，用一個常量替換另外一個常量。

提取完變異操作符之后，將變異操作符應用到列控系統的模型中，會得到很多個列控系統的變異模型。如表1列出布爾運算符替代操作符應用到一模型中，得到的變異模型，此變異操作符將布爾運算符“|”改成布爾運算符“&”。例如：原模型p的條件表達式if ( x | y )經過此變異操作符的變異之后得到了表達式if ( x &y )，從而得到了變異模型p'。

通過以上方法，利用不同的變異操作符，可以得到很多個變異模型。

2.3 測試用例自動生成

本文的測試用例自動生成方法是基于變異和模型檢驗的。變異如前所述，模型檢驗是指用SMV語言描述系統功能需求，得到系統模型，再利用CTL語言描述系統的性質和模型檢驗工具SMV驗證系統是否滿足這些性質。如果不滿足，SMV就會輸出一條不滿足這一性質的反例。從測試的角度來看，反例提供了一種構造測試用例的有效途徑[13]。模型檢驗的原理如圖2所示。

表1 布爾運算符替代操作符

圖2 模型檢驗的原理

3 RBC切換場景的建模和測試用例自動生成

3.1 RBC切換場景

無線閉塞中心（RBC）是CTCS-3級列控系統的重要組成部分，它為列車提供移動授權（MA）來保障列車的安全運行。當列車在線路上運行并到達某個RBC控制區域邊界時，列車從當前RBC（“移交RBC”）控制區域進入到下一個RBC（“接收RBC”）控制區域，列車控制權限從移交RBC轉換到接收RBC的過程稱為RBC切換[14]。RBC切換方式分為2種：一部車載電臺正常和兩部車載電臺都正常。以只有一部車載電臺正常的RBC切換的方式為例，其切換流程如下：

（1）列車在“移交RBC”控制下運行。當列車通過RBC切換預告應答器之后，車載設備向“移交RBC”發送列車位置報告。

（2）當“移交RBC”收到位置報告后，向車載設備發送RBC切換命令，并向“接收RBC”發送列車預告信息和進路請求信息。

（3）“接收RBC”向“移交RBC”發送進路相關信息，并且“移交RBC”根據接收到的進路信息，向車載設備發送延伸至接收RBC區域內的行車許可。

（4）當列車頭部通過切換邊界后，車載設備向“移交RBC”發送列車位置報告，“移交RBC”將此位置報告轉發給“接收RBC”，“接收RBC”向“移交RBC”發送接管列車信息。

（5）當列車尾部通過切換邊界后，車載設備向“移交RBC”發送列車位置報告，然后“移交RBC”斷開與車載設備的通信會話，同時將其從“移交RBC”的列車清單中刪除。

（6）車載設備與“接收RBC”建立通信會話。（7）列車在“接收RBC”的控制下運行。

3.2 RBC切換的模型

在RBC切換過程中，列車需要與RBC、應答器等設備進行信息交互，因此，RBC切換過程的SMV模型中包含RBC模塊、列車模塊、應答器模塊[15]。所建立的模型片段如下所示：

--************************* --MAIN MODULE

MODULE main()//主模塊

……

--********RBC MODULE ********

MODULE RBC()//RBC模塊

……

--****** TARIN MODULE()******

MODULE TARIN()//列車模塊

……

--********Balise MODULE ********

MODULE Balise()//應答器模塊

……

同時，根據RBC切換場景，在主模塊中定義了如下幾個主要的變量：rbcHandover（移交RBC）、rbcAccept（接收RBC）、train（列車）、balise（應答器）。每個模塊都有自己的方法和變量，如表2所示。

3.3 RBC切換的變異模型

根據前述的方法，需要將4個變異操作符應用到RBC切換的模型中，得到RBC切換的變異模型。例如:將布爾值替代操作符應用到RBC切換的模型中，即利用布爾值“FLASE”替代了變量“handover”，得到了變異模型，模型片段如下所示。

--****** 原模型******

rbcAcc_control:=handover &

表2 變量和方法的含義

rbcAccept.RBC_Connect_Train=TRUE

……

--****** 變異模型******

rbcAcc_control:=FALSE &

rbcAccept.RBC_Connect_Train=TRUE;

……

將以上4個變異操作符應用到RBC切換的模型中，每個變異操作符都會產生大量的變異模型，這些變異模型可以用來生成測試用例。

3.4 測試用例自動生成

將上文生成的變異模型輸入到SMV中，利用模型檢驗原理生成反例。有的變異模型會產生多個反例，不會產生反例。表3展示了每個變異操作符產生的變異模型的數量，以及生成反例的數量。

表3 變異模型和反例的數量

如下所示，展示了模型檢驗器SMV產生的一個反例的路徑：

--****** Counterexample Trace******

-＞ State: 1.1 ＜-

rbcHandover.RBC_Control_Train = TRUE

rbcHandover.RBC_Connect_Train = TRUE

rbcAccept.RBC_Control_Train = FALSE

rbcAccept.RBC_Connect_Train = FALSE

train.train_position = IniPos

train_level = C3

-＞ State: 1.2 ＜-

balise.PreBalise = TRUE

train.train_position = PrePos

-＞ State: 1.3 ＜-

balise.PreBalise = FALSE

balise.ExeBalise = TRUE

train.train_position = HeadExePos

-＞ State: 1.4 ＜-

rbcHandover.RBC_Connect_Train =FALSE

train.train_position = TailExePos

rbcHov_disconnect = TRUE

-＞ State: 1.5 ＜-

train.train_position =TailExePos_10s

train_TailExePos_10s = TRUE

-＞ State: 1.6 ＜-

train.train_position =TailExePos_20s

train_TailExePos_20s = TRUE

-＞ State: 1.7 ＜-

train.train_position = TailExePos_30s

train_TailExePos_30s = TRUE

-＞ State: 1.8 ＜-

train.train_position = TailExePos_high40s

train_c2_1 = TRUE

rbcAccept.RBC_Connect_Train = FALSE

-＞ State: 1.9 ＜-

train.train_position = EndPos

train_level = C2

可以提取上圖的反例路徑得到測試用例，這個測試用例的具體含義為：列車被“移交RBC”控制，在CTCS-3等級下運行→列車車頭通過預告應答器位置→列車車頭通過執行應答器位置→列車車尾通過執行應答器，并與“移交RBC”斷開連接→列車運行超過40 s，還未與“接收RBC”連接上→列車降級到CTCS-2等級運行。

通過以上分析，此反例生成的測試用例的測試目的是，當列車與“移交RBC”斷開連接到與“接收RBC”建立通信會話，如果此連接超過系統允許的40 s，查看列車是否會降至CTCS-2級系統運行。

4 結束語

本文提出了基于變異模型的CTCS-3級列控系統測試用例自動生成方法。建立系統的SMV模型，通過變異將錯誤注入到模型中，得到變異模型，將變異模型輸入到模型檢驗器SMV中，利用模型檢驗生成反例的技術，自動生成測試用例，以更好地滿足列控系統測試的要求，并且提高了測試效率。通過對典型場景RBC切換進行建模，并生成其有關的測試用例，驗證了此方法的有效性。

[1] 唐 濤．列車運行控制系統[M]．北京：中國鐵道出版社，2012．

[2] 袁 磊，呂繼東，劉 雨，等．一種全覆蓋的列控車載系統測試用例自動生成算法研究[J]．鐵道學報，2014，36（8）：55-62．

[3] 劉新忠，徐高潮，胡 亮，等．一種基于約束的變異測試數據生成方法 [J]．計算機研究與發展，2011，48（4）：617-626．

[4] 金 丹．安全計算機平臺測試序列的生成及應用[D]．北京：北京交通大學，2013．

[5] 陸毅明．面向對象程序的變異測試方法研究—基于代數式規格的變異測試系統的研究與實現[D]．上海：上海交通大學，2007.

[6] Hamlet R G. Testing programs with the aid of a compiler[J]. IEEE Transactions on Software Engineering, 1977, 3(4): 279–290．

[7] 單錦輝，高友峰，等．一種新的變異測試數據自動生成方法 [J].計算機學報，2008，31（6）：1025-1034．

[8] Ammann P E, Black P E, Majurski W. Using model checking to generate tests from specifications[C]. Formal Engineering Methods,1998. Proceedings. Second International Conference on. IEEE, 1998: 46-54．

[9] 郭文章．ATS系統內部通信協議的設計及形式化驗證[D].北京：北京交通大學，2009.

[10]張 巖．列車運行控制系統軟件故障相關形式化測試方法[D]．北京：北京交通大學，2012.

[11] Ammann P, Ding W, Xu D. Using a model checker to test safety properties[C]. Engineering of Complex Computer Systems, 2001. Proceedings. Seventh IEEE International Conference on. IEEE, 2001: 212-221．

[12] Black P E, Okun V, Yesha Y. Mutation of model checker specif i cations for test generation and evaluation[M]. New York. Springer US, 2001: 14-20．

[13] Okun V. Specification mutation for test generation and analysis[D]．University of Maryland Baltimore County, 2004.

[14]中華人民共和國鐵道部．CTCS-3級列控系統系統需求規范（SRS）[S]．北京：中國鐵道出版社, 2009．

[15]呂繼東，唐 濤．高速鐵路列控系統運營場景實時性的建模與驗證[J] .鐵道學報，2011，33（6）：54-61.

責任編輯 徐侃春

Mutation model-based generation of test cases for CTCS-3 Train Control System

LIU Xiaoliang1, YUAN Lei1, LV Jidong2, WEI Guodong2, FU Deji1
( 1. State Key Laboratory of Rail Traf fi c Control and Safety, Beijing Jiaotong University, Beijing 100044, China; 2. National Engineering Research Center of Train Control System, Beijing Jiaotong University, Beijing 100044, China)

Based on mutation model of CTCS-3 Train Control System, this paper proposed a mutation model-based method to generate test cases automatically. According to the requirements specif i cation of Train Control System, the SMV model was established and mutated. The mutated model was put into the SMV model checker. The test case was generated automatically by using the model checking methods and the eff i ciency of the test case generation was improved dramatically. Finally, a scenario of Radio Block Center (RBC) handover in CTCS-3 Train Control System was taken as an example, verif i ed the effectiveness of the method.

mutation model; Train Control System; test case; model checking; SMV

1005-8451（2015）06-0054-05

2014-11-13

北京高等學校青年英才計劃項目（YETP0580）；中央高校基本科研業務費專項資金資助（2014JBM022）；國家自然科學基金資助項目（61304185）。

劉曉亮，在讀碩士研究生；袁 磊，講師。

U284.482∶TP39

A