基于变异模型的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