Testing Modeling Method for Engineering Testing of High-Speed Railway Signaling System
-
摘要:
高铁信号系统工程测试关注系统中各设备间的复杂行为关系和状态同步，工程测试的测试建模方法缺少复杂行为交互和同步机制，针对此问题，提出基于扩展有限状态机的高铁信号系统工程测试建模方法和测试用例生成方法. 首先，分析高铁信号系统工程测试的特点，提出复杂事件交互和状态同步的测试建模需求，以有限状态机理论为基础，扩展出状态事件和层次性，满足信号系统工程测试中复杂行为关系和状态同步的建模需求，采用
Z 规格说明语言给出扩展有限状态机的形式化定义，定义扩展有限状态机的格局和同步机制；然后，提出将扩展有限状态机转化为时间自动机的算法，利用时间自动机的测试用例生成算法自动生成高铁信号系统工程测试的测试用例；最后，以高铁信号系统工程测试中的进路控制为例，建立扩展有限状态机模型并生成测试用例，通过变异分析对生成的测试用例进行评估. 结果表明：测试用例在检测状态变异和事件表达式变异时的变异评分均为1，具有良好的覆盖度，能够满足高铁信号系统工程测试的需求.Abstract:The engineering testing of a high-speed railway signaling system (HSRSS) focuses on the complex behavior relationship and state synchronization among various equipment in the system. Since the testing modeling method for engineering testing lacks complex behavior interaction and synchronization mechanism, the engineering testing modeling method and test case generation method of HSRSS based on an extended finite state machine (EFSM) were proposed. First, the engineering testing characteristics of HSRSS were analyzed, and the testing modeling requirements for complex event interaction and state synchronization were proposed. Based on the theory of finite state machine, the state events and hierarchy were extended to meet the modeling requirements for complex behavior relationships and state synchronization in engineering testing of HSRSS. The formal definition of EFSM was given by using
Z specification language. The pattern and synchronization mechanism of EFSM were defined. Then, the algorithm of transforming the EFSM into a timed automata (TA) was put forward, and the test case generation algorithm of TA was used to automatically generate test cases for engineering testing of HSRSS. Finally, with the route control in engineering testing of HSRSS as an example, an EFSM model was established, and test cases were generated. In addition, the generated test cases were evaluated through mutation analysis. The result shows that the test cases have a mutation score of 1 when testing state mutation and signal expression mutation, and they have good coverage, which can meet the requirements of engineering testing of HSRSS. -
截至2023年11月30日，我国高速铁路营业里程已达到4.37万公里，成为世界上高铁运营里程最长、运营动车组最多、运行场景最复杂的国家. 信号系统是保障高铁安全、高效运行的核心设备，目前，我国正深入研究涵盖计算机联锁、列控中心、无线闭塞中心和调度集中等关键设备的综合测试平台. 加强设备间的测试验证，优化现场工程测试方案，大力降低信号系统工程中的安全风险，信号系统工程测试已成为我国高铁领域中的重要研究课题.
在高铁工程项目中，由于站场、线路参数和速度等级等条件的不同，信号系统设备需要根据具体的工程数据进行相应的接口配置，保证工程项目中设备间行为关系的一致性. 高铁信号系统作为一种对安全性与可靠性要求极高的工程应用[1]，系统工程中若存在行为关系错误，将可能引发重大事故，导致严重的生命与财产损失. 由于高铁信号系统工程的安全性不局限于单个设备的功能安全，在线路正式投入运营前，需要对系统中各设备之间的交互和设备间的各项行为关系进行充分的测试，涉及复杂的信号交互和设备间的状态同步，增加了高铁信号系统工程测试的难度.
目前，高铁信号系统测试的研究热点主要为基于模型的测试（MBT）理论，常用的测试建模方法包括Petri网、时间自动机（TA）和UML状态图（unified modeling language statechart）等，研究方向主要包括自动搜索测试模型生成测试用例、将测试模型与测试关键技术或系统安全性分析理论结合生成更全面的测试用例和针对高铁信号系统领域的测试建模方法3个方面：1） 在自动搜索测试模型生成测试用例方面，文献[2]和文献[3]构建无线闭塞中心切换场景的有色Petri网（CPN）模型，分别研究蚁群算法和深度优先搜索等算法优化测试序列. 文献[4]和文献[5]以车载设备为研究对象，构建CPN模型，分别研究测试序列搜索算法和中国邮路算法生成测试序列集. 文献[6]针对列控中心的特点，构建带有输入输出时间的确定性有限状态机模型，利用广度优先搜索算法和边界值分析方法生成测试用例. 文献[7]研究时间自动机建模理论，提出了基于UPPAAL-TRON的列控系统在线测试框架和测试用例生成算法. 2） 在测试模型与测试关键技术或系统安全性分析理论结合方面，文献[8]和文献[9]在TA方法的基础上，分别结合变异测试理论和故障树理论，提出更全面的列控系统测试用例生成方法. 文献[10]针对列控系统非确定性时延的问题，结合TA建模和一致性测试理论，提出一致性在线测试方法. 文献[11]采用UML状态图建模方法，针对轨道电路编码功能，综合图覆盖、组合覆盖和文法分析等测试技术生成测试用例. 文献[12]利用有限状态机模型描述车载目标速度监控曲线的内部状态迁移过程，利用I/O等价原理和等价类划分理论，进一步引入被测系统的故障模型和故障域范围生成更为全面的测试用例集. 文献[13]将基于搜索的技术和基于模型的突变测试相结合，设计适配函数指导测试用例的搜索过程. 文献[14]针对列控系统的复杂故障模式，结合失效模式与影响分析（FMEA）和UML序列图等技术，建立系统的故障扩展混合自动机模型，生成包含故障的安全测试用例. 3） 在测试建模方法方面，针对高铁信号系统测试建模过程中描述信号系统领域特征不够全面的问题，以有限状态机理论为研究基础，文献[15]提出时间状态机测试建模理论和测试用例生成方法，文献[16]提出风险时间状态机建模方法.
复杂行为关系和状态同步机制是高铁信号系统工程测试的重点内容之一. 目前对高铁信号系统工程中复杂的信号交互和状态同步机制研究较少，既有研究采用的测试建模方法在描述信号系统工程测试的复杂行为关系和状态同步时，如CPN、TA，模型复杂度较高、可读性差；UML状态图具有同步机制，但结构复杂，直接搜索高效的测试用例的难度较大. 信号系统工程测试缺少系统性的建模方法，对复杂行为和状态同步关系的测试用例设计主要依赖于专家经验，覆盖不够全面，测试效率不高. 本文针对高铁信号系统工程测试建模中的复杂行为关系和状态同步问题，以有限状态机理论为研究基础，提出扩展有限状态机测试建模方法描述信号系统工程测试中的复杂行为关系和状态同步，并提出测试用例自动生成方法，提高信号系统工程测试用例生成的全面性，为提升我国高铁信号系统的安全性和可靠性提供新的途径和研究思路.
1. 高铁信号系统工程测试建模需求
高铁信号系统功能涵盖站内进路控制、区间方向控制、点灯控制、应答器报文控制、轨道电路编码、临时限速设置和移动授权等功能，功能分散在计算机联锁、列控中心、临时限速服务器和无线闭塞中心等各个安全设备中，整个工程过程的结果形成了各个设备之间的工程关联关系，包括映射关系和行为关系：映射关系包括室外安装映射、施工配线映射和工程数据映射；行为关系包括继电电路行为和信号设备行为，如图1所示.
高铁信号工程测试主要包括2个方面的内容：1） 工程设计与实际系统的一致性测试；2） 信号系统设备之间的行为关系测试. 本文针对高铁信号系统工程中设备之间的行为关系测试展开研究. 高铁信号系统行为交互复杂，需由多个设备相互配合实现整个系统的功能，设备间不可避免地产生大量事件交互. 由于工程测试是从整个高铁信号系统的安全运行出发，以系统整体为研究对象，侧重设备之间的交互过程，测试建模方法需要重点描述设备之间大量的事件交互以及各个设备之间的状态同步等特点. 本文针对信号系统工程测试中行为关系的特点，在有限状态机理论的基础上，扩展出状态事件、层次性和同步机制，提出适合高铁信号系统工程测试的建模方法.
2. 有限状态机概述
有限状态机（FSM）是MBT理论中经典的测试建模方法[17]，采用可视化的方式直观地描述系统状态以及状态之间的转移关系，通常用作测试用例编制和测试结果评判的模型依据.
定义1 有限状态机是一个六元组，M=(S,sinit,Σ,X,δ,λ)[18]，S为有限状态集合；sinit∈S，为初始状态；Σ为有限输入符号集；X为有限输出符号集；δ，S×Σ→X，为输出函数；λ，S×Σ→S，为状态转移函数.
图2为一个FSM模型示例Mex. Mex包括初始状态sin和输出状态sout，I1、I2为输入符号集，O1、O2为输出符号集. sin接收到输入I2时转移到sout状态，同时输出O2. Mex六元组如下：S={sin, sout}，sinit = sin，Σ={I1, I2}，X={O1, O2}，λ（sout, I1）= sin，λ（sin, I2）= sout，δ（sin, I2）= O2，δ（sout, I1）= O1.
根据有限状态机的定义，其不具有同步和复杂事件交互的机制，不能满足高铁信号系统工程测试的需求.
3. 扩展有限状态机
本节以有限状态机作为测试建模的理论基础，对FSM进行扩展，提出面向高铁信号系统工程测试的扩展有限状态机建模方法（EFSM）.
结合Z规格说明语言，提出EFSM的定义. 为描述方便，普遍采用逐层递进的方式对复杂建模方法进行描述[19-20]. 首先，定义EFSM的基本元素，在FSM的状态中扩展出事件和同步属性，然后定义EFSM的层次结构，最后给出EFSM的形式化定义，达到描述高铁信号系统工程测试模型的复杂行为和状态同步关系的目的.
3.1 EFSM的基本元素
EFSM包括状态、事件表达式和迁移等基本元素.
1） 状态
EFSM的一个非空、有限的状态集合记为S.
[S]
∃ x : ℕ1 ⦁ #S = x
状态具有初始状态（INIT）和同步状态（FINAL）2种属性.
F ::= INIT | FINAL
状态包括BASIC、AND和OR 3种类型.
D ::= BASIC | AND | OR
2） 事件
事件E具有产生和不产生2种状态，SYNC表示同步事件，E0表示事件一直产生的常量.
[E]
∃ x : ℕ ⦁ #E = x
3） 事件表达式
事件之间的and、or和not逻辑关系构成事件表达式，记为Ex，如a or b表示事件a或事件b至少有一个产生.
4） 迁移
迁移是EFSM从源状态转移到终止状态的方式，包括源状态su，事件e，转移时产生的事件c和终止状态se. 迁移的Z语言描述为
3.2 层次性扩展
本小节在EFSM基本元素的基础上，进一步定义EFSM的层次结构.
EFSM的状态层次Ψ包括顶状态stop、状态事件分配函数v、直接子状态函数u、直接父状态函数p、状态类型分配函数r、状态属性分配函数m. Ψ满足以下性质：
1） stop 是唯一不具有父状态的状态，且 v 不能为其分配状态事件；
2） m 仅对 AND 状态中的直接 OR 子状态中的BASIC 状态分配 FINAL 属性；
3） u为AND 状态和OR 状态分配直接子状态，且不能循环分配；
4） OR 状态包含且仅包含一个初始状态，且所有直接子状态均属于同一层次；
5） 多个并发的OR 状态组成AND状态；
6） 任意非 stop 的状态有且仅有一个直接父状态，且均可以通过 u 由 stop传递到达.
Ψ的Z模式定义如下：
EFSM由状态层次和迁移集构成，Z 模式定义为
EFSM满足以下性质：
1） stop状态不为任何迁移的源状态或终止状态；
2） 迁移的源状态和终止状态不能为OR 状态，可以是AND或BASIC状态，且一条迁移有且仅有一个源状态和终止状态；
2） 迁移不能跨层次迁移；
3） 具有SYNC事件的变迁，其源状态与产生SYNC事件的AND状态具有相同的直接父状态；
4） 具有SYNC事件的变迁，其源状态为AND状态或其父状态为AND状态；
5） OR 状态的初始状态无源状态，且对任意直接子状态，可由初始状态通过迁移传递到达；
6） 迁移的触发事件不能是SYNC.
3.3 格 局
EFSM能够同时激活的最大状态集合称为格局，记为n，初始格局记为n0. 格局遵循以下规则：
1） stop状态属于n；
2） 如果OR状态s属于n，则s有且仅有一个直接子状态属于n；
3） 如果AND状态s属于n，则s的每一个直接子状态都属于n；
4） 如果非stop的状态s属于n，则s的直接父状态属于n；
5） n仅包含满足规则（1）～（4）的所有状态.
对任意格局，至少应该包含stop状态和一个BASIC状态，描述如下：
3.4 同步机制
EFSM利用状态的FINAL属性实现模型中相关状态之间的同步和转移. EFSM仅为AND状态的直接OR子状态中的BASIC状态定义FINAL属性，当该AND状态的所有直接OR状态均激活FINAL状态时，AND状态自动产生SYNC事件. SYNC事件的作用域仅为该AND状态同层次的变迁集，且1个AND状态最多包含1个SYNC事件. 图3为EFSM示例模型.
图3包括st、s0～s14 （15个状态）、e1～e3、SYNC 4个事件，其中顶状态为st，初始状态为{s0, s1, s2, s4, s7}. 状态s3、s5、s6、s8具有FINAL属性，n0=(s0, s1, s2, s4, s7)，u(s1)={s12, s13}，p(s1)=s10，r(s1)=AND，r(s2)=BASIC，r(s12)=OR，v(s6)=e3.
图3的层次性结构如图4所示，其中AND状态的子状态用弧线连接.
当e1、e2事件触发后，s3、s5同时激活，触发SYNC事件，SYNC事件影响s1同层次范围内的迁移，触发s1SYNC→s6，转移到s6状态，触发状态事件e3. s6激活时，e3持续产生. 当s6、s8激活时触发SYNC事件，影响st同层次范围内的变迁，触发s0SYNC→s9，转移到s9，格局主要转移过程如图5所示.
4. 基于EFSM的测试用例生成方法
由于EFSM结构相对复杂，模型解析繁琐，不易直接从EFSM生成测试用例. 目前，对基于时间自动机（TA）的测试用例生成算法研究丰富，开发了较为成熟的建模和测试用例生成工具UPPAAL. 因此，本节研究EFSM和 UPPAAL TA的特点，提出EFSM转换UPPAAL TA的算法，采用模型转换的方式，利用UPPAAL TA较为成熟的算法和工具实现EFSM测试模型到测试用例的自动生成.
UPPAAL在TA的基础上，扩展出int、bool和broadcast chan 等类型[21]，集成Yggdrasil提供Query file、Depth Search和Single Step 3种机制自动生成测试用例[22]. EFSM转换为UPPAAL TA的算法为
算法1 EFSM转换UPPAAL TA算法
输入：EFSM模型M
输出：UPPAAL TA模型M1
步骤1 从M中选取s，且ε s = OR，s集合记为Sk.
步骤2 选取si∈Sk，建立si对应的TA模型mi；将si的直接子状态转换为mi的位置；将si的迁移转换为mi的变迁.
步骤3 将si中的事件映射为mi的broadcast chan. 如果si包括not事件表达式，在mi中新增broadcast chan映射该not事件表达式.
步骤4 如果si包括状态事件，mi中新增bool变量，对应位置增加条件为true的自迁移，入射变迁将bool变量置为true，出射变迁置为false.
步骤5 如果si包括FINAL状态，mi新增bool变量描述该状态是否激活；mi对应的位置中增加条件为true的自迁移，入射变迁将bool变量置为true，出射变迁置为false.
步骤6 将si的SYNC事件映射为mi中对应的bool变量合取表达式.
步骤7 将si的事件表达式分解为单个事件或bool变量，mi根据si事件表达式对应的各个事件或变量依次进行状态转移.
步骤8 遍历si的格局转移关系，调整mi结构，保证mi与si转移关系的一致性.
步骤9 Sk = Sk \ si.
步骤10 如果Sk =∅，则继续步骤11，否则重复步骤2～9.
步骤11 遍历M 的格局转移关系，调整M1结构，保证转移关系一致；输出M1= m1 || m2 || ⋯ || mi.
转换算法以EFSM的OR状态为核心，将EFSM的事件映射为UPPAAL TA中的broadcast chan，将状态事件映射为bool变量，将SYNC事件映射为bool合取表达式的方式，具体包括以下规则：
1） 将EFSM中的OR状态转换为对应的TA模型；
2） 将OR状态的直接子状态转化为TA的位置，将OR状态之间的迁移转化为TA中对应位置之间的变迁；
3） 将EFSM的事件转化为TA的broadcast chan；
4） 在TA中新增broadcast chan表示EFSM的not事件表达式，将EFSM的事件表达式分解为TA的多个broadcast chan或bool变量的状态转移；
5） 对EFSM的FINAL状态，在TA新增bool变量描述该状态激活，在对应的位置中增加条件为true的自迁移，入射变迁将bool变量置为true，出射变迁置为false；
6） 用bool变量的合取表达式替换SYNC事件；
7） 将EFSM的状态事件映射为1个bool变量，并在TA对应位置的入射变迁将bool变量置为true，出射变迁置为false.
图3的EFSM模型对应的TA模型如图6所示，包括TA1～TA5 5个子模型. EFSM模型包括：s14、s10、s11、s12和s13 5个OR状态，分别映射为5个TA子模型；s3、s5、s6、s8 4个FINAL状态分别映射为TA中的4个位置和4个bool变量（b3、b5、b6、b8），通过变量取值true表示状态激活；s6的状态事件e3映射为bool变量b6_3.
5. 案例分析
为节省篇幅，本节以高铁信号系统工程测试中的进路控制测试为例，建立EFSM测试模型，并转化为UPPAAL TA模型生成测试用例.
5.1 基于EFSM的进路控制测试模型
进路控制是高铁信号系统工程测试的核心工作之一，涉及的设备对象包括轨道区段、道岔、信号机、列控中心（TCC）和无线闭塞中心（RBC）等. 为描述方便，本节仅针对进路控制主要的行为关系建立EFSM模型，如图7所示，记为Droute，事件名称及其含义见表1.
表 1 Droute事件含义Table 1. Meaning of events in Droute事件 含义 事件 含义 e10 进路占用 e11 进路空闲 e12 进路红光带 e13 进路检查通过 e20 道岔正确 e21 超限绝缘相邻区段空闲 e30 敌对进路满足 e31 灯丝正常 e41 向 TCC 发送进路 e42 向 RBC 发送 SA e43 取消进路 e44 延迟解锁 e45 分段解锁 Droute中，状态s10、s20、s23、s30、s33、s40分别表示“进路状态”“道岔状态”“超限绝缘相邻区段状态”“敌对进路”“灯丝状态”“进路控制”的初始状态，其余状态含义见表2.
表 2 Droute状态含义Table 2. Meaning of states in Droute状态 含义 状态 含义 s11 进路处于占用状态 s12 进路处于空闲状态 s13 进路处于红光带状态 s21 道岔位置处于非法状态 s22 道岔位置处于合法状态 s24 超限绝缘相邻区段处于占用状态 s25 超限绝缘相邻区段处于空闲状态 s31 敌对进路处于建立状态 s32 敌对进路处于未建立状态 s34 灯丝处于故障状态 s35 灯丝处于正常状态 s41 进路处于建立状态 s42 进路处于取消状态 工程测试过程中，进路控制检查进路中道岔状态是否符合预期、超限绝缘是否正确、进路中区段是否空闲，如果条件都符合要求，进路锁闭. 信号开放状态重复检查区段空闲、道岔位置正确、敌对进路未建立. 进路解锁主要分为正常解锁、延迟解锁和取消进路.
5.2 测试用例生成
根据EFSM转换为UPPAAL TA的算法，Droute的TA模型如图8 所示，包括TARoute1～TARoute7 7个子模型，记为Droute_TA. 其中，b12为算法1新增的bool变量，表示进路处于空闲状态，其余变量类似.
Droute通过19个BASIC状态、29条迁移和13个信号描述了进路控制过程的工程测试需求. TA模型描述该需求所需的状态、变迁、broadcast chan和变量数较多，如表3所示，表明EFSM结构更清晰，可读性更好，建模能力更强.
表 3 Droute与Droute_TA 对比Table 3. Comparison between Droute and Droute个 模型 构件数 状态数 变迁数 事件/变量数 Droute 1 19 29 13 DTA 7 25 47 22 针对Droute_TA模型，采用UPPAAL Yggdrasil的Query file、Depth Search和Single Step 3种机制自动生成19条测试用例，典型测试用例如表4所示.
表 4 Droute测试用例（部分）Table 4. Test cases of Droute （part）测试用例 主要内容 1 a） 进路区段空闲，道岔位置正确，超限绝缘相邻区段占用；b） 超限绝缘相邻区段空闲，进路上区段红光带，进路不能锁闭 2 进路空闲、超限绝缘相邻区段空闲、道岔位置正确、敌对进路未建立，进路锁闭，信号机开放 3 a） 进路空闲，超限绝缘相邻区段空闲，道岔位置正确，进路锁闭，信号尚未开放；b） 敌对进路未建立，灯丝正常，但进路占用，信号不能开放 4 a） 进路锁闭后，向 TCC 发送联锁进路；b） 进路锁闭后，向 RBC 发送 SA 信息 5 进路锁闭后，灯丝断丝，信号不能开放 6 列车在进路内正常运行，进路分段解锁 7 接近区段占用，接车进路解锁时需延时 3 min 5.3 测试用例评估
目前，高铁信号工程领域进路控制的测试用例主要来源于专家经验和工程积累. 根据EFSM 生成的测试案例完全包含了既有测试案例，且更为全面，覆盖超限绝缘相邻区段、TCC、RBC、灯丝断丝等关键场景. 以测试用例1为例，测试内容主要包括2个场景：首先，进路区段空闲，道岔位置正确，但超限绝缘相邻区段占用；随后，超限绝缘相邻区段由占用状态变为空闲状态，但同时进路区段发生红光带，进路不能锁闭. 相对于既有的测试用例生成方法，本文提出的方法能够提高高铁信号工程测试用例的全面性.
为对测试用例的有效性进行定量评价，本节采用变异分析方法对测试用例发现错误的能力进行评估. 首先采用变异算子对测试模型进行变异，产生一系列的变异模型，然后在模型中执行测试用例，若测试用例能够发现测试模型和变异模型之间的差异，则证明测试用例是有效的. 变异评分计算公式为[23]
MS=M3M1−M2, (1) 式中：M1为变异体总数，M2为变异体中等效变异体的数量，M3为测试用例发现的变异体数量.
本节通过增加、减少Droute的状态、迁移，以及改变Droute信号表达式的内容产生45个变异模型[24]、无等效变异模型. 图9为改变Droute状态s52信号表达式产生的变异模型. 在模型中运行测试用例4能够检验出变异模型，表明测试用例是有效的.
Droute变异算子、变异模型数量及变异测试结果的变异评分见表5. 从表5可知，在检测状态变异和事件表达式变异时，测试用例的变异评分均为1，结果表明，测试用例发现了绝大多数的变异，检测错误的能力较好.
表 5 测试用例评估Table 5. Test case evaluation变异算子 变异描述 变异体数量/个 发现变异体数量/个 变异评分 迁移变异 增加或减少迁移 20 12 0.6 状态变异 增加或减少状态 10 10 1.0 事件表达式变异 改变事件表达式内容 15 15 1.0 6. 结 论
1） 针对高铁信号系统工程测试的特点，提出高铁信号系统工程测试复杂事件交互和状态同步的测试建模需求.
2） 在FSM建模理论的基础上，扩展出层次性、状态事件和FINAL属性，提出扩展有限状态机描述信号系统工程测试需求.
3） 提出将扩展有限状态机转换为UPPAAL TA的算法，利用UPPAAL算法自动生成测试用例.
4） 以高铁信号系统工程测试中的进路控制为例，建立测试模型并生成测试用例. 相比时间自动机建模方法，扩展有限状态机描述能力更强；采用变异分析对测试用例进行评估，结果表明测试用例发现了绝大多数变异.
-
表 1 Droute事件含义
Table 1. Meaning of events in Droute
事件 含义 事件 含义 e10 进路占用 e11 进路空闲 e12 进路红光带 e13 进路检查通过 e20 道岔正确 e21 超限绝缘相邻区段空闲 e30 敌对进路满足 e31 灯丝正常 e41 向 TCC 发送进路 e42 向 RBC 发送 SA e43 取消进路 e44 延迟解锁 e45 分段解锁 
下载: 导出CSV
表 2 Droute状态含义
Table 2. Meaning of states in Droute
状态 含义 状态 含义 s11 进路处于占用状态 s12 进路处于空闲状态 s13 进路处于红光带状态 s21 道岔位置处于非法状态 s22 道岔位置处于合法状态 s24 超限绝缘相邻区段处于占用状态 s25 超限绝缘相邻区段处于空闲状态 s31 敌对进路处于建立状态 s32 敌对进路处于未建立状态 s34 灯丝处于故障状态 s35 灯丝处于正常状态 s41 进路处于建立状态 s42 进路处于取消状态
下载: 导出CSV
表 3 Droute与Droute_TA 对比
Table 3. Comparison between Droute and Droute
个 模型 构件数 状态数 变迁数 事件/变量数 Droute 1 19 29 13 DTA 7 25 47 22
下载: 导出CSV
表 4 Droute测试用例（部分）
Table 4. Test cases of Droute （part）
测试用例 主要内容 1 a） 进路区段空闲，道岔位置正确，超限绝缘相邻区段占用；b） 超限绝缘相邻区段空闲，进路上区段红光带，进路不能锁闭 2 进路空闲、超限绝缘相邻区段空闲、道岔位置正确、敌对进路未建立，进路锁闭，信号机开放 3 a） 进路空闲，超限绝缘相邻区段空闲，道岔位置正确，进路锁闭，信号尚未开放；b） 敌对进路未建立，灯丝正常，但进路占用，信号不能开放 4 a） 进路锁闭后，向 TCC 发送联锁进路；b） 进路锁闭后，向 RBC 发送 SA 信息 5 进路锁闭后，灯丝断丝，信号不能开放 6 列车在进路内正常运行，进路分段解锁 7 接近区段占用，接车进路解锁时需延时 3 min
下载: 导出CSV
表 5 测试用例评估
Table 5. Test case evaluation
变异算子 变异描述 变异体数量/个 发现变异体数量/个 变异评分 迁移变异 增加或减少迁移 20 12 0.6 状态变异 增加或减少状态 10 10 1.0 事件表达式变异 改变事件表达式内容 15 15 1.0
下载: 导出CSV
-
[1] 上官伟,胡福威,袁敏,等. 基于弹复力效应的列控车载设备可靠性分析方法[J]. 铁道学报,2018,40(6): 75-82. doi: 10.3969/j.issn.1001-8360.2018.06.010SHANGGUAN Wei, HU Fuwei, YUAN Min, et al. Reliability analysis method for on-board equipment of train control system based on resilience effect[J]. Journal of the China Railway Society, 2018, 40(6): 75-82. doi: 10.3969/j.issn.1001-8360.2018.06.010 [2] 齐凡瑞,李强. 列控系统RBC测试序列优化生成方法[J]. 北京交通大学学报,2022,46(2): 11-19,28. doi: 10.11860/j.issn.1673-0291.20210139QI Fanrui, LI Qiang. Optimal generation method of RBC test sequence for train control system[J]. Journal of Beijing Jiaotong University, 2022, 46(2): 11-19,28. doi: 10.11860/j.issn.1673-0291.20210139 [3] 梁茨,郑伟,李开成,等. 基于路径优化算法的测试序列自动生成及验证[J]. 铁道学报,2013,35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009LIANG Ci, ZHENG Wei, LI Kaicheng, et al. Automated generation of test cases and sequences based on path optimization algorithm[J]. Journal of the China Railway Society, 2013, 35(6): 53-58. doi: 10.3969/j.issn.1001-8360.2013.06.009 [4] 赵显琼,郑伟,唐涛. 一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用[J]. 铁道学报,2012,34(5): 70-80. doi: 10.3969/j.issn.1001-8360.2012.05.012ZHAO Xianqiong, ZHENG Wei, TANG Tao. Model-based formal approach for generating test cases and test sequences automatically by example of the ETCS-2[J]. Journal of the China Railway Society, 2012, 34(5): 70-80. doi: 10.3969/j.issn.1001-8360.2012.05.012 [5] 赵晓宇,杨志杰,吕旌阳. 基于有色Petri网的车载设备模式转换测试序列生成方法[J]. 中国铁道科学,2017,38(4): 115-123. doi: 10.3969/j.issn.1001-4632.2017.04.16ZHAO Xiaoyu, YANG Zhijie, LÜ Jingyang. Test sequence generation method of mode transition for on-board equipment based on colored petri net[J]. China Railway Science, 2017, 38(4): 115-123. doi: 10.3969/j.issn.1001-4632.2017.04.16 [6] 王硕,张亚东,郭进,等. 列控中心自动化测试测试用例生成方法[J]. 北京交通大学学报,2020,44(5): 49-54. doi: 10.11860/j.issn.1673-0291.20200052WANG Shuo, ZHANG Yadong, GUO Jin, et al. Generation method of test cases for automated testing of TCC[J]. Journal of Beijing Jiaotong University, 2020, 44(5): 49-54. doi: 10.11860/j.issn.1673-0291.20200052 [7] LV J D, AHMAD E, TANG T. Non-deterministic delay behavior testing of Chinese train control system using UPPAAL-TRON[J]. IEEE Intelligent Transportation Systems Magazine, 2021, 13(3): 58-82. doi: 10.1109/MITS.2019.2953536 [8] 魏柏全,吕继东,陈柯行,等. 基于TAIO变异的CTCS-3列控系统测试案例生成方法[J]. 西南交通大学学报,2020,55(5): 937-945,962. doi: 10.3969/j.issn.0258-2724.20180078WEI Baiquan, LÜ Jidong, CHEN Kexing, et al. Mutation timed automata with input and output-based method of generating test suites for Chinese train control system level 3[J]. Journal of Southwest Jiaotong University, 2020, 55(5): 937-945,962. doi: 10.3969/j.issn.0258-2724.20180078 [9] LI C L, LI K C, TANG T, et al. Model-based generation of safety test-cases for Onboard systems[C]//2013 IEEE International Conference on Intelligent Rail Transportation Proceedings. Beijing: IEEE, 2013: 191-196. [10] 吕继东,朱晓琳,王海峰,等. 基于UPPAAL-TRON的高速铁路列控系统非确定性时延一致性测试研究[J]. 铁道学报,2016,38(1): 54-64. doi: 10.3969/j.issn.1001-8360.2016.01.009LV Jidong, ZHU Xiaolin, WANG Haifeng, et al. Online conformance testing of non-determinism time delay in high-speed train control system using UPPAAL-TRON[J]. Journal of the China Railway Society, 2016, 38(1): 54-64. doi: 10.3969/j.issn.1001-8360.2016.01.009 [11] 曹雅鑫. 基于UML状态图的列控中心轨道电路编码功能测试用例生成方法研究[D]. 成都:西南交通大学,2017. [12] 郑伟,唐涛,吕继东,等. 基于IECP的CTCS-3列控车载TSM曲线完备性测试用例集生成方法研究[J]. 铁道学报,2020,42(5): 72-83. doi: 10.3969/j.issn.1001-8360.2020.05.010ZHENG Wei, TANG Tao, LÜ Jidong, et al. Method of generating completeness test suit based on IECP for CTCS-3 train control TSM profile[J]. Journal of the China Railway Society, 2020, 42(5): 72-83. doi: 10.3969/j.issn.1001-8360.2020.05.010 [13] LV J D, LU W L, WANG T, et al. The search-based mutation testing of the Chinese train control system level 3 on board a train control system[J]. IEEE Intelligent Transportation Systems Magazine, 2022, 14(5): 41-58. doi: 10.1109/MITS.2021.3069900 [14] SUN Y J, LI K C, YUAN L, et al. Safety test case generation of train-ground transmission function for CTCS based on fault models[C]//2019 IEEE Intelligent Transportation Systems Conference (ITSC). Auckland: IEEE, 2019: 3355-3360. [15] 李耀,张晓霞,郭进,等. 高铁信号系统安全关键功能测试建模方法[J]. 西南交通大学学报,2022,57(1): 28-35,45. doi: 10.3969/j.issn.0258-2724.20200378LI Yao, ZHANG Xiaoxia, GUO Jin, et al. Testing modeling method for safety critical function of high-speed railway signal system[J]. Journal of Southwest Jiaotong University, 2022, 57(1): 28-35,45. doi: 10.3969/j.issn.0258-2724.20200378 [16] 李耀,张晓霞,郭进,等. 铁路信号系统软件测试建模方法[J]. 西南交通大学学报,2022,57(2): 392-400,424. doi: 10.3969/j.issn.0258-2724.20200530LI Yao, ZHANG Xiaoxia, GUO Jin, et al. Modeling method for testing railway signal system software[J]. Journal of Southwest Jiaotong University, 2022, 57(2): 392-400,424. doi: 10.3969/j.issn.0258-2724.20200530 [17] AMMANN P, OFFUTT J. Introduction to Software Testing[M]. New York: Cambridge University Press, 2017. [18] 吴彪. 基于EFSM的测试用例自动生成方法的研究[D]. 杭州:浙江理工大学,2016. [19] MIKK E, LAKHNECH Y, PETERSOHN C, et al. On formal semantics of statecharts as supported by STATEMATE[C]//Proceedings of the 2nd BCS-FACS conference on Northern Formal Methods. Ilkley: [s. n.], 1997: 1 -12. [20] 朱雪阳,唐稚松. Statecharts的组合语义与求精[J]. 软件学报,2006,17(4): 670-681. doi: 10.1360/jos170670ZHU Xueyang, TANG Zhisong. Compositional semantics and refinement of statecharts[J]. Journal of Software, 2006, 17(4): 670-681. doi: 10.1360/jos170670 [21] SOLIMAN D, THRAMBOULIDIS K, FREY G. Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applications[J]. Annual Reviews in Control, 2012, 36: 338-345. doi: 10.1016/j.arcontrol.2012.09.015 [22] LI Y, ZHANG X X, ZHANG Y D, et al. Towards A test paths generation method for CTCS level transition[J]. MATEC Web of Conferences, 2020, 325: 1001-1005. doi: 10.1051/matecconf/202032501001 [23] 李兰心,王海峰,齐志华,等. 基于SCADE模型的车载ATP测试用例生成方法[J]. 铁道学报,2020,42(9): 102-110. doi: 10.3969/j.issn.1001-8360.2020.09.013LI Lanxin, WANG Haifeng, QI Zhihua, et al. SCADE model-based method of test cases generation for onboard ATP system[J]. Journal of the China Railway Society, 2020, 42(9): 102-110. doi: 10.3969/j.issn.1001-8360.2020.09.013 [24] 魏柏全. 基于TAIO变异分析的新型列控系统安全功能测试评价研究[D]. 北京:北京交通大学,2018. -
下载:
下载:
点击查看大图
计量
- 文章访问数: 348
- HTML全文浏览量: 85
- PDF下载量: 75
- 被引次数: 0