基于TA的等级转换场景变异测试方法研究

宋 莉， 李 飞,2,3， 赵 瑜， 赵 健

(1.马鞍山学院 人工智能创新学院，安徽 马鞍山 243199; 2. 安徽工业大学 电气与信息工程学院, 安徽 马鞍山 243032; 3. 中国科学院合肥物质科学研究院，安徽 合肥 230031)

宋莉，李飞，赵瑜，等.基于TA的等级转换场景变异测试方法研究[J].石家庄铁道大学学报(自然科学版),2022,35(1):57-63.

等级转换场景是列控系统(Chinese Train Control Syetem，CTCS)典型的运营场景之一，是实现CTCS-2/CTCS-3级兼容的技术方法。研究等级转换场景时一般需要考虑2种情况，其一是正常情况下在固定地点进行的级间转换，其二是由于特殊原因引起的降级转换。

测试是分析验证系统正确性及可靠性的重要手段，测试用例是测试的基础。近年来，基于模型的测试案例日趋成熟，文献[1]结合时间自动机和一致性关系理论，提出了一种新型列车自动保护系统(Automatic Train Protection，ATP) 在线一致性测试方法，并取得了良好的效果；文献[2]基于输入输出时间自动机理论对列控系统中9种列车运营模式进行变异测试分析，得到了较为完善的测试案例；文献[3]针对报警系统构建TA模型和变异体模型，使用增量算法技术生成测试案例，并对案例集的完备性进行了评估。

本文对列控系统等级转换场景构建TA模型和变异体模型，同时借助测试辅助工具MoMuT::TA生成测试案例，并补充完善原测试案例集，得到了较为完善的测试案例集。

1 基于TA变异分析的测试案例生成方法

1.1 时间自动机理论(TA)

时间自动机理论增加了时间约束机制，每一个系统时钟均可在任意一个位置和状态迁移时对其重置，从而可以有效表达实时系统的时间约束特性[4]。

时间自动机TA可以描述为TA=，在该六元组中，S为一组有限位置，S0⊆S为TA的初始位置，A为一组有限事件，X为一组有限时钟，I:SФ(х)描述映射，x∈X，任一位置s∈S都被指定Ф(х)中的时钟约束δ，E⊆S×A×Ф(х)×2x×S，表示系统中所有状态迁移的集合[5]。

列控系统等级转换场景是一个复杂的场景，由多个构成对象构成，因此在建立TA模型时，单一模型是无法满足其功能需求的，需要同时建立多个模型同步描述系统行为。此时将等级转换场景划分为不同模块单独建立TA模型，同时对各模型增加并行组合与约束条件，实现模型之间的同步通信，进而构成整个系统的时间自动机模型。

UPPAAL是基于时间自动机的建模验证工具，通过在UPPAAL的编辑器中声明通道和共享变量实现等级转换场景中不同模块间的通信，进而构成一个完整的TA模型[6]。任意时刻，并行模块之间的发送器和接收器由通道声明(Chanb)联系在一起，“b!”表示发送事件b后位置迁移，“b?”表示接收事件b后位置迁移，“b!”和“b?”是同时发生的，有发送动作“b!”就一定有接收动作“b?”。此外，UPPAAL还用broadcast chan声明广播通道，可以实现一发多收的功能，以broadcast chand为例，发生“d!”后，系统中

所有子模型的“d?”都可能发生。设置通道声明实现了不同子模型之间的信息交互，将复杂系统有机建立起来。

UPPAAL的验证器使用了BNF(Backus-Naur Form)语言验证模型的性质，BNF是一种简洁、方便的描述语言，其定义如下：Prop::=E<>p|A[]p|E[]p|A<>p|p→q。各语句的含义如表1所示。

表1 BNF语句及其含义

1.2 TA变异

模型变异通过对系统中某些特定部分做微小改动来充分模拟系统所有的潜在危险，是一种基于缺陷的软件技术。在变异测试中，针对时间自动机模型，通过设计2类变异算子生成变异体：时间性变异算子(Timed Mutation Operator，TMO)和功能性变异算子(Functional Mutation Operator，FMO)。时间性变异算子通过改变系统时钟约束使其发生时间性错误，继而构造变异模型。功能性变异算子通过改变系统模型中的位置、迁移、函数等使其发生功能性故障，继而构造变异模型[7]。在列控系统等级转换场景中，设置15种变异算子，包括5种时间性变异算子和10种功能性变异算子。表2列举了这15种变异算子。

表2 变异算子

1.3 TA变异分析与评估

(1)若∃i∈[1,n]，使得Execute(TA,tci)≠Execute(M,tci)，即执行测试案例后，TA与变异体M之间不存在一致的路径交集，称作杀死变异体M，此时在测试集中就可以删除该测试案例以节省测试成本。

(2)若∀i∈[1,n]，都有Execute(M,tci)=Execute(TA,tci),称作未杀死变异体M，此时需要对变异体M做非法判断和等价判断；若判断结果为非法变异体和等价变异体，则称作无效变异体。

2 等级转换场景变异测试

在列控系统中，等级转换场景是实现CTCS-2级和CTCS-3级兼容的技术方法，研究等级转换场景时一般需要考虑2种情况，其一是正常情况下在固定地点进行的级间转换，其二是由于特殊原因引起的降级转换[8]。下面详细介绍在等级转换场景下时间自动机建模及变异分析和测试案例集完备研究。

