cbtc系统通信协议设计和形式化的分析

《cbtc系统通信协议设计和形式化的分析》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、中文摘要摘要：在基于通信的列车运行控制(Communications-basedTrainConU'ol,CBrI℃)系统中，各子系统问可靠的数据通信是保证整个系统安全的基础。为了达到数据传输安全的目的，论文设计实现了一个相对完备的通信协议供自主开发的CBTC系统使用，并且引入形式化方法对其进行分析，证明了该协议的安全性。论文阐述了CBTC系统通信协议的设计原理。首先根据自主开发的CBTC系统在数据传输安全方面的需要，详细分析了通信协议的安全需求及性能指标；然后引入了安全传输规范，利用规范中提供的安全防护措施分层次地设计了CBl

2、fC系统通信协议。论文选择形式化语言CPN(ColouredPetdNet)和它的支持工具CPNTools对CBTC系统通信协议进行“自上而下”的建模。首先给出了CBTC系统通信协议的顶层模型；而后深入研究了单链路协议模型的建立过程，从基本模型着手，逐步加入安全防护机制，最后得到完善的协议模型。基于所建模型，使用CPNTools对CBTC系统通信协议进行验证和性能分析。根据安全通信协议的分析方法，首先对模型进行必要的分解和简化，通过状态空间分析验证模型的有界性、活性等动态特性；而后考虑影响系统安全的各种危险因素，对通信协议的性能

3、进行分析，并得出各种性能参数的均值；最后将这些性能参数的均值和既定的性能指标进行比较，证明所设计的通信协议是符合我们的CBTC系统安全传输需求的。关键词：CBTC通信协议；安全传输规范；着色Petri网；建模；性能分析；分类号：U49ABSTRACTABSTRACIr：InmeCommtmieatiom-bas簋lTrainControl(CB'rC)system,thereliabledataeommtmicationbetweeneverysub-syst舶isthefoundationofthewholesystem’ss

4、afety．InordertotransferinformationsafdKaself-containedcommunicationprotocolofCBTCsystemwasdesignedandimplementedinthispaper,andformalizationmethodWaSbroughtintoanalyzetheprotocolinordl薯toproveit’ssafhyperformance．Inthepaper,thedesignprinciplesofthecommunicationprotoc

5、oloftheCBTCsystemw雠expatiated．Firstly,safetyrequirementsandcapabilitytarg哟oftlaeprotocolwcirl。analyzedaccordingtothedemandsoftheCBTCsystemattheasl僦tofsafeinformationmmsferring；thenthesafetyrelatede．ommunieadonstandardwasintroduced．andtheprotocoloftheCBTCsystemⅥ∞desig

6、nedhierarchicallyusingtlacsafetydefeneesprovidedinthestandard．Inthepaper,formalizationlanguageCPN．andCPNToolswc陀chosentobuildthemodelsoftheprotocolfromtoptobottom．Firstly,thetopmodeloftheprotocoloftheCBTCsystanWaSbuilt；岫themodelingprocessofsinglelinkprotocolWaSseriou

7、slystudied．Startingwiththebasalmodel，theconsummatemodeloftheprotocolWaSobtainedbyaddingeachsafetydefencestepbystcp．TheprotocoloftheCBTCsystem1,ttllSvalidatedandanalyzedbasedOnthebuiltmodelsbyCPNTools．AccordingtOtheanalysismethodsofsafetycommunicationprotocol，thebuilt

8、modelswereessentiallybrokeadownandpredigestedfirstly,thedynmiecharacteristicsofthemodelsWCI'evalidatedbyusingthestatesspacesanalysi