我国高铁运营里程已经超过2.9万公里，占世界高铁运营里程的2/3以上，累计运输旅客超过100亿人次. 我国已成为世界上高铁运营里程最长、运输密度最高、运营场景最复杂的国家. 高铁信号系统具有SIL4级的安全需求，安全关键功能一旦失效可能造成列车追尾、脱轨等行车事故，导致人员伤亡及重大财产损失^[1]. 保证高铁信号系统安全关键功能的安全性对我国高铁的安全运营、国家“高铁走出去”具有重要意义.

基于模型的测试是目前高铁信号系统安全关键功能安全性测试的研究热点，常用的测试建模方法包括时间自动机（timed automata，TA）、UML Statechart和Petri网（Petri net）等，研究内容重点关注如何从安全关键功能的测试模型生成覆盖全面且高效的测试用例. 文献[2]针对ATP （automatic train protection）系统模式转换功能测试用例难以实现全覆盖的问题，采用TA建模方法建立测试模型，提出满足全状态和全变迁覆盖准则的测试用例生成方法，提高测试用例的生成效率和重用性. 文献[3]以RBC （radio block center）切换功能为例，提出基于TA和HCSP （hybrid communication sequential process）的测试建模方法，研究全状态和全变迁覆盖的测试用例自动生成方法，列控系统测试用例的生成效率提高30%. 文献[4]以TA作为测试建模的基础理论，通过在测试模型中注入故障的方式提高测试用例的全面性. 文献[5]基于TA建模理论，提出输入输出时间自动机（timed automata with input and output, TAIO）建模方法，提出基于TAIO变异分析的列控系统安全关键功能测试框架. 文献[6]以有色Petri网（colored Petri net，CPN）作为测试建模的理论基础，通过状态空间搜索自动生成车地通信功能的测试用例，提高测试用例生成的自动化程度. 文献[7]针对ATP系统模式转换功能，建立CPN测试模型，解决状态空间爆炸和搜索死循环的问题，生成满足全路径覆盖准则的测试序列集. 文献[8]针对列控中心轨道电路编码功能，研究UML Statechart测试建模方法，提出图覆盖、组合覆盖和文法分析相结合的方式自动生成测试用例. 文献[9]针对列控中心改变运动方向功能，建立UML Statechart测试模型，研究基于UML Statechart模型自动生成覆盖全面的测试用例的算法，为自动化测试提供基础.

目前的研究丰富了高铁信号系统的测试用例，提高了测试活动的自动化程度和测试效率，但对高铁信号系统安全关键功能测试建模理论的研究相对较少. 目前主要采用的测试建模方法没有很好地针对高铁信号系统功能逻辑和时钟约束的特点，导致测试模型复杂，测试用例缺少时钟约束. 首先，详细分析高铁信号系统测试模型的建模需求；然后，在有限状态机理论的基础上从功能逻辑和时钟约束2个方面提出时间状态机建模方法；最后，以计算机联锁道岔子系统为例进行了分析，为基于模型的高铁信号系统测试提供新的建模理论.

1.   问题描述

1.1   高铁信号系统测试用例生成方法概述

基于模型的测试（model-based testing，MBT）^[10]理论是高铁信号系统安全关键功能测试用例生成的研究重点内容之一. MBT属于基于规范的测试范畴，其编制测试用例和评判测试结果时均以被测系统（system under test，SUT）的测试模型作为依据. MBT已经在高铁信号系统RBC、ATP和CBI （computer based interlocking）等设备的安全关键功能测试中得到重点研究^[11-14]. 实践表明，该方法能够有效地发现系统问题，提高测试效率和自动化程度.

基于模型的测试主要包括分析被测系统需求、建立测试模型、生成抽象测试用例、具体化抽象测试用例、执行测试和分析测试结果6个阶段. 首先，基于被测系统的需求规格等文件对系统功能和结构进行抽象，建立系统的测试模型；其次，依据测试模型，选取测试覆盖准则自动生成抽象测试用例；然后，结合行业知识将抽象测试用例实例化为可执行的测试用例；最后，将测试用例加载到测试环境中执行测试，观察、分析测试结果.

1.2   高铁信号系统测试建模的问题