2.1 基于TA的等级转换场景建模

基于时间自动机理论和等级转换场景的工作流程，建立列控系统等级转换TA模型。主要涉及4个模块，无限闭塞中心(RBC)、车载系统(Onboard)、司机(Driver)和应答器(Balise)。利用时间自动机积的定义构建网络自动机的模型，记为RODB模型，如图1所示。

设RODB模型的事件集合为∑，则有：∑=∑RBC&Onboard∪∑Onboard&Driver∪∑Balise&Onboard

图1 RODB时间自动机模型

2.2 RODB变异体模型建立

借助15种变异算子对已建立的RODB模型进行变异，形成相应的变异体模型。此处以“从Onboard向RBC建立联系”为例，通过改变约束时间，说明变异体模型的形式。

“从Onboard向RBC建立联系”的时间自动机模型为TA_A0,其表示“在输入行为Link后，系统从位置idle迁移到q1，在T_trainto rbc≤10的约束条件下输出行为Connect，进而迁移到位置q2，最后经输出CommInfo行为将位置迁移到WaitTrainInfo”。对TA_A0进行改变约束，即将约束条件T_trainto rbc≤10分别变异为取消约束条件、T_trainto rbc≥10、T_trainto rbc>10、T_trainto rbc≤20，产生的变异体分别为TA_M1、TA_M2、TA_M3、TA_M4，如图2所示。

图2 变异体模型

2.3 测试辅助工具 MoMuT: : TA

MoMuT::TA是一种支持时间自动机建模语言，研究实时系统而开发的黑盒测试案例生成工具，能够自主完成TA模型的变异及生成基于变异模型的测试用例。首先,MoMuT: : TA通过输入UPPAAL中的原始模型XML文件，并分析XML文件中的基本因子，形成启用模型，添加变异算子使得模型变异，得到变异体。其次，通过一致性检查/k界模型检验方法将生成的变异体模型与TA模型反复判定得到有效变异体，最终将获取的有效变异体应用于测试案例生成算法中，得到测试案例。图3为借助测试辅助工具MoMuT: : TA生成变异体和测试案例的工作流程。

图3 MoMuT: : TA生成变异体和测试案例的工作流程

3 等级转换变异测试与完备性评估

基于对等级转换场景的工作流程及信息交互的分析，构建了RODB模型。结合15种变异算子，对无限闭塞中心RBC、车载系统、司机操作和地面应答器4个子模块分析构建变异体模型，基于RODB模型和变异体模型，评估测试案例的完备性。

3.1 测试案例的筛选归并

列控系统是一个复杂且庞大的系统，通过查阅《CTCS-3级列控系统测试案例(V3.0)》可知，共包含469个测试案例，主要研究等级转换场景下变异测试分析，故首先需从这469个测试案例中筛选出与等级转换相关的测试案例。

根据设定的等级转换场景和已建立的RODB模型，共筛选出与之相关的44个测试案例。为了减少测试案例的数量，降低变异测试的成本，根据测试的性质和目的将部分相似度较高的测试案例进行分类归并，简化测试案例集。

3.2 变异体的生成

生成RODB模型的变异体之前，基于变异算子的规则对原模型进行变异分析，借助辅助工具MoMuT::TA对变异对象进行分析并生成变异体。在进行变异测试之前，通过一致性检查/k界模型检验筛除测试中的非法变异体和等价变异体，分析研究的主体为剩余的有效变异体[9]。表3为变异体模型信息统计结果。

表3 变异体模型信息统计结果

3.3 变异分析的执行和结果

将测试案例集的参数信息分别反复输入到RODB原模型和变异体中，比较两者的输出，统计各类变异体的个数，结合变异分数公式，评估测试案例集的完备性，为完善测试案例集提供依据。

表4给出了RODB模型变异测试的数据，表中M为生成的总变异体数，E为等价变异体数，N为非法变异体数，L为活变异体数，K为模型中杀死的变异体数，P表示计算的变异分数，α表示变异算子的序号，α=1,2,…,15。

表4 变异测试数据

4 测试案例集的完善

为了研究等级转换场景中变异测试和完备性评估存在的问题，对测试中的37个未杀死变异体进行分析，找出变异体未被杀死的原因，其中有33个未杀死变异体指向测试案例“超速制动防护处理”覆盖不全，4个未杀死变异体指向测试案例对模型遍历不全，根据分析结果，补充完善相关的测试案例，基于对变异模型的分析研究，再次借助辅助工具MoMuT: : TA验证可得到，NCR、WCR和SCR均获取了有效测试数据且变异分数达到了1.00。除此之外，表中的CGC、NUF变异算子的变异分数均提高到了0.95以上，其余变异算子的变异分数也得到了相应提高。表明现有的测试案例集完备性较好。

表5 补充和完善后的变异测试数据

5 结论

对等级转换场景下的变异测试方法进行研究。首先，基于时间自动机理论，利用UPPAAL工具对等级转换场景建立TA模型；其次，对所建立的TA模型进行变异测试并依据加权变异分数定量评估其完备性；最后，分析完善原测试案例集，使所有的变异分数均提高到了0.95以上，从而得到了较为完善的测试案例集。