STP安全通信协议设计与形式化验证
|
摘要
无线调车机车信号和监控系统(STP)是基于无线数传电台,实现车载和地面设备之间双向信息传输的实时信号监控和安全防护系统。为保证系统中车-地之间交互信息的实时性、可靠性与完整性,依据欧标EN50159,在现有ETCS安全通信协议EuroRadio的基础上,通过增加安全连接超时重发、双序号时间戳和故障导向安全机制,设计一套适用于STP系统的安全通信协议,并利用分层着色Petri网和ASK-CTL时序逻辑验证语言对其进行建模和形式化验证。分析结果表明,该协议不仅满足功能安全性要求,同时还能保证系统在非理想信道环境下的故障导向安全。
The STP system is based on data-transmission radio. By the data transmission between the mobile equipment and the ground equipment,it can realize the real-time monitoring of train signal,which is used to ensure the safety protection of the train. To make sure that the information,which transmits by wireless to be real-time,reliable and complete,this paper designs a safety communication protocol for STP. According to En50159,it adds some extra safety measures,such as timeout,sequence-number and so on in STP safe communication protocol,which is based on EuroRadio,to ensure the communication system to be fail-safe. And it uses hierarchical Colored Petri Net( CPN) and ASK-CTL formula to build hierarchy models and make formal verification of the proposed protocol. Analysis results show that the proposed protocol for STP has the functional safety,and it also can be fail-safe,even though the transmission happens during the undesired channel.
The STP system is based on data-transmission radio. By the data transmission between the mobile equipment and the ground equipment,it can realize the real-time monitoring of train signal,which is used to ensure the safety protection of the train. To make sure that the information,which transmits by wireless to be real-time,reliable and complete,this paper designs a safety communication protocol for STP. According to En50159,it adds some extra safety measures,such as timeout,sequence-number and so on in STP safe communication protocol,which is based on EuroRadio,to ensure the communication system to be fail-safe. And it uses hierarchical Colored Petri Net( CPN) and ASK-CTL formula to build hierarchy models and make formal verification of the proposed protocol. Analysis results show that the proposed protocol for STP has the functional safety,and it also can be fail-safe,even though the transmission happens during the undesired channel.
引文
[1]申旭光,郭其一,成远.无线调车机车信号和监控系统车地通信的模型设计[J].机车电传动,2007(5):34-36.
[2]曹桂均,林通源.调车机车信号和监控系统[J].铁路工程,2006,3(2):7-10.
[3]林炳跃.基于UPPAAL的无线调车机车信号和监控系统的建模与分析[D].北京:中国铁道科学研究院,2009.
[4] ERTM S. EuroRadio FIS:class 1 requirements:SUBSET-037V225[S]. 2003.
[5] CENELE C. Railway application-communication,signaling and processing systems-part2:safety-related communication in open transmission systems:EN50159-2[S]. 2001.
[6]陈黎洁,单振宇,唐涛.列车运行控制系统中安全通信协议的形式化分析[J].铁道学报,2012,34(7):70-76.
[7]单振宇. CTCS-3级车地通信协议设计与验证[D].北京:北京交通大学,2009.
[8]曹桂均,冯军,杨华昌.无线调车机车信号和监控系统暂行技术规范:TJ/DW035-2014[S]. 2014.
[9]胡晓辉,陈慧丽,石广田,等. CTCT-4级安全通信协议的形式化建模与验证[J].计算机工程与应用,2014,50(4):81-85.
[10]于宏博,钟章队. ETCS中安全通信的研究与探讨[J].铁道通信信号,2005,41(1):30-33.
[11]杨明,邱昕夕,陈祥献,等. CBTC中安全通信协议的设计与仿真研究[J].计算机工程,2012,38(19):241-246.
[12]陈黎洁.列车运行控制系统安全通信协议验证方法的研究[D].北京:北京交通大学,2013.
[13] JENSEN K. A brief introduction to colored Petri nets[M]. Berlin,Germany:Springer,1997.
[14]徐田华,赵红礼,唐涛.基于有色Petri网的ETCS无线通信可靠性分析[J].铁道学报,2008,30(1):38-42.
[15]徐亮,余建平.改进的验证正确性ACTL性质的限界模型检测方法[J].计算机科学,2013,40(6A):99-102.
[16]苏开乐,骆翔宇,吕关锋.符号化模型检测CTL*[J].计算机学报,2005,28(11):1798-1806.
[17] GIRAULT C. Petri nets for systems engineering[M].Berlin,Germany:Springer,2010.
[2]曹桂均,林通源.调车机车信号和监控系统[J].铁路工程,2006,3(2):7-10.
[3]林炳跃.基于UPPAAL的无线调车机车信号和监控系统的建模与分析[D].北京:中国铁道科学研究院,2009.
[4] ERTM S. EuroRadio FIS:class 1 requirements:SUBSET-037V225[S]. 2003.
[5] CENELE C. Railway application-communication,signaling and processing systems-part2:safety-related communication in open transmission systems:EN50159-2[S]. 2001.
[6]陈黎洁,单振宇,唐涛.列车运行控制系统中安全通信协议的形式化分析[J].铁道学报,2012,34(7):70-76.
[7]单振宇. CTCS-3级车地通信协议设计与验证[D].北京:北京交通大学,2009.
[8]曹桂均,冯军,杨华昌.无线调车机车信号和监控系统暂行技术规范:TJ/DW035-2014[S]. 2014.
[9]胡晓辉,陈慧丽,石广田,等. CTCT-4级安全通信协议的形式化建模与验证[J].计算机工程与应用,2014,50(4):81-85.
[10]于宏博,钟章队. ETCS中安全通信的研究与探讨[J].铁道通信信号,2005,41(1):30-33.
[11]杨明,邱昕夕,陈祥献,等. CBTC中安全通信协议的设计与仿真研究[J].计算机工程,2012,38(19):241-246.
[12]陈黎洁.列车运行控制系统安全通信协议验证方法的研究[D].北京:北京交通大学,2013.
[13] JENSEN K. A brief introduction to colored Petri nets[M]. Berlin,Germany:Springer,1997.
[14]徐田华,赵红礼,唐涛.基于有色Petri网的ETCS无线通信可靠性分析[J].铁道学报,2008,30(1):38-42.
[15]徐亮,余建平.改进的验证正确性ACTL性质的限界模型检测方法[J].计算机科学,2013,40(6A):99-102.
[16]苏开乐,骆翔宇,吕关锋.符号化模型检测CTL*[J].计算机学报,2005,28(11):1798-1806.
[17] GIRAULT C. Petri nets for systems engineering[M].Berlin,Germany:Springer,2010.