测试模型是高铁信号系统测试用例编制的基础. 目前，高铁信号系统的测试建模方法不是针对信号系统安全关键功能测试的领域建模方法，不能很好、完整地描述高铁信号系统的行为特征. 模典型的高铁信号系统测试建方法包括有限状态机（finite state machine, FSM）、UML Statechart、TA和Petri网等，其中，FSM、UML Statechart和Petri网等方法不具有描述时钟约束的能力，导致该模型生成的测试用例不能反映系统的时间特性，不能满足测试活动的全面性和完备性要求. TA能够描述系统的时钟约束，但不具有层次结构，对复杂功能逻辑的描述能力较差，不易描述高铁信号系统安全关键功能的全部行为，容易出现状态数量爆炸、测试模型难以理解、甚至错误的问题.

在安全关键系统形式化建模和分析领域，研究学者提出了timed color Petri nets^[15]、Safecharts^[16]、SyncCharts^[17]、RTSC^[18] 、UML RT-Statechart^[19]和TSSM^[20]等建模方法，解决了安全关键功能复杂逻辑和时钟约束的形式化描述和验证问题. 但针对高铁信号系统测试，这些建模方法的语法、语义复杂，测试模型解析和测试用例生成难度较大，不易直接应用在高铁信号系统的测试活动中. 因此，研究适合于高铁信号系统测试领域的形式化建模方法对高铁信号系统安全关键功能的测试具有一定的意义.

2.   高铁信号系统测试建模需求

测试模型作为高铁信号系统测试理论的重要基础，需要尽可能全面、清晰地呈现被测系统的行为特性. 本节针对高铁信号系统的特点，分析高铁信号系统测试活动的测试建模需求.

根据高铁信号系统测试活动的过程和目标，高铁信号系统测试建模包括功能建模需求和性能建模需求两个方面. 功能建模需求描述系统的功能逻辑（function logic），明确系统需要满足的安全条件；性能建模需求指与系统功能相关的时钟约束或限制（clock constraint）.

1） 功能逻辑

随着计算机和通信技术的发展，高铁信号系统承担的安全功能越来越多，功能逻辑越来越复杂. 如CTCS-3级列控系统包括9种工作模式，14个主要运营场景，206个功能特征^[21]. 高铁信号系统已构成一个复杂的控制系统，存在着大量的并发、竞争和冲突等逻辑关系，控制状态转移条件复杂. 高铁信号系统测试模型需要满足功能逻辑的复杂性和并发性，严密、准确地反应系统的功能需求，且具有良好的可读性和可理解性.

2） 时钟约束

高铁信号系统安全关键功能运算结果的安全性和正确性不仅取决于系统逻辑的处理过程，还取决于运算过程中的时钟约束，属于典型的实时系统（real-time system）. 高铁信号系统的时钟约束主要指系统功能需要在指定的时间内完成，或在规定的时限之后才能发生. 如《CTCS-3级列控系统测试案例（V3.0）》^[21]功能特征190的测试用例3要求“司机未在5秒内进行确认，实施最大常用制动”. 而且，安全关键功能的时钟约束通常为硬实时性要求，如道岔转换时间、RBC交互时间、MA （movement authority）有效时间等^[22]，时钟约束错误或缺失，可能造成重大安全事故.

根据以上分析，高铁信号系统安全关键功能的测试建模方法需要能够很好地描述系统复杂的功能逻辑和时钟约束.

3.   时间状态机测试建模方法

有限状态机（finite state machine, FSM）是MBT理论中经典的测试建模方法^[23-24]，其通过可视化的方式描述系统的功能逻辑，具有清晰、直观的优点. 本节在FSM的基础上扩展出时间状态机建模方法，首先介绍FSM的定义，然后在FSM的迁移中扩展出时钟约束，结合Z规格说明语言给出时间状态机的定义.

3.1   有限状态机概述

FSM是表示有限状态以及状态之间转移和动作等行为的数学模型，具有精确性、可推导性和可验证性.

定义1 （有限状态机）　一个有限状态机M是个六元组，如式（1）^[24].

式中：S为有限状态集合；${s_0}$为初始状态，${s_0} \in S$；λ为状态转移函数，$\lambda : S I \to S$；δ为输出函数，$\delta : S I \to O$；I为有限输入符号集合；O为有限输出符号集合.

图1为一个开关的FSM模型.

图  1  有限状态机示例

Figure  1.  Example of finite state machine

