基于模型的CTCS-3 级列控系统测试案例自动生成方法

吕继东， 朱晓琳， 李开成， 唐 涛， 王海峰

(1. 北京交通大学轨道交通运行控制系统国家工程研究中心，北京100044;2. 中国铁道科学研究院通信信号研究所，北京100044;3. 北京交通大学轨道交通控制与安全国家重点实验室，北京100044)

作为典型的安全苛求系统，列控系统功能的任何故障都可能造成巨大的生命和财产损失［1］. 形式化方法和测试方法是保证列控系统功能正确性的两个重要途径，在列控系统开发生命周期中起着不同的作用.

形式化方法一般用于列控系统开发的前期，已广泛用于列控系统需求规范的功能正确性研究［2］.早期列控系统的形式化研究主要使用时段演算方法(duration calculus，DC)［3］. 然而，时段演算不能完全满足列控系统的形式化建模要求，随着列控系统复杂度的提高，系统中诸如期限(deadline)、直到…才(wait until)、超时(time out)等形式化描述存在一 定 的 不足［4］. 进程代 数(process algebra)通过描述并发和通信系统为分析离散事件系统提供了结构化方法［5］，其中，HCSP(hybrid communication sequential process)方法是对CSP(communication sequential process)的一种扩展，广泛应用于列控系统功能正确性研究［6］. 一致性测试是保证系统功能正确性的另一个重要手段，一般用于列控系统开发的后期.通过分析被测系统(system under test，SUT)与其需求规范之间的关系，验证系统的功能是否与需求规范一致［7］. 国内外列控系统功能一致性测试的研究主要集中在测试案例生成方法上［8-10］.

CTCS-3 级列控系统功能复杂，涵盖了注册与启动、注销、等级转换、行车许可、RBC(radio block center)切换、自动过分相、重联与摘解、临时限速、降级情况、调车作业和特殊进路等14 个典型的运营场景.运营场景之间具有顺序和并发等特点(例如，行车许可场景和注册与启动场景之间是顺序关系，但与RBC 切换场景是并发关系).运营场景需求规范中包含了若干个并发执行和交互的实时计算构件，规定了车载设备和RBC 设备接口信息时序约束［11］.上述研究主要集中在列控系统单个运营场景时序约束行为的正确性上，对整个列控系统层次的建模描述鲜有研究;并且不同运营场景存在不同的时序约束(例如超时(TimeOut)、期限(deadline)、直到…才(wait until)等等)，针对这些时序约束的建模与验证也存在不足.形式化方法应既能在列控系统层次上描述不同运营场景之间的关系，又能在运营场景层次上描述接口信息交互行为的时序约束，因此，结合运营场景需求规范的特征和特点选择合适的形式化方法是研究的难点.

另一方面，列控系统具有实时性、混杂性等特点，系统功能的正确性不仅要求逻辑功能的正确性，而且要求在规定的时间约束内做出正确的逻辑响应.不同的运营场景、不同的测试目的和不同的时间约束都对应不同的测试案例，功能测试面临着状态空间爆炸和时间特性测试的问题. 例如，在列控系统运营场景中，RBC 根据接收到车载设备发送消息的时间，结合运营场景中的时间约束要求，在规定的时间内必须输出对应的逻辑功能(正常的移动授权或紧急制动).针对运营场景接口信息交互的时序特点，选择恰当的测试目的，进行高效的测试案例自动生成，并形成涵盖列控系统所有运营场景的测试套，是研究的另一个难点.

本文基于HCSP 和TA(timed automata)理论［12］，提出了一种基于模型的列控系统测试案例生成方法.首先，结合列控系统运营场景之间的执行特点，利用HCSP 的顺序和并发操作进行了列控系统功能的形式化建模;其次，利用HCSP 支持中断机制(通讯中断、时间中断等)的特点，针对相关运营场景内部组件交互的时序约束(例如延迟、超时、中断等)进行了形式化建模，并通过引入转换规则，将HCSP 的一个子集转换成TA 网络模型，从而进行相关属性的验证;再次，基于时间自动机网络模型，给出了列控系统在单一运营场景执行下不同覆盖准则下(全状态、全变迁和自定义-使用)的测试案例生成算法，以及涵盖所有列控系统运营场景的测试案例套优化算法，并在此基础上，结合模型检验工具Uppaal 和CoVer，提出了一条适合于列控系统测试案例自动生成的工具链;最后，结合典型的CTCS-3 级列控系统RBC 切换运营场景，建立场景的HCSP 模型，验证了场景中时序约束的属性.结合不同的测试覆盖准则，生成了相关的测试案例套，并进行了比较分析.

