基于SDL的CTCS-3车地通信协议的描述与实现
|
摘要
我国CTCS-3级列车运行控制系统是基于无线通信GSM-R的列车运行控制系统。GSM-R系统为列车运行提供安全、可靠的数据传输通道,实现了车地间双向通信。为确保CTCS-3级列车运行控制系统数据传输的安全性和可靠性,用于抵御各种安全隐患的车地通信协议的正确性及合理性显得尤为重要。
论文首先阐述了CTCS-3级车地通信协议的系统结构,根据数据传输安全相关需求,详细分析了CTCS-3级车地通信协议的安全通信标准。然后,论文选用形式化描述语言SDL和其支撑工具Telelogic TAU,对CTCS-3级车地通信协议状态机进行形式化描述,建立SDL系统模型,并对其进行协同仿真和遍历验证,生成消息序列流图MSC和错误报告,并通过验证说明了该SDL系统模型的准确性。最后,论文在所建SDL系统模型的基础上将其自动转换为C代码,并最终应用与CTCS-3级车地通信协议软件中,该软件已经服务于CTCS-3级列控系统测试评估认证平台。
论文将标准描述语言SDL引入CTCS-3级列控系统,以形式化描述技术为主线对CTCS-3级车地通信协议进行描述与实现,不仅能够从协议描述上消除语言的二义性,而且能够减少实现通信软件的错误,缩短开发周期,降低开发难度。基于SDL协议设计方法实现的CTCS-3级车地通信协议软件在防护数据传输的安全性和可靠性上也有很好的保障,将其成功应用于CTCS-3级列控系统测试评估认证平台能够进一步证明该方法的实用性,对CTCS-3级列控系统的验证和评估测试具有重要的现实意义。
China Train Control System level3is based on GSM-R, offering the safely reliable data transmission channel between the on-board and trackside equipment to achieve the two-way communication between each other. In order to ensure the security and reliability of data transmission, the correctness and reasonableness of CTCS-3communication protocols which is used to against a variety of security risks between on-board and trackside equipment is particularly important.
In the paper, according to security-related data transmission requirements, the protocol system architecture and the safely transfer standard of communication protocol for onboard-trackside equipment in CTCS-3system were described in detail. Then formal description language SDL and its support tool Telelogic TAU were chosen to describe communication protocol for onboard-trackside in CTCS-3system, and established its SDL model. Based on the model, the message sequence diagram and error reporting were generated by the co-simulation and verification, which can verify the accuracy of SDL model. Finally, SDL model were converted into C code automatically, the application program of CTCS-3communication protocol can be obtained to running on CTCS-3certification testing and evaluation platform successfully.
The standard description language SDL was introduced in the paper. Based on the idea of protocol engineering, the communication protocol for onboard-trackside equipment in CTCS-3system were describe using formal description techniques, which not only eliminate language ambiguity in protocol description, but also reduce development errors, shorten development cycles in the process of realizing communication protocol software..
论文首先阐述了CTCS-3级车地通信协议的系统结构,根据数据传输安全相关需求,详细分析了CTCS-3级车地通信协议的安全通信标准。然后,论文选用形式化描述语言SDL和其支撑工具Telelogic TAU,对CTCS-3级车地通信协议状态机进行形式化描述,建立SDL系统模型,并对其进行协同仿真和遍历验证,生成消息序列流图MSC和错误报告,并通过验证说明了该SDL系统模型的准确性。最后,论文在所建SDL系统模型的基础上将其自动转换为C代码,并最终应用与CTCS-3级车地通信协议软件中,该软件已经服务于CTCS-3级列控系统测试评估认证平台。
论文将标准描述语言SDL引入CTCS-3级列控系统,以形式化描述技术为主线对CTCS-3级车地通信协议进行描述与实现,不仅能够从协议描述上消除语言的二义性,而且能够减少实现通信软件的错误,缩短开发周期,降低开发难度。基于SDL协议设计方法实现的CTCS-3级车地通信协议软件在防护数据传输的安全性和可靠性上也有很好的保障,将其成功应用于CTCS-3级列控系统测试评估认证平台能够进一步证明该方法的实用性,对CTCS-3级列控系统的验证和评估测试具有重要的现实意义。
China Train Control System level3is based on GSM-R, offering the safely reliable data transmission channel between the on-board and trackside equipment to achieve the two-way communication between each other. In order to ensure the security and reliability of data transmission, the correctness and reasonableness of CTCS-3communication protocols which is used to against a variety of security risks between on-board and trackside equipment is particularly important.
In the paper, according to security-related data transmission requirements, the protocol system architecture and the safely transfer standard of communication protocol for onboard-trackside equipment in CTCS-3system were described in detail. Then formal description language SDL and its support tool Telelogic TAU were chosen to describe communication protocol for onboard-trackside in CTCS-3system, and established its SDL model. Based on the model, the message sequence diagram and error reporting were generated by the co-simulation and verification, which can verify the accuracy of SDL model. Finally, SDL model were converted into C code automatically, the application program of CTCS-3communication protocol can be obtained to running on CTCS-3certification testing and evaluation platform successfully.
The standard description language SDL was introduced in the paper. Based on the idea of protocol engineering, the communication protocol for onboard-trackside equipment in CTCS-3system were describe using formal description techniques, which not only eliminate language ambiguity in protocol description, but also reduce development errors, shorten development cycles in the process of realizing communication protocol software..
引文
[1]钟章队,李旭,蒋文怡.铁路综合数字移动通信系统[M].北京：中国铁道出版社.2003：342-352.
[2]李开成,卜长堃,毛俊杰,傅世善等.国外铁路通信信号新技术纵览[M].北京：中国铁道出版社.2005,8：4-7.
[3]唐涛,郜春海ETCS系统分析及CTCS的研究[J].湖南：机车电传动,2004,6：49-53.
[4]季学胜,唐涛CTCS-3级列车运行控制系统综合测试平台研究[J].北京：铁道通信信号,2007,43(7)：1-3.
[5]成登高.中国列车运行控制系统(CTCS)技术简介[J].山西：科技情报开发与经济.2007,17(32)：275-276.
[6]单振宇CTCS-3级车地通信协议设计与验证[D].北京.北京交通大学.2009：3-37.
[7]刘雨CBTC系统通信协议的设计和形式化分析[D].北京：北京交通大学.2007：3-42.
[8]宋茂强.通信软件设计基础[M].北京：北京邮电大学出版社,2001：3-219.
[9]高翔.协议一致性测试研究及测控系统形式化协议设计技术[D].南京：东南大学.2007：8-30.
[10]李雁.基于TTCN-3的CTCS-3级车地通信协议一致性测试研究[D].北京：北京交通大学.2009：21-27.
[11]和诚凯IEEE802.11协议无线局域网固件(firmware)的研究与开发[D].西安：西安电子科技大学.2004：65-67.
[12]王宇凡.通信协议形式化描述和验证理论与方法的研究[D].安徽：中国科学技术大学.2005：35-37.
[13]王立荣.基于SDL的TDSCDMA确认传输模式的仿真测试的研究[D].北京：北京邮电大学.2007：57-59.
[14]林挺.蓝牙核心协议栈的研究[D].北京：北京交通大学.2006：37-42.
[15]陈德辉.形式化描述技术在嵌入式通信软件设计中的研究与应西[D].南京：南京邮电大学.2007：58-64.
[16]潘红艳.用于通信网络协议开发的形式化方法[J].计算机工程.2004,2：113-116.
[17]齐赛.SDL形式描述语言初探[J].通讯世界.2001,3：52-53.
[18]褚秉华,仇佩亮.电信协议工程与形式化方法[J].浙江大学学报(工学版).第37卷第1期.
[19]章韵,杨庚.基于SDL的通信协议系统设计方法.[J].计算机工程与应用.2001年第22期.
[20]蔡宇IEEE802.11b无线局域网媒体访问控制器研究与实现[D].北京：清华大学.2004：73-91.
[21]罗军舟,顾冠群.协议描述和验证的基本方法[J].南京：东南大学学报.1996年第5期.
[22]蒋国明.协议形式化模型及建模技术研究[D].浙江：浙江理工大学.2006年.
[23]王永刚.浅谈铁路通信信号一体化技术[J].科技资讯.2010年第7期.
[24]章志燮.基于构造类别代数的协议安全测试研究[D].安微：中国科技技术大学.2009年.
[25]Esposito Rosaria, Lazzaro Armando, Marmo Pietro, Sanseviero Angela. Formal Verification of ERTMS EURORADIO Safety Critical Protocol [J]. Ansaldo Segnalamento Ferroviario S.p.A.
[26]滕竹.基于EFSM的CBTC通信协议一致性测试的研究[D].北京交通大学.2008年.
[27]CENELEC:EN50159-2 Railway Application:Signaling and Communication-Safety-Related Communication in Open Transmission System.2001.
[28]Using:SUBSET-0372.2.0 EURORADIO FIS.2005
[29]Hans-Werner Renz. Open Communication Standards for safe and Secure Railway Control, Alcatel Telecommunications Review,2004..26
[30]Linn R Jetal. Protocol Specification, Testing, and Verification. Amsterdam:North-Holland,1992
[31]Rudin H. Protocol engineering:a Critical assessment. In:Aggarwal Sed. Protocol Specification, Testing, and Verification. Amsterdam:North-Holland,1988
[32]Helovuo, J:Leppanen, Application of Concurrency to System Design,2001, Proceedings.2001, International Conference on.2001.
[33]许明伟.协议性能测试理论与应用研究[D].北京：清华大学.1998年.
[34]Lee D, Netravali A N, Sabnani K K, etal. Passive testing and applications to network management. J. Procedings of IEEE International Conference on Network Protocols,1977.
[35]李晓梅.基于UML模型的SIP即时通信系统的研究与设计[D].北京：北京邮电大学.2009年.
[36]陈伟玲.协议安全测试理论和方法的研究[D].安徽：中国科学技术大学.2008年.
[37]Ana Cavalli, Dario Vieira. An Enhanced Passive Testing Approach for Network. J. Protocols. Procedings of IEEE International Conference on Network Protocols,2006.
[38]古天龙,蔡国永.网络协议的形式化分析与设计[M].北京：电子工业出版社.2003年11月
[39]Jan Ellsbeger, Dieter Hogrefe, Amardeo Sarma. SDL Formal Objest-oriented Language for Communicating System, Prentice-Hall.1997.
[40]ITU-T Z.100. Specification and Description Language(SDL).1999.
[41]Gregory White, Eric Fisch, and Udo Pooch. Computer System and Network Security, CRC press. 1996.
[42]Telelogic TAU Help file.
[43]彭磊.面向服务的WSN体系结构、RD方法与应用研究[D].成都：电子科技大学.2009.
[2]李开成,卜长堃,毛俊杰,傅世善等.国外铁路通信信号新技术纵览[M].北京：中国铁道出版社.2005,8：4-7.
[3]唐涛,郜春海ETCS系统分析及CTCS的研究[J].湖南：机车电传动,2004,6：49-53.
[4]季学胜,唐涛CTCS-3级列车运行控制系统综合测试平台研究[J].北京：铁道通信信号,2007,43(7)：1-3.
[5]成登高.中国列车运行控制系统(CTCS)技术简介[J].山西：科技情报开发与经济.2007,17(32)：275-276.
[6]单振宇CTCS-3级车地通信协议设计与验证[D].北京.北京交通大学.2009：3-37.
[7]刘雨CBTC系统通信协议的设计和形式化分析[D].北京：北京交通大学.2007：3-42.
[8]宋茂强.通信软件设计基础[M].北京：北京邮电大学出版社,2001：3-219.
[9]高翔.协议一致性测试研究及测控系统形式化协议设计技术[D].南京：东南大学.2007：8-30.
[10]李雁.基于TTCN-3的CTCS-3级车地通信协议一致性测试研究[D].北京：北京交通大学.2009：21-27.
[11]和诚凯IEEE802.11协议无线局域网固件(firmware)的研究与开发[D].西安：西安电子科技大学.2004：65-67.
[12]王宇凡.通信协议形式化描述和验证理论与方法的研究[D].安徽：中国科学技术大学.2005：35-37.
[13]王立荣.基于SDL的TDSCDMA确认传输模式的仿真测试的研究[D].北京：北京邮电大学.2007：57-59.
[14]林挺.蓝牙核心协议栈的研究[D].北京：北京交通大学.2006：37-42.
[15]陈德辉.形式化描述技术在嵌入式通信软件设计中的研究与应西[D].南京：南京邮电大学.2007：58-64.
[16]潘红艳.用于通信网络协议开发的形式化方法[J].计算机工程.2004,2：113-116.
[17]齐赛.SDL形式描述语言初探[J].通讯世界.2001,3：52-53.
[18]褚秉华,仇佩亮.电信协议工程与形式化方法[J].浙江大学学报(工学版).第37卷第1期.
[19]章韵,杨庚.基于SDL的通信协议系统设计方法.[J].计算机工程与应用.2001年第22期.
[20]蔡宇IEEE802.11b无线局域网媒体访问控制器研究与实现[D].北京：清华大学.2004：73-91.
[21]罗军舟,顾冠群.协议描述和验证的基本方法[J].南京：东南大学学报.1996年第5期.
[22]蒋国明.协议形式化模型及建模技术研究[D].浙江：浙江理工大学.2006年.
[23]王永刚.浅谈铁路通信信号一体化技术[J].科技资讯.2010年第7期.
[24]章志燮.基于构造类别代数的协议安全测试研究[D].安微：中国科技技术大学.2009年.
[25]Esposito Rosaria, Lazzaro Armando, Marmo Pietro, Sanseviero Angela. Formal Verification of ERTMS EURORADIO Safety Critical Protocol [J]. Ansaldo Segnalamento Ferroviario S.p.A.
[26]滕竹.基于EFSM的CBTC通信协议一致性测试的研究[D].北京交通大学.2008年.
[27]CENELEC:EN50159-2 Railway Application:Signaling and Communication-Safety-Related Communication in Open Transmission System.2001.
[28]Using:SUBSET-0372.2.0 EURORADIO FIS.2005
[29]Hans-Werner Renz. Open Communication Standards for safe and Secure Railway Control, Alcatel Telecommunications Review,2004..26
[30]Linn R Jetal. Protocol Specification, Testing, and Verification. Amsterdam:North-Holland,1992
[31]Rudin H. Protocol engineering:a Critical assessment. In:Aggarwal Sed. Protocol Specification, Testing, and Verification. Amsterdam:North-Holland,1988
[32]Helovuo, J:Leppanen, Application of Concurrency to System Design,2001, Proceedings.2001, International Conference on.2001.
[33]许明伟.协议性能测试理论与应用研究[D].北京：清华大学.1998年.
[34]Lee D, Netravali A N, Sabnani K K, etal. Passive testing and applications to network management. J. Procedings of IEEE International Conference on Network Protocols,1977.
[35]李晓梅.基于UML模型的SIP即时通信系统的研究与设计[D].北京：北京邮电大学.2009年.
[36]陈伟玲.协议安全测试理论和方法的研究[D].安徽：中国科学技术大学.2008年.
[37]Ana Cavalli, Dario Vieira. An Enhanced Passive Testing Approach for Network. J. Protocols. Procedings of IEEE International Conference on Network Protocols,2006.
[38]古天龙,蔡国永.网络协议的形式化分析与设计[M].北京：电子工业出版社.2003年11月
[39]Jan Ellsbeger, Dieter Hogrefe, Amardeo Sarma. SDL Formal Objest-oriented Language for Communicating System, Prentice-Hall.1997.
[40]ITU-T Z.100. Specification and Description Language(SDL).1999.
[41]Gregory White, Eric Fisch, and Udo Pooch. Computer System and Network Security, CRC press. 1996.
[42]Telelogic TAU Help file.
[43]彭磊.面向服务的WSN体系结构、RD方法与应用研究[D].成都：电子科技大学.2009.