下载: 全尺寸图片 幻灯片

图1中包括关（s_off）和开（s_on）两个状态，其中s_off为初始状态. s_off接收到输入A时转移到s_on状态，输出$A{'}$，s_on接收到输入B时转移到s_off状态，输出$B{'}$. 模型对应的六元组如式（2）.

根据FSM的定义，FSM缺少描述时钟约束的机制. 接下来结合Z规格说明语言，在FSM描述功能逻辑的基础上，增加层次结构，扩展出时钟约束，提出时间状态机（timed finite state machine，TFSM）.

3.2   TFSM基本元素

TFSM包括时钟、信号和状态等基本元素.

1） 时钟

TFSM采用时钟描述时间的流逝，有限时钟集合记为C，Z语言描述如下：

[C]

$\exists$ m: $\mathbb{N}$ • #C = m

TFSM时钟约束集合记为Ψ，Z语言描述如下：

[Ψ]

$\exists$ m : $\mathbb{N}$ • #Ψ = m

对一个时钟变量集合C，Ψ具有如下形式：

$\varPsi {\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt} ::{\kern 1pt} {\kern 1pt} {\kern 1pt} = {\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt} x \propto d|{\psi _1} \wedge {\psi _2}$，

式中：${\psi _1}$、${\psi _{\text{2}}}$为时钟约束；$x \in C$；$d \in \mathbb{N}$；$\propto \in \{ \leqslant , < , \geqslant , > , = \}$.

2） 信号

信号具有产生和不产生两种状态，Z语言描述如下：

[G]

$\exists$ m: $\mathbb{N}$ • #G = m

TFSM在某一时刻，其他正交组件产生的信号称为动作.

3） 状态

状态是高铁信号系统安全关键功能在一定时期内的存在形式. TFSM的非空、有限状态集合记为S，Z语言描述如下：

[S]

$\exists$m: $\mathbb{N}$₁ • #S = m

状态类型包括简单状态（PRIM），或状态（OR）和与状态（AND） 3种，Z语言描述如下：

P ::= PRIM | OR | AND

4） 迁移

迁移T是TFSM从源状态转移到目标状态的方式，包括源状态s_c、信号g、时钟约束ψ、转移时产生的动作a、重置的时钟c及目标状态s_t. 迁移的Z语言描述如下：

OR状态由同层次的状态和迁移组成，包含且仅包含一个初始状态，初始状态为无源状态，且是任意状态的源状态. 多个并发的OR状态组成AND状态.

3.3   TFSM定义

本小节在TFSM基本元素的基础上，采用Z规格说明语言定义TFSM的层次结构，给出TFSM的定义.

TFSM的状态层次Π包括底状态γ、为状态分配子状态的有限状态层次函数h，定义状态类型的有限状态类型函数ε，定义状态父状态的函数d，满足以下性质：

1） h为非PRIM类型的状态分配子状态，且状态层次不能形成循环结构；

2） γ不为PRIM状态，是唯一没有父状态的状态；

3） 任意非γ的状态都具有唯一的父状态，且均可以由γ通过h传递到达.

Π的Z模式定义如下，其中：$\mathbb{F}\;S$表示集合S的所有有限子集的集合，dom h表示h的定义域，ran h表示h的值域.

TFSM由状态层次π和迁移集t_s构成. 对任意迁移，仅有一个同层次的源状态和目标状态. 源状态和目标状态可以是AND或PRIM状态. Z模式定义如下，其中：$\mathbb{F}_1T$表示集合T的所有非空有限子集的集合.

3.4   TFSM格局

一个时钟集合C的时钟解释v是指每个时钟变量c到时间序列上的一个全映射. 某时刻，TFSM能够同时处于的最大的状态集结合当前的时钟解释称为格局（configuration），记为u，格局对应的状态集记为$u'$，初始格局记为u₀，初始格局对应的状态集记为${u'_0}$. 在任意时刻，TFSM只有一个活动的格局，满足以下规则：

1） $u'$ 包含γ状态；

2） $u'$ 包含AND状态s，则 $u'$ 包含s的每个子状态；

3） $u'$ 包含OR状态s，则 $u'$ 包含s的某个子状态；

4） $u'$ 包含非γ的状态s，则 $u'$ 包含s的父状态.

TFSM格局的公理描述如下：

4.   基于TFSM的测试用例生成方法