1 列控系统运营场景的建模与验证方法

HCSP［13-14］是一种以CSP 为基础，引入描述混成系统中连续动态行为的微分方程，以及各种中断机制(通信中断、时间中断、事件中断等)，以期实现对外部事件引发进程迁移行为进行描述的形式化建模语言.

1.1 列控系统功能的HCSP 模型

根据CTCS-3 级列控系统总体技术方案［11］，定义一列列车从“注册与启动”到“注销”的某种运营过程，如图1 所示.

假设以上整个系统层的每个运营场景都由一个HCSP 的原子公式来描述，注册与启动场景:PS0;级间转换场景:PS1;行车许可场景:PS2;临时限速场景:PS3;自动过分相场景:PS4;RBC 切换场景:PS5;降级场景:PS6;注销场景:PS7.

利用HCSP 的顺序操作和并发操作算子，定义整个列控系统功能的HCSP 模型为

SYS≜PS0;PS1;PS2(PS3;PS4;PS5);PS6;PS7.

图1 列控系统运营场景过程Fig.1 Operation scenario process of the train control system

1.2 基于HCSP 子集的运营场景建模方法

主要研究集中在列控系统运营场景内部组件交互的时序约束行为描述上，结合列控系统运营场景的描述特点，提出了6 种更适合于列控系统场景描述的时序模型:周期性、延迟、时间等待、超时、截止期限和时间中断，并给出了适合于列控系统场景时序描述的一个HCSP 子集HCSPsub(仅考虑时间t是唯一的连续变量)，如表1 所示. 假设P 和Q 为两个进程，其HCSPsub进程的定义见表1.

表1 HCSPsub的进程定义Tab.1 Process definition of HCSPsub

1.3 基于TA 的验证方法

规则1 Stop

Stop 指系统永远不会终止的idle 进程，记作Astop，Astop=({i}，i，φ，φ，φ，{(i，true)}，φ).

规则2 Skip

Skip 指系统立即终止的进程，记作Askip，Askip=({i，f}，i，{f}，{τ}，φ，{i，urgent)，(f，true)}，{(i，τ，φ，true，f)}).

规则3 事件前缀

如图2 所示，事件前缀是指事件a 发生在时间自动机A 的任何变迁之前，记作eventprefix(a，A).

图2 事件前缀Fig.2 Event prefix

规则4 尾递归

如图3 所示，尾递归指系统永远不会终止的进程，记作recur(A，S0).

