基于模型的车载设备测试用例自动生成研究

易承龙，李开成，周晶晶

(北京交通大学轨道交通运行控制系统国家工程研究中心，北京 100044)

2004年，铁道部提出“四横四纵”铁路快速客运专线网建设规划，从此启动了中国高速铁路发展计划。随着铁路事业的快速发展，列控系统的安全性也成为了人们关注的焦点[1]。作为列控系统核心的车载设备在正式使用前必须进行全面测试，测试的基础是测试用例的生成。目前，车载设备测试用例是根据专家经验通过启发的方式得到，这种方式既耗时，又不能保证测试用例的覆盖度[2]；因此，有必要在保证测试覆盖度的前提下将测试用例的生成过程自动化。

1 列控系统车载设备测试现状

现阶段，CTCS-3级车载设备的测试是通过系统既有的外部接口进行功能测试，采用的是黑盒测试及主动测试方法[3]。功能测试由系统功能需求规范提取出功能特征，依据功能特征编写测试用例，然后由测试用例串联成测试序列[3-5]。 目前，由功能特征设计测试用例的过程主要由手工完成，测试的效率低、耗时长，并且随着测试规范和测试目的的改变，测试工作量增大。测试用例编写人员需要对系统深入了解，并且具备丰富的测试经验，即使这样在测试用例的编写过程中也难免有所遗漏。显然，使用这种方法编写的车载设备测试用例往往难以保证测试质量，因此有必要将测试用例生成的过程模型化、自动化。国内外众多专家的研究表明基于时间自动机模型的测试可以有效地提高车载设备的测试效率[6]。

2 时间自动机及Cover简介

时间自动机是由R.Alur和D.Dill提出的，作为实时系统建模的方法，它为实时系统建模提供了快速易用的形式化方法[7]。首先，时间自动机引入了系统在某些状态之间的转移，这些状态用位置元素来表示。其次，时间自动机在有限状态机的基础上引入了时间变量，这不仅可以记录模型状态转移间所消耗的时间，同样可用作判定是否应该发生状态转移的条件。

Cover是一个基于模型的实时系统测试用例自动生成工具，由Uppsala大学开发并于2005年推出，它有一个表达能力很强的observer语言，可以用来描述一大类覆盖准则，包括结构准则(如位置或边覆盖)、数据流准则(如定义使用对和语义覆盖等)，能够实现从时间自动机模型到基于覆盖度算法的测试用例套的自动转换[8]。

3 基于UPPAAL的列车运行场景建模

车载设备是一个典型的实时系统，系统的安全性要求系统不仅要做出正确的响应，还必须在规定的时间内做出响应。此外，列控系统出现故障之后，能否在规定的时间内实现“故障-安全”也是关系列车安全运行的关键因素，因而列控系统的时间特性可以由时间自动机模型很好地反映。本文运用时间自动机理论形式化描述列控系统注册与启动场景，并从功能要求和性能要求2方面对模型进行验证。

3.1 列车注册与启动场景介绍

注册与启动场景[9]描述的是列车从站内或区间车载设备从停止状态开始，依次经过设备上电、激活并开启驾驶台、输入列车数据、具备发车条件至列车启动时信号系统的整个工作流程。其工作流程如图1、图2所示。

图1 注册场景流程图

图2 启动场景流程图

3.2 列车注册与启动场景建模与验证

通过以上对系统流程的分析，注册与启动场景关系到司机、EVC和RBC之间的信息交互，所以需要使用UPPAAL分别对司机、EVC和RBC建立时间自动机模型。

3.2.1 司机模型

在列车注册与启动场景中司机扮演重要角色，EVC通过DMI与司机进行交互，提示司机输入信息或进行确认，其UPPAAL模型如图3所示。

图3 司机模型

司机模型的时间自动机定义为：

TA=

初始位置L0= {DriverInActivity};

位置集合L={DriverInActivity,DriverActivity, WaitToConRBC,ConToRbcReady,ReadyToGo,Go}