本节给出基于TFSM自动生成测试用例的方法. 目前，针对TA和Petri网等测试模型，研究学者已经提出了许多相对成熟的测试用例自动生成算法. 由于TA能够同时描述功能逻辑和时钟约束，本节将TFSM等价转换为TA，利用基于TA的测试用例生成算法自动生成TFSM的测试用例.

定义2 （时间自动机）　一个时间自动机TA是一个六元组$(L,{l_0},\varSigma ,X,M,E)$，其中：L为有限位置集合；${l_0} \in L$为初始位置；$\varSigma$为有限字符集合；X为有限时钟集合；M为将位置映射到时钟约束的映射；E为转移的集合，$E \subseteq L \varSigma \times {2^x} \varPhi \left( X \right) L$，$\varPhi \left( X \right)$为时钟约束集合.

定义3 （TFSM测试用例）　对任意TFSM，如果从格局u_i能够到达格局u_j，i,j≥0，则TFSM中u_i和u_j之间存在一条路径，称该路径为TFSM中以u_i和u_j为测试需求的测试用例.

定义4 （TA测试用例）　对任意TA，如果从位置l_i沿TA中的边能够到达l_j，i,j≥0，则TA中l_i和l_j之间存在一条路径，称该路径为TA中以l_i和l_j节点为测试需求的测试用例.

定理1　设$\kappa$为一个TFSM向一个六元组$(L,{l_0},\varSigma ,X,M,E)$的映射，且

$L{\kern 1pt} {\kern 1pt} {\kern 1pt} {\text{ = }}{\kern 1pt} u'$；