(SS0，init，FS0，Σ，C，Inv，T')，

其中:

图3 尾递归Fig.3 Tail recursion

规则5 延迟

如图4 所示，延迟主要用于描述系统执行某一段延迟时间单元的进程，记作delay(t)，

其中:

图4 延迟Fig.4 Delay

规则6 期限

如图5 所示，期限指系统执行完成进程必须在一定时间单元内，记作deadline(A，t)，

图5 期限Fig.5 Deadline

规则7 时间等待

如图6 所示，时间等待(WaitUntil)表示系统在等待某段时间后终止的进程，记作waitunitl(A，t)，

图6 时间等待Fig.6 Wait until

规则8 外部选择

如图7 所示，外部选择表示系统根据外部的事件进行动作变迁选择的进程，记作extchoice(A1，A2)，

图7 外部选择Fig.7 External choice

规则9 顺序组合

如图8 所示，顺序组合表示系统执行任务先后顺序的进程，记作seq(A1，A2)，

图8 顺序组合Fig.8 Sequential composition

规则10 超时

如图9 所示，超时描述系统通过时间段切换控制权的进程，记作timeout(A1，A2，t)，

图9 超时Fig.9 Time out

规则11 时间中断

图10 所示，时间中断描述系统通过时间点中断切换控制权的进程，记作timeinter(A1，A2，t)，

图10 时间中断Fig.10 Time interrupt

规则12 事件中断

如图11 所示，时间中断描述系统通过事件中断切换控制权的进程，记作evtinter(A1，A2，a)，

图11 事件中断Fig.11 Event interrupt

更多定义详见文献［13］.假设P 为HCSPsub的进程，A 为一个时间自动机，定义转换函数Φ:P→A为HCSPsub到时间自动机A 的映射，从而有以下转换规则:

基于上述转换规则，可以利用典型的模型检验工具Uppaal［15］进行TA 模型相关属性的自动验证分析，相关研究可参考文献［13］.

2 基于TA 模型的测试案例生成方法

在模型转换规则的基础上，利用典型的模型检验工具(Uppaal 和CoVer［16］)，给出了一条适合于列控系统测试案例自动生成的工具链. 如图12 所示，整个测试方法包括4 个步骤.

图12 基于模型的测试案例生成方法Fig.12 Model-based test case generation method

第1 步 规范分析阶段

通过分析列控系统运营场景规范，提取列控系统建模对象和验证属性. 例如，CTCS-3 级列控系统“行车许可”运营场景(PS2)中规定:

(1)RBC 能够发送移动授权信息给车载;

(2)车载能够发送给RBC 位置报告信息;

(3)车载如果在［0，T］内接收不到移动授权信息则实施紧急制动操作，其中，T 是一个大于0的常数.

第2 步 模型抽象阶段

通过对列控系统规范的分析，基于HCSPsub和TA 理论，抽象出列控系统场景规范的形式化模型.

(1)通过定义列控系统运营场景中相关对象的进程，建立列控系统运营场景的时序模型. 上述“行车许可”运营场景(PS2)的时序模型定义如下:

式中:Prbc和Pevc分别为“行车许可”运营场景中的RBC 和车载的进程;PEB为紧急制动进程(这里用stop 表示);MA 和pos 分别为移动授权信息和位置报告信息.

(2)结合1.3 节的转换规则，将列控系统的HCSPsub模型转换成TA 网络模型.上述行车许可场景的HCSPsub模型可转换成如下自动机网络模型:

Φ(PrbcPevc)=para(Φ(Prbc)，Φ(Pevc)).

由规则3、4 和9，得到RBC 的TA 模型，如图13 所示.

图13 RBC 模型Fig.13 RBC model

由规则3、4、9 和12，得到EVC 的TA 模型，如图14 所示.

结合TA 理论，RBC 和EVC 自动机时序模型的行为可以描述成:

图14 EVC 模型Fig.14 European vital computer (EVC)model

第3 步 模型建立阶段

利用UPPAAL 和CoVer 两个TA 模型检验工具，进行测试案例自动生成研究.

(1)利用建模工具Uppaal 建立TA 网络模型，并验证相关属性(安全相关属性和时间相关属性).结合上述的“行车许可”运营场景TA 模型，定义该自动机网络Uppaal 模型为R-E:

RBC EVC.

R-E 的UPPAAL 模型如下图15 所示.

图15 R-E 模型Fig.15 R-E model

(2)利用测试案例生成工具CoVer，结合不同测试准则，进行测试套的自动生成.

典型的测试案例tc(test case)可以表示成一个三元组＜input，step，output ＞，即测试输入、执行步骤和期望输出. 测试序列ts(test sequence)则为运行测试案例过程中执行的行为序列.假设被测设备为EVC，上述例子中，测试执行序列ts 可以通过时间自动机时序模型run(rbc)变迁上的输入或输出序列:

该测试序列ts 表示RBC 执行了3 条相同的测试案例tc:＜MA，NULL，pos ＞. RBC 首先执行第1条测试案例tc，向被测设备EVC 接口输入消息MA，等待期望输出消息pos，一旦收到pos，继续执行第2 条测试案例tc，直到所有测试案例执行完为止.

CoVer 利用观测器原理［16］，提供了3 种领域功能无关的覆盖准则(全状态、全变迁或者自定义-使用)，如图16(a)～(c)所示. 根据不同的测试目的，针对运营场景的自动机时序模型，给出全状态、全变迁和自定义-使用3 种测试案例自动生成算法.

图16 测试案例覆盖准则Fig.16 Test case coverage criteria

图16(a)定义了全状态覆盖准则，其包含被测进程TA 模型中所有状态的覆盖准则.

图16(b)定义了全变迁覆盖准则，其包含被测进程TA 模型中所有变迁的覆盖准则.

图16(c)定义了自定义-使用全覆盖准则，其包含被测进程TA 模型中所有自定义变量的覆盖准则.

结合本节实例，仅给出满足被测设备EVC 自动机全状态和全变迁覆盖准则下的测试序列(自定义-使用覆盖准则在第3 节介绍).

(1)全状态覆盖测试序列

根据R-E 自动机时序行为模型run(rbc evc)，构造1 条测试序列，使之在执行测试序列的过程中，被测EVC 的行为run(evc)能够经过所有EVC的状态.可直观地定义:

(2)全变迁覆盖测试序列

同理，构造1 条测试序列，使之经过所有EVC的变迁，可直观地定义:

式中:d1＜T，d2≥T，d3≥0.

第4 步 列控系统测试案例自动生成阶段

由于列控系统不同的运营场景具有不同的时序模型，通过简单叠加各个运营场景测试案例的方式，能够得到整个系统的测试案例套，然而这会造成大量重复的测试案例.为了得到在某种测试准则条件下，100%覆盖整个列控系统运营场景时序模型的测试案例集，设计了如下优化算法:

算法描述如下:

对于任何一个给定的运营场景时序模型M0和S0，定义i=0，并给定一个测试准则∅.

(1)进入循环，针对初始的运营场景时序模型，进行测试案例自动生成操作Total_TestCase，并将结果存储在ts 中;

(2)判断测试案例套Sts中是否含有ts.如果含有，则执行i=i+1，并且跳转至循环;

(3)如果不含有ts，存储ts 到Sts中;

(4)执行change_initial(Mi，Si)操作，得到下一个运营场景时序模型，执行i=i+1;

(5)循环执行步骤(1)，直到i=N 为止.

3 案例分析

3.1 RBC 切换场景

RBC 切换是指RBC 间在指定区域(切换应答器)实现对列车无缝切换［11］，如图17 所示.

根据CTCS-3 级列控系统总体技术方案内容，以两部电台的RBC 切换过程为例，HRBC 表示移交RBC，TRBC 表示接管RBC，整个切换流程如图18 所示.

图17 RBC 切换场景原理Fig.17 Principle of RBC transition scenario

图18 RBC 切换场景流程Fig.18 Process of RBC handover scenario

3.2 RBC 切换的HCSP 模型

(1)Timer 进程

Timer 进程通过通道circle 来控制HRBC、TRBC 与EVC 进程之间消息的交互.

(2)Speed 进程

Speed 进程由speed0 进程、speed1 进程、speed2进程和speed3 进程组成，通过通道acc 和Dec 模拟列车的加速和减速过程，其HCSP 模型如下:

(3)Queue 进程

Queue 进程是一个由add 进程和shift 进程组成的尾递归进程，主要完成HRBC 和TRBC 对EVC的管理功能.对应的HCSP 模型如下:

(4)HRBC 进程

HRBC 进程描述的HRBC 与EVC 之间的周期性信息交互过程，由建立链接start、建立通信会晤buildconnect、控制control、MA 计算computeMA、切换预通告pre、进路信息请求req、混合MA 计算comPmixMA、注销logout 和删除列车delete 共9 个进程组成.对应的HCSP 模型如下:

(5)EVC 进程

EVC 进程描述EVC 与HRBC 和TRBC 之间的周期性信息交互过程，由建立链接start、建立通信会晤buildconnect、发送位置报告reportPos、MA 请求MAreq、速度控制ControlSpeed、切换handover、建立链接start1、建立通信会晤buildconnect1、注销logout 和链接失败disconnect 等10 个进程组成.对应的HCSP 模型如下:

(6)TRBC 进程

TRBC 进程描述TRBC 与HRBC 和EVC 之间的周期性信息交互过程，由切换预通告pre、进路信息Routeinfo、建立链接 start、建立通信会晤buildconnect、控制control、MA 计算compMA、切换handover 等7 个进程组成.对应的HCSP 模型如下:

通过1.3 节的转换规则，将RBC 的切换HCSP模型转换成TA 网络模型，定义为TSQ-HET:

其中各个进程的转换关系如下:

如图19 所示，利用Uppaal 工具对TSQ-HET进行了仿真和验证.模型中，“!”和“?”表示自动机网络模型间信息交互的发生.

3.3 自动测试案例生成

在TSQ-HET 模型的基础上，以TSQ-HET 模型中的EVC 为被测对象(SUT)，针对3 种不同的测试案例覆盖准则(全状态、全变迁和MA(消息M3)相关的测试案例)进行了自动测试案例的生成.图20 描述了M3 相关的测试案例生成算法，依据该算法可以通过模型自动生成M3 相关的测试案例套.

如图21 所示，整个M3 相关的测试案例套包含3 部分:路径trace(trace #1)、测试案例覆盖项test case item 以及转移条件transitions.

本文给出以下3 个指标来衡量测试案例自动生成的有效性.

(1)测试套:满足相关覆盖准则的测试案例数量，以及测试案例覆盖的事件执行(EdgeN)数量.测试套的数量越大，表明测试越充分，反之亦然;

图19 TSQ-HET 时间网络自动机Fig.19 Network of TSQ-HET timed automata

图20 M3 相关的测试案例生成准则Fig.20 Test case generation criterion about M3

(2)测试时间:满足相关覆盖准则条件下，测试案例自动生成的时间. 时间越短，表明测试案例生成效率越高，反之亦然;

(3)内存消耗:满足相关覆盖准则条件下，CoVer 软件消耗的内存大小. 内存消耗越小，表明测试案例生成效率越高，反之亦然.不同测试准则下的测试套比较见表2.

图21 EVC 的测试套Fig.21 Test suites of EVC

表2 从测试套(案例数量、测试案例覆盖项)、测试时间和内存消耗3 个方面，对3 种不同的测试案例覆盖准则(全状态、全变迁和MA(消息M3)相关的测试案例)进行了对比分析. 结论表明，全状态覆盖的测试套执行时间和内存消耗均大于全变迁和自定义-使用，自定义-使用的测试时间和内存消耗最小，能够有效的提高测试的效率.

表2 不同测试准则下的测试套比较Tab.2 Comparison of test suites under different criteria

4 结束语

本文基于HCSP 和TA 理论，提出了一种基于模型的列控系统测试案例生成方法.针对HCSP 的一个子集，提出了HCSP 的子集模型转换成TA 网络模型的转换规则，实现了列控系统HCSP 安全属性和时间相关属性的自动验证. 基于TA 网络模型，提出了全状态、全变迁和自定义-使用3 种覆盖准则下的测试案例自动生成算法，优化了列控系统测试案例套的自动生成. 在此基础上，给出了一个基于Uppaal＆CoVer 模型检验工具链，实现了列控系统测试案例自动生成. 最后，结合实际CTCS-3级列控系统RBC 切换场景进行了案例分析，生成了不同覆盖准则的测试套，并进行了比较分析，测试结果表明了方法的有效性.

［1］ 吕继东. 列车运行控制系统分层形式化建模与验证分析［D］. 北京:北京交通大学，2011.

［2］ 古天龙. 软件开发的形式化方法［M］. 北京:高等教育出版社，2005:6-8.

［3］ CHAOCHEN Z，HANSEN M. Duration calculus a formal approach to real-time systems［M］. ［S. l.］:Springer-Verlag，2003:14-16.

［4］ DONG Jinsong，HAO Ping，QIN Shengchao，et al.Timed automata patterns［J］. IEEE Transactions on Software Engineering，34，2008:844-845.

［5］ HOARE C A R. Communicating sequential processes［J］.Communications of the ACM，1978，21(8):666-677.

［6］ LIU Jiang，LÜ Jidong，ZHAO Quan. Programming languages and systems:a calculus for hybrid CSP［M］.Berlin:Springer，2010:1-15.

［7］ BEIZER B. Black-box testing，techniques for functional testing of software and systems［M］. New York:Wiley，1995:39-41.

［8］ 张勇，王超琦. CTCS-3 级列控系统车载设备测试序列优化生成方法［J］. 中国铁道科学，2011，32(3):100-106.ZHANG Yong，WANG Chaoqi. The method for the optimal generation of test sequence for CTCS-3 on-board equipment［J］. China Railway Science，2011，32(3):100-106.

［9］ 徐中伟，吴芳美. 形式化故障树分析建模和软件安全性测试［J］. 同济大学学报:自然科学版，2001，29(11):1299-1302.XU Zhongwei，WU Fangmei. Formal fault tree analysis modeling and software safety testing［J］. Journal of Tongji University:Natural Science，2001，29(11):1299-1302.

［10］ 赵显琼，唐涛. 多端口形式化测试自动生成方法在CTCS-3 车载系统中的应用［J］. 铁道学报，2011，33(7):44-51.ZHAO Xianqiong， TANG Tao. Multi-port based automatic formal testing generation and its application in CTCS-3 level on-board system［J］. Journal of the China Railway Society，2011，33(7):44-51.

［11］ 张曙光. CTCS-3 级列控系统总体技术方案［M］. 北京.中国铁道出版社，2008:49-50.

［12］ ALUR R，DILL D L. A theory of timed automata［J］.Theoretical Computer Science，1994，126:183-235.

［13］ 吕继东，唐涛. 高速铁路列控系统运营场景实时性建模与验证［J］. 铁道学报，2011，33(6):54-61.LÜ Jidong，TANG Tao. Modeling and verification of time constraints of operation scenarios of high-speed train control system［J］. Journal of the China Railway Society，2011，33(6):54-61.

［14］ ZHOU Chaochen，WANG Ji，ANDERS P. Ravn a formal description of hybrid systems［C］∥Proc. of the DIMACS/SYCON Workshop on Hybrid Systems III:Verification and Control. New York:Springer-Verlag，1996:511-530.

［15］ BEHRMANN G，LARSEN K G，MOLLER O，et al.UPPAAL-present and future［C］∥Proc. of the 40th IEEE Conference on Decision and Control. Orlando:［s. n.］，2001:2881-2886.

［16］ HESSEL A，PETTERSSON P. CoVer:a real-time test case generation tool［C］∥19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software. Berlin:Springer，2007:73-77.