基于在线一致性测试理论的CBTC车载ATO功能测试研究
2020-04-16郭昊男吕继东刘宏杰
郭昊男，吕继东，柴 铭，刘宏杰，唐 涛
(北京交通大学 轨道交通运行控制系统国家工程研究中心， 北京 100044)
输入/输出一致性测试(IOCO)，在严格的环境假设基础上，通过环境产生测试激励施加于被测系统并根据实际输出与预期输出的一致性关系，判断被测系统是否满足功能需求约束[1]，是验证车载ATO控制逻辑正确性与安全性的重要手段，近年来国内外学者已进行了大量的研究[2-6]。
基于模型的在线测试方法是针对黑盒系统的IOCO新方法[7],将测试激励实时施加于真实被测系统，并实时对比实际被测系统与其需求模型的输出，根据二者一致性关系判断被测系统是否满足需求规范。
同传统离线测试相比，在线测试能够根据被测系统实时输出确定系统的行为轨迹，避免了不确定性带来的测试案例数量爆炸，提高了测试的完备性[8]。时间自动机理论建模方法在完整的数理逻辑基础上对时间系统进行刻画，能够对系统安全需求进行严格与充分的验证[9-10]。本文使用的UPPAAL-TRON测试工具以时间自动机模型为测试依据，实现了基于模型的在线一致性测试方法。
本文采用基于时间自动机模型的在线一致性测试方法验证车载ATO自动控车命令生成设计原理和具体实现同功能需求是否一致。首先分析了追踪场景下的ATO逻辑功能和安全特性，提出车载ATO在线测试的一致性需求；然后定义场景中各部分的一致性输入/输出接口，建立了相关自动机网络模型并形成了在线测试框架；最后通过变异分析，针对车载ATO软件典型的实现错误(错误的安全距离、静态限速、功能逻辑以及命令丢失等)，进行安全性验证。结论表明，该在线一致性测试方法能够及时检测出车载ATO软件行为与规范模型的不一致，为未来CBTC的进一步研发与安全验证提供一定的理论参考。
1 ATO功能介绍及应用场景分析
具有ATO功能的列车运行控制系统见图1，系统根据列车运行情况反馈及通过线路情况，自动调整目标距离、目标速度，实现列车的自动运行。通常ATO在设计时不会直接考虑ATP限速，而是由ATP直接对列车速度进行监督[11]，这种方式虽然能够保证运行安全，但可能造成正常情况下列车紧急停车，本文所讨论的ATO子系统融合了ATP功能。
本文选取CBTC中典型的两车追踪控制运行过程作为测试场景，并使用该场景下的列车运行安全需求作为验证依据。CBTC系统连续模式下两车追踪运行场景中系统的通信与控制过程见图2。列车每个周期将自己的运行方向、列车位置、速度等信息通过轨旁无线接入点(AP)并经由数据通信系统发送至相应的区域控制器(ZC)①、区域控制器综合数据服务单元(DSU)②、联锁系统(CI)③、以及车载提供的信息后，实时计算出列车的移动授权(MA)，并经由数据通信系统通过轨旁无线接入点下发给相应列车④、⑤、⑥。列车收到MA后，车载ATP根据MA中的授权终点距离、线路限速等信息计算列车的距离-速度安全防护曲线，车载ATO在安全防护曲线的监督下，生成控车命令，控制列车自动运行⑦。
上述场景中，每周期前后两车分别向ZC报告列车位置、速度等消息(即图2中①、②、③过程)的时序存在不确定性，因此使用离线测试方法难以做到完备测试。本文主要研究使用基于UPPAAL-TRON在线一致性测试方法，验证上述典型的具有实时性和不确定性的运行场景下ATO控制逻辑是否满足列控系统安全需求。
2 基于模型的在线测试理论方法
2.1 时间输入/输出变迁系统及相关时间一致性关系
A为系统的可观测行为集，由输出行为Aout和输入行为Ain组成。τ为系统不可观测行为,τ∉A,记Aτ=A∪{τ}。时间输入/输出变迁系统TIOTS(Timed Input/Output Transition Systems)定义为[12]：
定义1TIOTS由一个五元组(S,s0,Ain,Aout,T)表示。其中：S是状态的集合；s0⊆S，表示初始状态集合；T表示一个变迁：T⊆S×(Aτ∪d≥0)×S，且具有性质：
其中,d∈R≥0,d为非负实数，R为实数。
σ∈(A∪d≥0)*为一个可观测时间轨迹，σ=d1a1d2a2…akdk+1，且σ∈Aτ∪R≥0，d,d1,d2,…,dn∈R≥0。其中R为实数。
定义TTr(s)为一个状态s的可观测时间轨迹为
( 1 )
对于状态s(及S′⊆S)和时间轨迹σ，sAfterσ表示s执行σ迁移后的可达状态集合，其定义为
( 2 )
( 3 )
定义可观测输出集Out(s)，表示由状态s(s∈S′⊆S)产生的可观测输出行为集合(或者时间延迟)
( 4 )
( 5 )
定义2e∈E表示某一确定的系统运行环境，i,s∈S表示系统状态，则环境相关时间输入/输出一致性关系RTIOCOe[10]为
iRTIOCOes=∀σ∈TTr(e)
Out((i,e)Afterσ)⊆Out((s,e)Afterσ)
( 6 )
式中:(i,e)为实际设备状态集；(s,e)为规范系统状态集；上述一致性关系含义为：设备i在运行环境e激励下，其任何可观测输出以及时间延迟必须满足设备行为模型s在同一环境模型e的激励下产生的输出以及时间延迟。
2.2 基于UPPAAL-TRON在线一致性测试方法原理
基于模型的一致性测试原理[13-14]见图3，分为系统层、模型层和测试层3个层次。
(1) 系统层：包含实际被测系统和真实运行环境，二者通过规定的输入/输出接口进行交互。
(2) 模型层：是对系统层中环境、设备以及输入/输出接口的数学抽象，它形式化地描述了环境以及设备的行为规范，并通过可观测的输入/输出接口将二者耦合在一起。
(3) 测试层：为减少测试对运行环境的依赖，在模型层中使用环境模型ε定义被测设备的运行环境在可观测输入/输出接口上的行为，测试层根据环境模型的描述产生相应的输入/输出激励代替真实环境同实际被测系统进行交互，并根据实际被测系统与设备模型M间的一致性关系得出测试结论。
基于UPPAAL-TRON的在线一致性测试工具可实现上述测试原理，见图4，图中符号“！”表示发送、“？”表示接收(下同)。TRON根据环境模型产生输出序列代替真实的环境输入，并判断实际被测系统(IUT)的输出是否符合其需求规范模型的描述。由于工具TRON产生的输入/输出(in与out)是依赖于TIOA模型描述的符号语言，需要使用适配器在其和IUT实际物理输入/输出接口(input与output)之间做对应关系转换。
3 车载ATO一致性在线测试设计
3.1 整体结构
基于UPPAAL-TRON的在线一致性ATO功能测试框架见图5。
(1) 测试环境
① 测试规范：测试规范是整个运营场景中的各部分交互的自动机网络模型，包括列车动力学自动机模型(Train0、Train1)，车载ATO自动机模型(ATO0，ATO1)，区域控制器ZC自动机模型，同步时钟自动机模型(Timer)。
② UPPAAL-TRON工具：工具UPPAAL用于对实时系统进行时间自动机模型网络的建模、校验和验证。TRON是基于时间自动机模型网络的在线一致性测试工具，它根据UPPAAL建立的模型(XML格式数据)对实际系统进行一致性测试。
(2) 被测系统
① ATO仿真软件：实际的车载ATO设备物理和逻辑结构复杂，测试周期长，难度大。本文借助计算机程序设计车载ATO仿真软件并测试，一方面降低了测试复杂度，另一方面能够改变软件内部结构研究在线测试方法对软件设计中错误及异常的检测能力。
② 适配器(Adapter)：为了将自动机网络中符号化的输入/输出通道和实际被测系统的输入/输出接口进行匹配，TRON提供了基于TCP/UDP通信的转换匹配协议用于在测试工具和被测系统之间构建适配器。
(3) 运行原理
ATO在运行过程中需要同ZC、时钟、列车等进行交互，在基于模型的在线一致性测试中，测试工具将使用相应的时间自动机模型产生输入激励与真实ATO进行交互，并根据真实ATO返回的信息与ATO模型返回的信息进行比对，通过二者的一致性关系得出测试结论。由于ATO的输出为控车命令，不易理解与分析，本文使用列车的位置速度作为可观测输入/ 输出接口上的数据监控列车运行。
3.2 自动机网络接口
根据图5中被测系统的模型网络结构，可定义相关的可观测输入/输出通道。其中，用带方向的箭头表示设备交互行为，箭头下方的通道名表示设备之间发送或者接收可观测消息的行为。
自动机网络中的可观测通道见图6，其含义分别为：时钟自动机每周期通过syn信号使Train0和Train1同步工作；Train0和Train1在每周期的同步信号到来后，向ZC发出lvtoZC消息报告自己当前的位置和速度, ZC在收到消息后将更新两车的移动授权；此外Train0和Train1每周期分别向ATO0和ATO1发送request消息，请求行车命令。ATO0与ATO1在收到列车的请求消息后，根据ZC给出的最新的MA计算行车命令，keep、acce、nbrake、ebrake分别表示巡航命令、加速命令、常用制动命令以及紧急制动命令。
3.3 UPPAAL时间自动机模型
(1) 列车动力学模型
列车运行的动力学过程时间自动机见图7，由图中虚线框所划分的⓪～⑤六个主要状态组及其之间的相互转移关系构成。⓪为自动机逻辑起点，①～⑤分别为1个周期中列车巡航、停车、常用制动、加速、紧急制动运行过程。图7中相关的符号含义见表1。
表1 列车自动机符号说明
符号类型含义IDint列车编号Startlocation列车自动机起始位置tclock列车时间自动机内部时钟STOPlocation周期开始处于停车状态,速度为零train_v[ID]arrayslot编号为ID的列车(以下简称列车ID)的速度KEEPlocation周期开始处于巡航状态train_s[ID]arrayslot列车ID的位置ACCElocation周期开始处于加速状态Tint时间周期NBlocation周期开始处于常用制动状态a1[ID]arrayslot加速度EBlocation周期开始处于紧急制动状态ebrakea[ID]arrayslot最小紧急制动减速度move(k)function巡航运行一周期的动力学过程nbrakea[ID]arrayslot当前常用制动减速度move(a)function加速运行一周期的动力学过程syn?channel时钟同步消息move(n)function常用制动运行一周期的动力学过程lvtoZC[ID]channel位置、速度消息move(e)function紧急制动运行一周期的动力学过程request[ID]channel请求消息t<2boolean在2个单位时间内keep[ID]channel巡航命令train_v[ID]>0boolean列车ID速度大于0acce[ID]channel加速命令train_v[ID]==0Boolean列车ID速度等于0nbrake[ID]channel常用制动命令t=0clockreset时钟置0操作ebrake[ID]channel紧急制动命令
以图7状态组①为例说明列车运行一个周期的过程。其动作序列描述为：(a)周期开始自动机处于KEEP位置，表示列车处于巡航状态。(b)当列车收到时钟同步消息syn后，将内部时钟t置为0，并迁移至下一匿名位置。(c)在两个单位时间内(t<2)，列车通过lvtoZC[ID]消息向ZC发送当前的位置和速度报告，并迁移至下一匿名位置。(d)在两个单位时间内(t<2)，列车向ATO发出request[ID]消息用于请求行车命令，并迁移至下一位置。(e)自动机执行move(k)函数，并迁移至状态组中的最末位置，准备向其它状态组转移。move(k)函数依照牛顿第二定律描述了列车在巡航状态下一个周期内的走行距离变化，动力学方程为
train_s[ID]=train_s[ID]+train_v[ID]×T
图7中反映的状态组①向其它状态组的转移关系见表2。
表2 状态组①转移关系
当时间自动机运行至状态组①的最后一个位置，将根据收到的ATO消息转移至相应的目标位置。例如当收到acce[ID]消息时，自动机将从当前位置转移至状态组④的ACCE位置。
其余状态组动作过程类似，仅是动力学方程或控制逻辑稍有不同，需要特别说明的是：
(a) 实际制动过程中，列车可能在任意时刻停车，由于模型是周期运行，为了防止出现负速度与位置偏差，对制动过程(④、⑤)增加了速度合法性判断与参数补偿逻辑。
(b) 自动机一旦进入状态组⑤将一直停留在状态组⑤直至停车，表示紧急制动过程不能缓解。
(2) 车载ATO模型
ATO时间自动机模型见图8，由图8中虚线框所划分的⓪～②三个功能模块及其之间的相互转移关系构成，主要作用分别是：参数初始化，速度防护以及命令触发。图中部分标识符含义已经在表1中说明，其余符号含义见表3。
图8中模块①集成了车载ATP的超速防护功能，控制逻辑见算法1。算法1与自动机模型对应关系为：第1～3行牵引假设对应图8中模块⓪匿名位置至模块①位置1之间的迁移，它考虑在上一时刻(-T)ATO输出加速命令(最不利情况)，若当前时刻(0)ATO也输出加速命令，则下一时刻(T)ATO输出相应制动命令时，列车能否在MA限制内安全停车。
不同制动曲线对列车运行过程所做的假设条件见图9。图9(a)中0～T阶段列车执行上一时刻ATO输出的加速命令；T～2T阶段列车执行当前时刻(0)ATO输出的加速命令；2T～3T阶段表示列车在T时刻的紧急制动命令下，列车牵引力被解除，制动力未施加时的惰行过程；3T～6T阶段表示弱常用制动条件下列车在预留反应时间(3T)内的运行过程；6T～9T阶段表示列车在制动力作用下至停车的过程。ev表示此过程中列车能够达到的最大速度，曲线围成的面积表示列车从当前时刻位置至停车点的走行距离。图9(b)～9(d)分别表示预留2T反应时间的中常用制动、预留T反应时间的强常用制动和紧急制动假设下的列车运行过程，margin表示在这些预留时间内列车的运行距离。
表3 ATO自动机符号说明
第4～5行巡航假设对应模型位置6到位置1之间的迁移，相较于加速假设，巡航假设列车运行过程中加速阶段只有一个周期，其余阶段均相同。7～13行的for循环对应模型位置1、2、3及其之间的迁移，变量index的值由1到4分别对应紧急制动触发曲线以及强、中、弱常用制动触发曲线。程序根据当前命令假设依次判断列车距离速度关系是否符合相应的制动曲线约束，判断结果与输出命令对应关系见表4。计算常用制动触发曲线时，区段限速在MA给定值的基础上保留2 m/s富余度。
第14～23行的while循环对应位置3、4、5、6及其之间的内部迁移，根据相应命令输出假设条件，结合当前列车位置及速度判断列车运行是否能够遵从相应的MA限制。
算法1ATO控制算法:
表4 约束关系与输出命令
从列车当前所在限速区段开始，计算列车制动力施加点位置到每一个限速区段终点位置的距离ed。其中：(a)conditon1()==ev
ATO首先考虑在牵引加速假设下，列车运动过程是否满足condition1()与condition2()条件，如果满足则表示ATO可给出加速命令，否则考虑巡航假设。如果巡航假设通过，则表示ATO可给出巡航命令，否则输出相应的制动命令。命令输出过程见图8模块②。
(3) ZC时间自动机
区域控制器ZC时间自动机见图10。在Start位置和Update位置之间有两条路径，分别表示ZC以不同的可能时序收到前车(编号0)和后车(编号1)发送的位置速度消息lvtoZC。变量ftrain表示前车的位置，前车依照线路静态限速运行(终点为3 km)，后车以前车位置为移动授权终点运行。
(4) 时钟自动机
时钟自动机(下称时钟)见图11，模型中的所有列车自动机(Train0，Train1)和ATO自动机(ATO0，ATO1)都使用时钟发出的syn信号进行同步。系统运行开始时时钟首先等待5个单位时间，对应实际系统的上电初始化过程。之后将以10个单位时间为周期，每周期的前2个单位时间内向列车发出时钟同步信号。
3.4 被测软件设计
被测软件由仿真列车及车载ATO模块和适配器组成，其中：
(1) 适配器 使用Java语言根据TRON的输入 / 输出接口配置流程在测试工具和被测系统之间构建适配器软件。其部分程序如Program1，其根据TRON规定的TCP协议格式进行输入/输出映射、仿真时间单位设置等工作。
Program1
public static oidconfig(int port) throws IOException{
initialTable();//初始化映射表
server=newServerSocket(port); //初始化socket
socket=server.accept();
//初始化输入/输出数据流
is=newDataInputStream(socket.getInputStream());
os=new DataOutputStream(socket.getOutputStream());
setIO();//根据映射表配置符号输入/输出与物理输入/输出
setTimeUnit(100 000); //设置测试时间单位
setTimeOut(3 000);//设置测试时长
os.writeByte(SA_TestExec);//开始执行测试
os.flush();
}
(2) 被测软件设 车辆仿真即遵照牛顿第二定律编写的车辆在不同命令下位置速度随时间的变化关系，ATO的控制算法已在算法1中详细描述，程序实现逻辑基本与模型描述一致。
4 模型验证及结果分析
4.1 模型参数配置
(1) 线路参数：线路全长3 km，包含两个静态限速区段，范围为0～2、2～3 km，分别对应限速20、10 m/s。
(2) 车辆参数：两车的动力特性相同，最大牵引加速度为1 m/s2,最小制动减速度为1 m/s2,弱、中、强常用制动减速度分别为1.1、1.2、1.3 m/s2，前后车初始位置分别0.5、0 km。
(3) 安全距离：后车MA终点位置距离前车当前位置至少300 m。
(4) 仿真时间：模型中初始化时间为5个单位时间，运行周期为10个单位时间；测试框架中每个单位时间对应物理时间100 ms。
4.2 模型验证
模型建立后需要在此基础上进行安全性质验证，UPPAAL提供了基于计算树逻辑(CTL)的性质描述语言及验证器[15]。描述语言由路径表达式和状态表达式组成，前者规定了表达式在状态路径上的作用范围，后者规定了有效范围内的状态应该满足的逻辑约束。根据路径表达式可以将验证性质分为可达性、安全性、存在性三类。可达性表达式E<>φ含义为给定状态公式φ，存在一条从开始状态出发的状态路径，沿着该路径φ最终被满足。安全性表示危险状态永远不会发生; 表达式A[]φ表示对于任意可达状态，φ始终被满足；表达式E[]φ含义为存在一条状态路径，φ始终被满足。存在性表示某些事件最终会发生; 表达式A<>φ含义为对于所有状态路径，φ最终都会被满足；表达式φ-->ψ表示只要φ被满足，ψ最终也会被满足。根据ATO控制逻辑原理及安全要求，对相关性质进行验证，表达式及结果见表5。
表5 模型验证结果
性质(1)验证自动机网络中是否存在死锁，系统可能因为死锁而停留在危险的状态；性质(2)验证ATO控制下两车是否能保持300 m的安全车距；性质(3)、(4)验证列车在静态限速区段是否遵守相应的限速要求；性质(5)表示列车紧急制动后一定会停车；性质(6)表示在最后一个限速区段内，前车一定能够停下；性质(7)表示存在列车速度不为0的停车状态。以上性质中(1)、(2)、(3)、(4)是列车运行的安全约束，性质(5)、(6)、(7)则是对系统实现原理进行验证，除性质(7)外其余性质均被验证通过。因为列车停车状态规定车速应当为零，(7)中描述的车速大于零的停车状态不存在。形式化验证进一步保证了系统实现机理的正确性及系统安全需求得到满足。
4.3 仿真结果分析
根据上述配置方案使用UPPAAL-TRON测试工具对仿真车载ATO逻辑功能进行测试，结果见图12，仿真时长为3 000个单位时间，mtu为model time unit 模型时间单位，在有效测试时间内环境时钟激励下，仿真软件的输出结果和自动机模型网络输出结果完全一致(TEST PASSED)。
图12 仿真车载ATO逻辑功能进行测试结果
两车追踪场景相关参数关系见图13。图13(a)为在相应限速区段运行时列车速度符合静态限速要求。图13(b)为两车位置随时间的变化，开始时刻两车距离500 m，到终点时两车距离接近安全车距300 m。值得注意的是，两车距离缩短过程总是发生在限速区段的分界点附近，这是因为在0～2 km限速区段，前车的MA终点远超后车MA终点，前车运行速度逐渐超过后车，两车距离逐渐增加。前车到达限速区段分界点附近时，受2～3 km区段限速限制，车速逐渐降低，由于后车动作的迟滞性，后车速度超过前车速度，两车距离逐渐减少。图13(c)为后车速度相对于前车速度变化的迟滞性，表现为从一个限速区段到另一个限速区段，后车速度变化晚于前车速度变化。在正常运营场景下，迟滞性降低了前车速度对后车速度的影响程度，能够让后车运行过程更为平稳，但在紧急场景下迟滞性增加了后车的反应时间，对行车安全产生不利影响。图13(d)为列车在收到时钟信号后向ZC发送位置速度消息的时间间隔。不同的时序关系表明对于具有不确定性的系统，UPPAAL-TRON也能够很好地工作。
在线测试过程中，前100个单位时间自动机网络可达状态集大小的变化以及相关信号发生时刻见图14。以10到20单位时间内的一个周期为例，ab段表示时钟激励信号发出后系统可达集增长的过程，ZC收到两车速度位置信号不同的时序关系导致了可达空间的急速增长；在b点当任意一辆列车首先发送速度位置报告后，之前的不确定时序关系就固定下来，因此bc段状态空间又急速减小。针对具有不确定性的系统的测试问题，在线测试方法能够根据被测系统实时反馈确定其行为路径，避免了状态空间增长导致的测试案例爆炸。
4.4变异测试
一致性测试的结果表明车载ATO软件的行为符合自动机模型的描述，其原理满足安全要求，实现符合规范描述。在此基础上，通过一些变异算子对仿真软件进行变异操作，验证UPPAAL-TRON测试方法的检错能力，变异算子及测试结果描述如下：
(1) 错误的安全距离：系统实现中将安全距离300 m错误地编写为200 m。测试结果见图15(a)，图中@为分隔符(下同)。测试工具检测到系统实现在第166～169个单位时间内的输出结果与规范模型运行结果不一致，给出了测试失败结论(TEST FAILED)。
(2) 错误的静态限速：系统实现中将0～2 km区段的静态限速20 m/s错误地编写成22 m/s。测试结果见图15(b)，检测工具在第195～198个单位时间内发现前车的距离速度与模型预期结果不一致，给出了测试失败结论(TEST FAILED)。
(3) 逻辑错误：算法1超速防护逻辑实现中，将制动终点到当前限速区段终点距离ed计算公式中a1*t2/2项错写为a1*t2测试结果见图15(c)，检测工具在第285～288个单位时间内发现后车的位置与速度同模型预期不符，若列车按照当前情况继续运行可能产生危险。
(4) 命令丢失：在实际系统中，因为通信原因可能出现命令延迟与丢失等情况，在ATO仿真软件中，可以模拟行车命令丢失的场景。测试结果见图15(d)，检测工具并没有发现系统中存在的异常。检查后发现虽然运行过程中ATO丢失了一个巡航命令，但是在实际设计中如果列车在一个周期内没有收到行车命令，将会参照上一个周期的命令继续运行，而上一个周期ATO发出的恰好也是巡航命令，因此在外部可观测通道上，仿真系统的输出行为和规范模型的输出结果完全一致。
图15 变异测试结果
以上4个变异测试在一定程度上反映了UPPAAL-TRON方法对于不确定实时系统的在线监测能力，同时图15(d)也揭示了该方法的一点不足。对黑盒测试而言，测试者(或测试工具)只能观察到被测系统与外界环境的交互行为，因此测试只能在可观测的输入/输出接口上进行，当内部错误未影响到交互接口时,如图15(d)，该错误就无法被检测。事实上，当被测系统内部存在逻辑错误时，基本都能以错误的输出形式表现出来，但是具有一定的随机性与不确定性，需要通过完备的测试环境激励及较大规模的重复测试来捕获。在不了解被测系统具体实现的情况下，针对黑盒系统的在线一致性测试方法能够较好地检验被测系统实现是否符合相应的需求规范及安全约束。在掌握系统具体实现细节的情况下，对于外部难以检验的行为，可以使用白盒测试如单元测试等来提高系统的可靠性，对于内部组件间的交互行为可以通过集成测试等手段来提高安全性。在条件允许的情况下(可以进入系统内部进行测试)，应当使用多种测试方法充分发挥不同测试手段的优点，针对具体问题展开测试，提高系统的安全性，可靠性及稳定性。
5 结束语
本文采用基于模型的在线一致性测试理论及方法，针对CBTC车载ATO的安全功能进行测试与分析，结果表明在线一致性测试方法能够实时地监控被测系统可观测输入/输出接口上的变化，动态追踪系统运行轨迹，有效地避免了传统离线测试的状态空间爆炸问题，提高了对CBTC车载ATO软件的检错能力与测试效率，为未来CBTC的进一步研发与安全验证提供一定的理论参考。此外，将进一步研究在线测试方法在混合测试中的应用，研究采用多种测试手段提高测试完备性，保证被测系统安全可靠。