${l_0}{\text{ = }}{\kern 1pt} {\kern 1pt} {\kern 1pt} {u'_0}$；

$\varSigma = G$；

$X = C$；

$M:L \to \varnothing$；

$E \subseteq L \varSigma \times {2^x} \varPhi \left( X \right) L$；

$\forall {l_1},{l_2} \in L$，$\varsigma \in \varSigma$，$x \subseteq X$，$\varphi \in \varPhi \left( X \right)$，$\left( {{l_1},\varsigma ,x,\varphi ,{l_2}} \right) \in E{\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt} \Rightarrow \exists {u_1},{u_2} \in u'$，${u_1} = {l_1}$，${u_2} = {l_2}$，${u_1}\xrightarrow{{\varsigma ,x,\varphi }}{u_2}$，且$\forall {u_1}, {u_2} \in u'$, $g \subseteq G$，${\kern 1pt} {\kern 1pt} c \subseteq C,{\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt} \psi \in \Psi ,{\kern 1pt} {\kern 1pt} {\kern 1pt} {\kern 1pt}$${u_1}\xrightarrow{{g,c,\psi }}{u_2}$$\Rightarrow {\kern 1pt} {\kern 1pt} \exists {l_1},{l_2} \in L{\kern 1pt}$，${\kern 1pt} \left( {{l_1},g,c,\psi ,{l_2}} \right) \in E$，则$(L,{l_0},\varSigma ,X,M,E)$是一个与TFSM具有相同测试用例集的TA.

证明　根据$\kappa$的定义，TFSM的格局状态集对应TA的位置集，TFSM的初始格局状态对应TA的初始位置，TFSM的信号集和时钟集分别对应为TA的有限字符集和时钟集，即$\kappa$将TFSM映射为一个所有位置均无时钟约束的TA. 对任意TA，$\forall {l_1},{l_2} \in L$，$\left( {{l_1},{l_2}} \right) \in E$，则TFSM中$\exists {u_1},{u_2} \in u'$，${u_1} = {l_1}$，${u_{\text{2}}} = {l_{\text{2}}}$. 根据$\kappa$的定义有${u_1} \to {u_2}$. 故TA中的任意测试用例${l_0},{l_1},\cdots$ 对应TFSM中的一条测试用例${u_0},{u_1}, \cdots$.

由定理1，TFSM的测试用例与TA的测试用例一一对应，如图2所示.

根据以上分析，基于TFSM的高铁信号系统测试用例生成的主要过程如下：首先，测试人员采用TFSM建模方法建立高铁信号系统安全关键功能的测试模型；然后，根据TFSM和TA测试用例集之间的一致性，将TFSM模型转化为TA模型，利用基于TA的高铁信号系统测试理论，对TA模型编制测试用例；最后，将测试用例加载到测试环境中进行测试，分析测试结果.

图  2  TFSM与TA的测试用例的关系

Figure  2.  Relationship of test cases between TFSM and TA

下载: 全尺寸图片 幻灯片

5.   案例分析

计算机联锁系统是高铁信号系统中典型的安全关键系统，具有SIL4的安全完整性要求. 本节以计算机联锁系统中的道岔定位选排子系统为例建立TFSM测试模型，并转换为TA模型编制测试用例.

5.1   基于TFSM的道岔转换测试模型

道岔定位选排子系统根据道岔操作命令或进路请求，检查道岔当前是否处于定位. 当道岔状态与期望不一致时，选排道岔到需求位置. 该系统涉及11个信号，信号名称及其含义如表1所示.

表  1  道岔子系统信号的含义

Table  1.  Meaning of signals in the switch subsystem

信号	含义		信号	含义
g1	反位请求		g2	定位需求
g3	正在转换		g4	请求转换
g5	道岔锁闭		g6	选排一致
g7	道岔定位		g8	道岔未锁闭
g9	道岔未在定位		g10	道岔未转换
g11	道岔定位操作

下载: 导出CSV 

| 显示表格

道岔定位选排子系统的TFSM测试模型记为D_{TFSM_SW}，如图3所示.

D_{TFSM_SW}包括1个时钟x，初始状态为$\left\{ {{s_{\text{1}}},{s_{\text{2}}},{s_{\text{4}}}} \right\}{\text{，}}$ ${\kern 0.5pt}\gamma = \left\{ {{s_{\text{0}}}} \right\} {\text{，}} \varepsilon \left( {{s_{\text{4}}}} \right)$为PRIM状态，$\varepsilon \left( {{s_{\text{1}}}} \right)$为OR状态，$d\left( {{s_2}} \right) =$${s_1} {\text{，}} h\left({s}_{\text{1}}\right)\text{=} \left\{{s}_{\text{2}},{s}_{\text{10}},{s}_{\text{11}}\right\}， {\kern 0.5pt} h\left( {{s_2}} \right){\text{ = }}\left\{ {{s_4},{s_5},{s_6},{s_7},{s_8},{s_9}} \right\}$.

5.2   测试用例生成

D_{TFSM_SW}通过11个状态、15条迁移和11个信号描述道岔转换过程的功能逻辑，通过时钟约束x > 1、x < 13和x ≥ 13描述道岔转换过程中的信号保持时间1 s和转换超时时间13 s的时钟约束，为测试用例生成提供了模型基础.

D_{TFSM_SW}等价的TA模型D_{TA_SW}如图4所示. D_{TA_SW}包括37条边和9个节点，为描述方便，D_{TA_SW}的状态名仅包括D_{TFSM_SW}格局中的PRIM状态.

图  3  道岔定位选排测试模型

Figure  3.  Testing model of switch subsystem

下载: 全尺寸图片 幻灯片

D_{TA_SW}的测试用例即为道岔定位选排子系统D_{TFSM_SW}的测试用例. 为检测TFSM编制测试用例的效果，本节基于文献[14]提出的基于模型的测试用例生成方法，以s₄为测试模型的开始节点和终止节点编制测试用例. 高铁信号系统测试模型典型的测试覆盖准则包括节点覆盖（node coverage，NC）、边覆盖（edge coverage，EC）、边对覆盖（edge-pair coverage，EPC）、完全路径覆盖（complete path coverage，CPC）、主路径覆盖（prime path coverage，PPC）和特定路径覆盖（specified path coverage，SPC）等. 本节以NC、EC、EPC和CPC覆盖准则为例，生成的测试用例如表2所示，其中用例总数表示D_{TFSM_SW}的测试用例数量，时钟约束用例数表示D_{TFSM_SW}中测试时钟约束的用例数量.

5.3   TFSM建模方法对比

为检验TFSM的建模能力，对道岔定位选排的TFSM模型与TA模型进行对比，如表3所示，其中，D_{TFSM_SW}的状态数为除去表示层次的OR状态后的状态数量.

由表3可知，D_{TFSM_SW}与D_{TA_SW}具有相同的状态数和信号数，但D_{TA_SW}的变迁数超过D_{TFSM_SW}的2倍，导致模型更为复杂. 且随着高铁信号系统功能逻辑复杂度的增加，TA模型的变迁数急剧增加，模型的可读性下降，容易导致模型错误. 与TA相比，TFSM更加直观、清晰，可读性良好，更适合描述高铁信号系统复杂的功能逻辑.

图  4  D_{TFSM_SW}等价的TA模型D_{TA_SW}

Figure  4.  TA model D_{TA_SW} equivalent to D_{TFSM_SW}

下载: 全尺寸图片 幻灯片

表  2  D_{TFSM_SW}测试用例统计

Table  2.  Test case statistics of D_{TFSM_SW}

覆盖准则	用例总数/个	时钟约束用例/个
NC	1	1
EC	28	8
EPC	32	8
CPC	52	16

下载: 导出CSV 

| 显示表格

表  3  D_{TFSM_SW}与D_{TA_SW}对比

Table  3.  Comparison of D_{TFSM_SW} and D_{TA_SW}

模型	状态/个	变迁/条	信号/个
DTFSM_SW	9	15	11
DTA_SW	9	37	11

下载: 导出CSV 

| 显示表格

为检验TFSM在编制测试用例方面的有效性，选择高铁信号系统安全关键功能中广泛采用的Petri网和UML Statechart建模方法对道岔定位选排子系统进行建模，以CPC覆盖准则为例编制测试用例，对比结果如表4所示.

由表4可知，TFSM、Petri网和UML Statechart建模方法在功能逻辑方面生成的测试用例数相同，但TFSM比Petri网和UML Statechart多生成了16条具有时钟约束的测试用例，如表5所示.

表  4  不同建模方法生成的测试用例对比

Table  4.  Comparison of test cases generated by different modeling methods

建模方法	功能逻辑 用例/个	时钟约束 用例/条
TFSM	36	16
Petri	36	0
UML Statechart	36	0

下载: 导出CSV 

| 显示表格

根据以上分析，TFSM建模方法适合描述高铁信号系统安全关键功能复杂的逻辑，并生成全面的覆盖功能逻辑和时钟约束的测试用例，能够满足高铁信号系统安全关键功能在功能逻辑和时钟约束方面的测试建模需求.

表  5  D_{TFSM_SW}具有时钟约束的测试案例

Table  5.  Test cases with clock constraints of D_{TFSM_SW}

序号	时钟约束测试案例		序号	时钟约束测试案例
1	g2, g8, g9, g10, x＞1, g1		9	g2, g8, g9, g10, x＞1, g9, x≥13
2	g2, g8, g9, g10, x＞1, g3		10	g2, g8, g9, g10, x＞1, g1
3	g2, g8, g9, g10, x＞1, g5		11	g2, g8, g9, g10, x＞1, g7, x＜13, g1
4	g2, g8, g9, g10, x＞1, g7		12	g2, g8, g9, g10, x＞1, g7, x＜13, g1
5	g11, g8, g9, g10, x＞1, g1		13	g11, g8, g9, g10, x＞1, g9, x≥13
6	g11, g8, g9, g10, x＞1, g3		14	g11, g8, g9, g10, x＞1, g1
7	g11, g8, g9, g10, x＞1, g5		15	g11, g8, g9, g10, x＞1, g7, x＜13, g1
8	g11, g8, g9, g10, x＞1, g7		16	g11, g8, g9, g10, x＞1, g7, x＜13, s3, g1

下载: 导出CSV 

| 显示表格

6.   结　论

1） 高铁信号系统安全关键功能的测试建模方法不能很好地描述系统特征，不具有描述时钟约束的能力，或难以描述安全关键功能逻辑的复杂性.

2） 本文提出的时间状态机建模方法以有限状态机理论为基础，具有严格的形式化定义，能够等价转化为时间自动机结构.

3） 通过道岔子系统的案例分析，时间状态机能够满足高铁信号系统安全关键功能在功能逻辑和时钟约束方面的测试建模需求，为高铁信号系统测试提供了形式化建模的理论基础.

4） 本文提出的方法已在高铁信号系统的计算机联锁和ATP设备的系统测试中得到应用，实践表明该方法能够提高高铁信号系统安全关键功能测试的完备性和测试效率.

致谢：本文工作得到高铁信号工程列控系统第三方仿真测试技术研究（N2018G062）项目的资助.