事件集合A={InputDriverID , InputDriverIDReady, EVCConWithRbc, TurnToC2SOM, InputVCData, InputVCDataReady, ReadyToStart……

状态转移E={,,

3.2.2 EVC模型

在列车注册与启动场景中，EVC逻辑最为复杂，它需要同时与RBC和司机进行交互，其UPPAAL模型如图4所示。

图4 EVC模型

3.2.3 RBC模型

在列车注册与启动场景中，RBC负责与EVC进行信息交互，RBC功能的正确是列车行车安全的保障，其UPPAAL模型如图5所示。

由于篇幅有限就不再罗列EVC、RBC自动机模型的位置集合、事件集合等信息。列车注册与启动场景模型建立完成后，利用UPPAAL软件自带的模拟器检查是否有语法错误。在通过语法编译后，点击自动运行按钮，通过比较发现运行结果与规范中的流程图完全一致，整个模型所完成的功能和性能要求如下：

图5 RBC模型

1)功能要求。

A[] not deadlock

系统没有死锁；

E<>((VC.VCWaitM3)and(RBC.RBCWaitM132))

RBC能定时接受车载发送的MA请求并向车载发送最新MA；

E<>((VC.VCWaitM24)and(RBC.RBCWaitM136))

车载设备能定时向RBC发送列车实时位置信息并收到RBC回复。

2)性能要求。

A[] VC.VCWaitM3 imply T_MaReq >MAReqPer-iod

车载设备周期向RBC发送请求MA；A[]VC.VCWaitM24 imply T_PositionReport >

PosRepPeriod

车载设备周期向RBC发送位置报告信息；

A[]VC.EditonJudgeStu imply ConnectNum <=TryToConNo

车载设备与RBC建立安全连接尝试呼叫的次数小于3次；

A[] VC.EditonJudgeStu imply T_Con <=T_NVCONTACT

车载设备与RBC建立安全连接时间不超过60 s。

在UPPAAL软件验证器中执行上述验证语句，结果显示上面所描述的性质都能通过，表明系统满足这些性质，模型是安全正确的，这为后面测试用例自动生成提供了正确的前提。

4 车载设备测试用例的自动生成

本文首先介绍了基于模型测试的原理和过程，然后引入基于覆盖度算法的辅助软件Cover，自动生成了车载设备的测试用例。

4.1 基于模型的测试原理

首先叙述一个事实：基于模型的测试序列自动生成方法应用的前提条件是假设系统是TITOS系统，也就是说对于每一个测试用例的输入，系统都有一个对应于系统详细设计中所描述的明确输出，车载设备满足这个条件。假设系统A是实时系统，它由2个部分组成，分别是系统模型S和系统所在的环境E。时间自动机在运转时，组成系统的各个部件在时钟约束的条件下从一个状态到达另一个状态形成一条序列，而特征轨迹就是序列的集合。利用UPPAAL对可达性问题分析产生的特征轨迹可用以下数学公式表达：

其中：si和ei分别是系统模型S和运行环境模型E的状态；ri是时间延迟或者其他同步动作。系统延迟和其他同步动作组成了测试用例中的事件因子，因此从特征轨迹到测试用例的转换，最简单的方法就是通过将特征轨迹映射到系统环境模型E中，叠加相关联的系统延迟，去掉不可见的转换过程，最后，将要在真实环境中执行的测试用例引入判决。其判决过程可以解释如下：时间自动机中某个状态用一个Bool类型变量标识，可以标识Pass和Fail状态，如果测试序列不能执行到这个状态，那么他将被标识为Fail状态，如果能执行经过这个状态，他将被标识为Pass状态。

4.2 车载设备测试用例的自动生成

4.2.1 Cover工具配置

在用Cover自动生成测试序列之前，必须对Cover进行相应的配置，相关配置参数如表1所示。

表1 Cover工具配置参数

Cover工具需要输入Model.xml文件、Observer.obs文件和Property.q文件。

