论文部分内容阅读
[摘要]在CTCS-3级列控系统中，RBC切换是车载设备的关键功能之一，它严重影响着列车的行车效率。本文采用随机Petri网层次化建模思想，对基于一部车载电台RBC切换方式进行建模和分析。建立了GSM-R故障模型为最底层模型，之后建立了周期性消息模型和非周期性消息模型，在此之上建立了RBC切换模型。最后，利用建模仿真软件TimeNET进行了仿真实验，以基于一部车载电台的RBC切换为例进行了分析，得到在不同列车运行速度和不同消息重发时间间隔对RBC切换成功率和切换时间的影响。
[关键词]列控系统；RBC切换；建模；随机Petri网；
Modeling and Analysis of CTCS-3 RBC Handover Based on SPN
[Abstract]In the CTCS-3 Train Control System,RBC Handover is one of the key functions of CTCS-3 On-Board Equipment,it seriously affects the train travel efficiency.In this paper,the RBC Handover with one MT2 is modeled analyzed with hierarchical modeling idea.Firstly,we had established the GSM-R application layer model.Secondly,we had modeled the periodic message and non-periodic message based on the GSM-R application layer model,then we could get the RBC Handover model.Finally,the RBC Handover with one MT2 was analyzed by using TimeNET.While we analyzed the factors which affect the RBC Handover success rate,such as the train speed,the message retransmission time interval.
[Key words]Train control system; RBC Handover; model; Stochastic Petri net;
中图分类号:U21 文献标识码:A 文章编号:1009-914X(2013)28-0018-03
为了确保列车运行安全、提高铁路运输效率，迫切需要装备性能先进、安全可靠的列车运行控制系统。中国列车运行控制系统CTCS（Chinese Train Control System）根据功能要求和设备配置将它划分0～4级五个应用等级。其中CTCS-3级列控系统是保证高速列车运行安全、高效的核心技术之一，它包括地面设备和车载设备。
RBC切换作为CTCS-3级列控系统车载设备的主要功能之一，它直接影响着高速列车的运行安全和运行效率。因此对RBC切换，尤其是对基于一部车载电台（比较恶劣条件）的RBC切换进行建模、仿真和验证，研究影响RBC切换时间和RBC切换成功率的主要因素，可以为提高车载设备执行RBC切换的成功率以及减少RBC切换时间提供理论指导和技术支持。
1 RBC切换建模工具
本文采用随机Petri网对RBC切换过程进行建模，是因为它对并行、分布系统有着易于描述的特点，适合描述本文中列控系统子系统间的数据以及状态的变换较多的情况。
Petri网的结构元素包括：位置、变迁和弧。位置：用于描述系统的局部状态。位置中包含标记，标记在位置中的变化表示系统处于不同的状态。变迁：用于描述修改系统状态的事件。弧：用于引述事件能够发生的局部状态和由事件引发的局部状态的改变。
随机Petri网变迁的实施过程为：在变迁的输入位置清除一个标记；再在变迁实施的延时中保持这种在输入位置的清除同時也不在变迁的输出位置产生一个标记状态；最后在变迁经过规定的延时后，在变迁的输出位置产生一个标记。
2 RBC切换建模
2.1 模型的结构
为了避免随机Petri网对复杂系统的描述时可能会导致状态空间爆炸问题，采用层次模型和分层分析这种方法来建立模型。本文将RBC切换的建模设计为上层模型，将无线消息传输模型设计成底层模型，采用自下而上的方式建立模型。这样在设计上层模型时只需考虑各子系统之间的交互，使得该模型具有良好的层次结构。本论文的建模结构为：（见图1）
2.2 底层模型
在本文中建立的底层模型主要包括GSM-R故障模型、周期性消息模型和非周期性消息模型。其中，GSM-R故障模型为最底层模型。
在随机Petri网图形表示中，用圆圈表示位置；用扁长方形表示一般时间变迁，用线段表示瞬时变迁，在位置中用黑点表示标记。
2.2.1 GSM-R故障模型
GSM-R故障的原因一般分为三种情况，即链路中断、突发降质以及越区切换。
链路中断是指GSM-R的通信链路有时会以很小的概率发生中断，当GSM-R设备检测到通信链路中断后，会再次尝试连接。在规范中要求GSM-R的连接中断概率要小于0.01次/小时，链路中断检测所需时间应小于1秒。在8秒内连接成功的概率为95%，大于10秒则认为连接出现错误。
突发降质是指信道发生的随机的短暂中断，在中断后能自动恢复正常。在规范中规定，无线信道突发降质的持续周期小于1秒的概率为99%，其产生周期大于7秒的概率为99%。
越区切换是指在两个相邻的GSM-R区间交接处会出现通信中止的现象。每个GSM-R无线区间的距离平均为7千米，设列车以v千米每小时的速度行驶，则每隔7/v小时列车经过一次GSM-R的区间交接处。越区切换会导致0.3秒的通信中断。GSM-R故障模型为：(见图2)
其中，位置“P0”表示GSM-R网络处于正常状态。“P1”代表GSM-R处于突发降质状态。“P2”代表GSM-R处于链路中断状态。“P3”表示链路重新连接状态。“P4”代表GSM-R处于越区切换状态。
变迁“T0、T1、T2”分别表示GSM-R从正常状态转入链路中断状态、突发降质状态、越区切换状态。“T3、T5、T6”表示恢复正常状态。“T4”代表链路检测过程。
2.2.2 无线消息模型
（1）周期性消息模型
在发送周期性消息时，接收设备不需要发送应答消息给发送设备，并且发送给接收设备的消息不需要重发，如消息丢失，则等待下一个周期的消息。周期性消息模型为：(见图3)
其中，位置“M”表示待发送的消息。 “UP”代表消息进入上行链路。“R”指消息到达接收端。“P0”表示消息发送失败。
变迁“S”表示消息发送。“T1、GSM-R”分别模拟周期性消息在GSM-R正常、故障情况下的传输延时。“delay”是指经过一定延时，进入下一周期。“re”指GSM-R恢复正常状态。
（2）非周期性消息模型
在发送非周期性消息时，如果让每一个发送周期都判断上一周期发送的消息是否得到回复，这样限制就过于严格。因此规定每经过一定的时间间隔就重新发送一次消息，当重新发送信息的次数达到规定值后（一般为三次），设置一个较大的时间间隔。如果在这个时间间隔中还是没有得到回复确认信息，则认为通信失败。非周期性消息模型为：(见图4)
其中，位置“M”代表待发送的消息。“P0”表示准备发送非周期性消息。“link1、link2、link3”分别表示消息第一、二、三次进入上行链路。“R”表示收到接收设备的回复信息。“F”代表消息发送失败。
变迁“S1”代表消息发送。“D0”是指发送消息进入信道的时间延时。“D1、D2、D3”模拟发送设备接收到接收设备回复信息的时间延时。“L”是指在三次发送后，经过一个大超时阶段。
2.3 顶层模型
在本论文中，顶层模型主要指无线通信管理模型和RBC切换模型。在CTCS-3级列控系统中，由于RBC控制区域有限，一条线路上存在多个RBC的控制区域。列车在线路上运行时，当到达RBC控制区域边界时，列车离开当前所处的RBC控制区域，进入下一个RBC控制区域。列车控制权限从移交RBC转换到接受RBC的过程就是RBC切换。
2.3.1 无线通信管理
（1）建立通信会晤
在车载设备与RBC建立通信会晤之前，先进行通道测试。再判断是否进行了网络注册，网络注册成功后，根据无线通信规范建立安全连接。只有建立了安全连接才能开始建立通信会话流程。建立通信会晤模型为：(见图5)
位置“P0”表示进行通道测试。“P1”代表通道不畅通。“P2”代表进行网络注册判断。“P3”是指与GSM-R进行安全链接。“P4”表示车载向RBC发送通信会话开始信息（消息155）“P5”表示成功和RBC建立通信会话。
变迁“T0、T1”分别表示通道不畅通、畅通。“T2、T3”分别表示网络注册不成功、成功。“T4”代表车载与RBC链接。“T5”收到RBC的系统版本消息（消息32）。
（2）终止通信会晤
当车载设备接收到地面设备的终止通信会晤的命令，或者当车载设备检测到需要终止通信会晤的错误条件，或者在任务开始阶段RBC拒绝列车，则车载设备需要终止通信会晤流程。
车载设备首先向RBC发送通信会话结束（消息156）。RBC收到消息156后，向车载回复通信会话结束确认（消息39）。然后根据无线通信规范释放安全链接。若一直没有收到消息39，则经过规定时间后，释放安全链接。终止通信会话的模型为：(见图6)
其中，位置“P0”表示车载信息组包。“P1”代表发送通信会话结束消息。“P2”表示车载设备释放安全链接。
变迁“T0”表示组包延时时间。“T1”模拟收到RBC发送的消息39。“T2”是指没有收到消息39的延时。
2.3.2 RBC切换模型
基于一部车载电台的RBC切换工作流程为：当列车通过RBC切换预告应答器组时，车载向RBC1发送列車位置报告。RBC1回复车载RBC切换命令（消息131）。当列车车头和车尾分别越过边界时，均向RBC1发送位置报告信息，之后与RBC1执行终止通信会晤流程。切断与RBC1的通信会晤后，车载开始呼叫RBC2，与其建立通信会晤。成功后，车载向RBC2发送消息129，RBC2回复消息8，车载设备与RBC2保持通信会话并接受行车许可，RBC切换结束。基于一部车载电台的RBC切换模型为：(见图7)
其中，位置“P0”表示列车正常控车状态。“P1、P3、P4、P5、P6、P7”代表车载发送给RBC1车载位置信息。“P2”是列车正常控车，直到到达边界。“P8”是车载主动切断与RBC的通信会晤。“P9”车载呼叫RBC2。“P10”代表车载向RBC2发送消息129。“P11”表示降级为CTCS-2级控车。“P12”表示成功切换状态。
变迁“T0”是指列车通过LTA。“T1”代表收到车载发送的RBC切换命令。“T2、T3”分别表示等待列车车头、车尾越过边界延时。“T5、T6、T7、T8”是指等待接收终止通信会晤命令的规定时间。 “T9”车载主动切断与RBC的通信会晤。“T10” 收到RBC发送的消息8。“T11”在规定时间延时后没有收到消息8。“T12”终止通信会晤。“T13”车载呼叫RBC不成功。
3 仿真分析
在本节中，主要根据CTCS系统RBC交接协议规范，在GSM-R故障模型和无线消息模型的基础上，建立基于一部车载电台的RBC切换模型，分别分析在不同列车速度，不同消息重发间隔的情况下，RBC切换的成功率和切换时间长短。
3.1 不同速度对RBC切换成功率影响分析
在GSM-R故障模型中，仅有越区切换跟列车运行速度有关。每个GSM-R无线小区的平均间距是7km，假设列车长度为400m，如果列车以速度v(km/h)行驶，则列车每隔7/v小时进行一次越区切换。如果列车最高运行速度为390 km/h，则40秒的运行距离为4333米。假设从预告点到切换点之间的距离为4333米的情况下，不同列车速度对基于一部车载电台RBC切换用时分布为：(见图8)
由图可知，列车速度越高，通过从预告点到切换点这段距离所用的时间越短，车身通过切换边界所用时间也越短，车载设备进行RBC切换所用时间也越少。
3.2 不同消息重发时间间隔对RBC切换成功率的影响分析
由于无线消息在GSM-R网络故障传输过程中可能会丢失，将导致消息重发，本节研究消息重发时间间隔对RBC切换时间及成功率的影响。
设置车载设备向RBC重发消息的时间间隔分别为1秒、2秒、3秒和4秒。(见图9)
通过实验可以得出，在非周期消息不丢失的情况下，消息重发时间间隔对RBC切换时间没有影响。
4 结束语
在本文中，利用随机Petri网理论为基础，采用层次模型和分层分析方法来建立基于一部车载电台的RBC切换模型。采用该方法使在建立上层模型时只用考虑列控子系统间的信息交互，使模型具有更好的层次结构，同时也能更准确地描述各子系统间的行为。最后在TimeNET建模仿真软件上分析了不同速度、不同消息重发时间间隔情况下，对RBC切换成功率以及切换时间的影响。并得到在一定范围内，提高RBC切换时间，切换成功概率会随之增加；但当切换时间增加到一定程度时，此法无效的结论。
参考文献
[1] 钟文燕.铁路信号系统的Petri网建模与分析研究[D].成都：西南交通大学，2005，5.
[2] 王亚菊，吴江娇. CTCS-3级列控系统RBC切换过程分析[J]. 北京：铁路通信信号，2010,46(4):12-16.
[3] 林闯.随机peitri网和系统性能评价（第二版）[M].北京：清华大学出版社.2005年4月
[4] 牛儒．曹源．唐涛．ETCS-2级列控系统RBC交接协议的形式化分析．北京．北京交通大学．2008．1．3
[5] Wing J M．Woodcock J．Davies J．Modelling and Simulation of Train Control Systems using Petri Nets[C]．Tagungsort．Toulouse．1999．1860—1867．
[关键词]列控系统；RBC切换；建模；随机Petri网；
Modeling and Analysis of CTCS-3 RBC Handover Based on SPN
[Abstract]In the CTCS-3 Train Control System,RBC Handover is one of the key functions of CTCS-3 On-Board Equipment,it seriously affects the train travel efficiency.In this paper,the RBC Handover with one MT2 is modeled analyzed with hierarchical modeling idea.Firstly,we had established the GSM-R application layer model.Secondly,we had modeled the periodic message and non-periodic message based on the GSM-R application layer model,then we could get the RBC Handover model.Finally,the RBC Handover with one MT2 was analyzed by using TimeNET.While we analyzed the factors which affect the RBC Handover success rate,such as the train speed,the message retransmission time interval.
[Key words]Train control system; RBC Handover; model; Stochastic Petri net;
中图分类号:U21 文献标识码:A 文章编号:1009-914X(2013)28-0018-03
为了确保列车运行安全、提高铁路运输效率，迫切需要装备性能先进、安全可靠的列车运行控制系统。中国列车运行控制系统CTCS（Chinese Train Control System）根据功能要求和设备配置将它划分0～4级五个应用等级。其中CTCS-3级列控系统是保证高速列车运行安全、高效的核心技术之一，它包括地面设备和车载设备。
RBC切换作为CTCS-3级列控系统车载设备的主要功能之一，它直接影响着高速列车的运行安全和运行效率。因此对RBC切换，尤其是对基于一部车载电台（比较恶劣条件）的RBC切换进行建模、仿真和验证，研究影响RBC切换时间和RBC切换成功率的主要因素，可以为提高车载设备执行RBC切换的成功率以及减少RBC切换时间提供理论指导和技术支持。
1 RBC切换建模工具
本文采用随机Petri网对RBC切换过程进行建模，是因为它对并行、分布系统有着易于描述的特点，适合描述本文中列控系统子系统间的数据以及状态的变换较多的情况。
Petri网的结构元素包括：位置、变迁和弧。位置：用于描述系统的局部状态。位置中包含标记，标记在位置中的变化表示系统处于不同的状态。变迁：用于描述修改系统状态的事件。弧：用于引述事件能够发生的局部状态和由事件引发的局部状态的改变。
随机Petri网变迁的实施过程为：在变迁的输入位置清除一个标记；再在变迁实施的延时中保持这种在输入位置的清除同時也不在变迁的输出位置产生一个标记状态；最后在变迁经过规定的延时后，在变迁的输出位置产生一个标记。
2 RBC切换建模
2.1 模型的结构
为了避免随机Petri网对复杂系统的描述时可能会导致状态空间爆炸问题，采用层次模型和分层分析这种方法来建立模型。本文将RBC切换的建模设计为上层模型，将无线消息传输模型设计成底层模型，采用自下而上的方式建立模型。这样在设计上层模型时只需考虑各子系统之间的交互，使得该模型具有良好的层次结构。本论文的建模结构为：（见图1）
2.2 底层模型
在本文中建立的底层模型主要包括GSM-R故障模型、周期性消息模型和非周期性消息模型。其中，GSM-R故障模型为最底层模型。
在随机Petri网图形表示中，用圆圈表示位置；用扁长方形表示一般时间变迁，用线段表示瞬时变迁，在位置中用黑点表示标记。
2.2.1 GSM-R故障模型
GSM-R故障的原因一般分为三种情况，即链路中断、突发降质以及越区切换。
链路中断是指GSM-R的通信链路有时会以很小的概率发生中断，当GSM-R设备检测到通信链路中断后，会再次尝试连接。在规范中要求GSM-R的连接中断概率要小于0.01次/小时，链路中断检测所需时间应小于1秒。在8秒内连接成功的概率为95%，大于10秒则认为连接出现错误。
突发降质是指信道发生的随机的短暂中断，在中断后能自动恢复正常。在规范中规定，无线信道突发降质的持续周期小于1秒的概率为99%，其产生周期大于7秒的概率为99%。
越区切换是指在两个相邻的GSM-R区间交接处会出现通信中止的现象。每个GSM-R无线区间的距离平均为7千米，设列车以v千米每小时的速度行驶，则每隔7/v小时列车经过一次GSM-R的区间交接处。越区切换会导致0.3秒的通信中断。GSM-R故障模型为：(见图2)
其中，位置“P0”表示GSM-R网络处于正常状态。“P1”代表GSM-R处于突发降质状态。“P2”代表GSM-R处于链路中断状态。“P3”表示链路重新连接状态。“P4”代表GSM-R处于越区切换状态。
变迁“T0、T1、T2”分别表示GSM-R从正常状态转入链路中断状态、突发降质状态、越区切换状态。“T3、T5、T6”表示恢复正常状态。“T4”代表链路检测过程。
2.2.2 无线消息模型
（1）周期性消息模型
在发送周期性消息时，接收设备不需要发送应答消息给发送设备，并且发送给接收设备的消息不需要重发，如消息丢失，则等待下一个周期的消息。周期性消息模型为：(见图3)
其中，位置“M”表示待发送的消息。 “UP”代表消息进入上行链路。“R”指消息到达接收端。“P0”表示消息发送失败。
变迁“S”表示消息发送。“T1、GSM-R”分别模拟周期性消息在GSM-R正常、故障情况下的传输延时。“delay”是指经过一定延时，进入下一周期。“re”指GSM-R恢复正常状态。
（2）非周期性消息模型
在发送非周期性消息时，如果让每一个发送周期都判断上一周期发送的消息是否得到回复，这样限制就过于严格。因此规定每经过一定的时间间隔就重新发送一次消息，当重新发送信息的次数达到规定值后（一般为三次），设置一个较大的时间间隔。如果在这个时间间隔中还是没有得到回复确认信息，则认为通信失败。非周期性消息模型为：(见图4)
其中，位置“M”代表待发送的消息。“P0”表示准备发送非周期性消息。“link1、link2、link3”分别表示消息第一、二、三次进入上行链路。“R”表示收到接收设备的回复信息。“F”代表消息发送失败。
变迁“S1”代表消息发送。“D0”是指发送消息进入信道的时间延时。“D1、D2、D3”模拟发送设备接收到接收设备回复信息的时间延时。“L”是指在三次发送后，经过一个大超时阶段。
2.3 顶层模型
在本论文中，顶层模型主要指无线通信管理模型和RBC切换模型。在CTCS-3级列控系统中，由于RBC控制区域有限，一条线路上存在多个RBC的控制区域。列车在线路上运行时，当到达RBC控制区域边界时，列车离开当前所处的RBC控制区域，进入下一个RBC控制区域。列车控制权限从移交RBC转换到接受RBC的过程就是RBC切换。
2.3.1 无线通信管理
（1）建立通信会晤
在车载设备与RBC建立通信会晤之前，先进行通道测试。再判断是否进行了网络注册，网络注册成功后，根据无线通信规范建立安全连接。只有建立了安全连接才能开始建立通信会话流程。建立通信会晤模型为：(见图5)
位置“P0”表示进行通道测试。“P1”代表通道不畅通。“P2”代表进行网络注册判断。“P3”是指与GSM-R进行安全链接。“P4”表示车载向RBC发送通信会话开始信息（消息155）“P5”表示成功和RBC建立通信会话。
变迁“T0、T1”分别表示通道不畅通、畅通。“T2、T3”分别表示网络注册不成功、成功。“T4”代表车载与RBC链接。“T5”收到RBC的系统版本消息（消息32）。
（2）终止通信会晤
当车载设备接收到地面设备的终止通信会晤的命令，或者当车载设备检测到需要终止通信会晤的错误条件，或者在任务开始阶段RBC拒绝列车，则车载设备需要终止通信会晤流程。
车载设备首先向RBC发送通信会话结束（消息156）。RBC收到消息156后，向车载回复通信会话结束确认（消息39）。然后根据无线通信规范释放安全链接。若一直没有收到消息39，则经过规定时间后，释放安全链接。终止通信会话的模型为：(见图6)
其中，位置“P0”表示车载信息组包。“P1”代表发送通信会话结束消息。“P2”表示车载设备释放安全链接。
变迁“T0”表示组包延时时间。“T1”模拟收到RBC发送的消息39。“T2”是指没有收到消息39的延时。
2.3.2 RBC切换模型
基于一部车载电台的RBC切换工作流程为：当列车通过RBC切换预告应答器组时，车载向RBC1发送列車位置报告。RBC1回复车载RBC切换命令（消息131）。当列车车头和车尾分别越过边界时，均向RBC1发送位置报告信息，之后与RBC1执行终止通信会晤流程。切断与RBC1的通信会晤后，车载开始呼叫RBC2，与其建立通信会晤。成功后，车载向RBC2发送消息129，RBC2回复消息8，车载设备与RBC2保持通信会话并接受行车许可，RBC切换结束。基于一部车载电台的RBC切换模型为：(见图7)
其中，位置“P0”表示列车正常控车状态。“P1、P3、P4、P5、P6、P7”代表车载发送给RBC1车载位置信息。“P2”是列车正常控车，直到到达边界。“P8”是车载主动切断与RBC的通信会晤。“P9”车载呼叫RBC2。“P10”代表车载向RBC2发送消息129。“P11”表示降级为CTCS-2级控车。“P12”表示成功切换状态。
变迁“T0”是指列车通过LTA。“T1”代表收到车载发送的RBC切换命令。“T2、T3”分别表示等待列车车头、车尾越过边界延时。“T5、T6、T7、T8”是指等待接收终止通信会晤命令的规定时间。 “T9”车载主动切断与RBC的通信会晤。“T10” 收到RBC发送的消息8。“T11”在规定时间延时后没有收到消息8。“T12”终止通信会晤。“T13”车载呼叫RBC不成功。
3 仿真分析
在本节中，主要根据CTCS系统RBC交接协议规范，在GSM-R故障模型和无线消息模型的基础上，建立基于一部车载电台的RBC切换模型，分别分析在不同列车速度，不同消息重发间隔的情况下，RBC切换的成功率和切换时间长短。
3.1 不同速度对RBC切换成功率影响分析
在GSM-R故障模型中，仅有越区切换跟列车运行速度有关。每个GSM-R无线小区的平均间距是7km，假设列车长度为400m，如果列车以速度v(km/h)行驶，则列车每隔7/v小时进行一次越区切换。如果列车最高运行速度为390 km/h，则40秒的运行距离为4333米。假设从预告点到切换点之间的距离为4333米的情况下，不同列车速度对基于一部车载电台RBC切换用时分布为：(见图8)
由图可知，列车速度越高，通过从预告点到切换点这段距离所用的时间越短，车身通过切换边界所用时间也越短，车载设备进行RBC切换所用时间也越少。
3.2 不同消息重发时间间隔对RBC切换成功率的影响分析
由于无线消息在GSM-R网络故障传输过程中可能会丢失，将导致消息重发，本节研究消息重发时间间隔对RBC切换时间及成功率的影响。
设置车载设备向RBC重发消息的时间间隔分别为1秒、2秒、3秒和4秒。(见图9)
通过实验可以得出，在非周期消息不丢失的情况下，消息重发时间间隔对RBC切换时间没有影响。
4 结束语
在本文中，利用随机Petri网理论为基础，采用层次模型和分层分析方法来建立基于一部车载电台的RBC切换模型。采用该方法使在建立上层模型时只用考虑列控子系统间的信息交互，使模型具有更好的层次结构，同时也能更准确地描述各子系统间的行为。最后在TimeNET建模仿真软件上分析了不同速度、不同消息重发时间间隔情况下，对RBC切换成功率以及切换时间的影响。并得到在一定范围内，提高RBC切换时间，切换成功概率会随之增加；但当切换时间增加到一定程度时，此法无效的结论。
参考文献
[1] 钟文燕.铁路信号系统的Petri网建模与分析研究[D].成都：西南交通大学，2005，5.
[2] 王亚菊，吴江娇. CTCS-3级列控系统RBC切换过程分析[J]. 北京：铁路通信信号，2010,46(4):12-16.
[3] 林闯.随机peitri网和系统性能评价（第二版）[M].北京：清华大学出版社.2005年4月
[4] 牛儒．曹源．唐涛．ETCS-2级列控系统RBC交接协议的形式化分析．北京．北京交通大学．2008．1．3
[5] Wing J M．Woodcock J．Davies J．Modelling and Simulation of Train Control Systems using Petri Nets[C]．Tagungsort．Toulouse．1999．1860—1867．