Model.xml文件即上一节使用UPPAAAL软件建模所生成的文件，需要拷贝到Cover工具所在的根目录下。

Observer.obs文件用于描述覆盖标准算法。其使用非常灵活，具体语法结构形式如下所示，以下所描述的为全位置覆盖标准。

observerObserver(procid P; )

{

node edgeNode(edgeid);

rulestartto edgeNode(E)with E :=edge(P);

accepting edgeNode;

}

Property.q文件用于配置Cover工具选择生成哪个时间自动机模型的测试例，其语法结构形式如下：

CoveredgeObs({P1,P2})

在这里，时间自动机过程集为{P1,P2}，也就是说P1和P2会分别代入Observer文件中的procid P进行运算。

4.2.2 测试用例的自动生成

根据上一节描述的配置方法配置Cover工具，并将XML格式的注册与启动场景的UPPAAL模型和使用全位置覆盖标准算法的Observer.obs文件拷贝到Cover程序所在的文件夹的根目录，运行Cover工具。将生成的测试案例用例保存在abc.tr文件中，运行结果表明共生成了7个测试案例。下面以Trace#1为例，介绍所生成的抽象语言描述的具体含义。Trace#1的具体描述如下：

·Trace #1:

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN

edgeN……

可以将以上所生成的抽象状态转移语言转换具体的状态转移图，这样所生成的测试用例的消息序列为：“初始状态”—“待机状态”—“准备建立连接状态”—“等待消息32状态”—“判断连接是否超时状态”—“判断系统版本状态”—“建立连接状态”—“等待配置参数状态”—“等待输入列车数据状态”—“等待列车数据确认状态”—“等待发车状态”—“正常工作状态”—“等待行车许可状态”—“发送列车位置报告状态”。

通过对比《CTCS-3级列控系统测试案例》中功能特征47的测试案1的基本信息和测试步骤，可以发现，其所描述的事件与Cover工具所生产的Trace#1相吻合。由上面的案例可知，利用时间自动机建模不仅可以验证模型的可达性，还可以通过搜索路径生成覆盖度完整的测试用例，并且可以通过配置Cover工具搜索算法改变测试用例的路径选择。

5 结束语

传统的车载系统功能测试用例生成主要依靠专家经验手工编制完成，测试的主观性强、效率低、耗时长，并且随着测试规范和测试目的的改变，测试工作量大，而且测试的覆盖度无法得到满足。本文提出了一种基于模型的车载系统安全测试用例自动生成方法，使用UPPAAL软件对列车注册与启动运营场景进行建模，并从功能和性能2方面对所建立的模型进行了验证，最后运用基于覆盖度的工具Cover自动生成车载设备测试用例，这为复杂时变系统测试用例的自动生成提出了一种新的思路。

[1]唐涛. 高速铁路列车运行控制系统车载设备安全性设计[J]. 北方交通大学学报,1999:23(5):83-87.

[2]王超琦.CTCS-3级列控系统车载设备测试序列的生成方法及工具研究[D].北京: 北京交通大学,2010:5-27.

[3]Beizer B . Black-Box Testing: Techniques for Functional Testing of SoftWare and Systems[M]. New York:John Wiley & Sons:1995:160-165.

[4]王倩倩.CTCS-3级列控系统测试案例优化生成方法研究[D].北京：北京交通大学， 2010:16-17.

[5]章慧.CTCS-3级列控系统车载设备测试方法研究[D].北京：北京交通大学，2007.

[6]范素娟.基于时间自动机模型的测试用例生成方法研究[D].郑州：郑州大学，2010.

[7]Alur R,Dill D L A.Theory of Timed Automata[J]. Theoretical Computer Science,1994,126:183-235.

[8] 范素娟,庄雷.基于时间自动机模型的测试用例生成方法[J]. 计算机工程与设计,2010(12): 2765-2768.

[9]张曙光.CTCS-3级列控系统总体技术方案[M].北京:中国铁道出版社, 2008:6-8.