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

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

1、北京交通大学硕士学位论文CBTC系统通信协议的设计和形式化分析姓名：刘雨申请学位级别：硕士专业：交通信息工程及控制指导教师：唐涛20071201中文摘要摘要：在基于通信的列车运行控制(Communications-basedTrainConU'ol,CBrI℃)系统中，各子系统问可靠的数据通信是保证整个系统安全的基础。为了达到数据传输安全的目的，论文设计实现了一个相对完备的通信协议供自主开发的CBTC系统使用，并且引入形式化方法对其进行分析，证明了该协议的安全性。论文阐述了CBTC系统通信协议的设计

2、原理。首先根据自主开发的CBTC系统在数据传输安全方面的需要，详细分析了通信协议的安全需求及性能指标；然后引入了安全传输规范，利用规范中提供的安全防护措施分层次地设计了CBlfC系统通信协议。论文选择形式化语言CPN(ColouredPetdNet)和它的支持工具CPNTools对CBTC系统通信协议进行“自上而下”的建模。首先给出了CBTC系统通信协议的顶层模型；而后深入研究了单链路协议模型的建立过程，从基本模型着手，逐步加入安全防护机制，最后得到完善的协议模型。基于所建模型，使用CPNTools

3、对CBTC系统通信协议进行验证和性能分析。根据安全通信协议的分析方法，首先对模型进行必要的分解和简化，通过状态空间分析验证模型的有界性、活性等动态特性；而后考虑影响系统安全的各种危险因素，对通信协议的性能进行分析，并得出各种性能参数的均值；最后将这些性能参数的均值和既定的性能指标进行比较，证明所设计的通信协议是符合我们的CBTC系统安全传输需求的。关键词：CBTC通信协议；安全传输规范；着色Petri网；建模；性能分析；分类号：U49ABSTRACTABSTRACIr：InmeCommtmieati

4、om-bas簋lTrainControl(CB'rC)system,thereliabledataeommtmicationbetweeneverysub-syst舶isthefoundationofthewholesystem’ssafety．InordertotransferinformationsafdKaself-containedcommunicationprotocolofCBTCsystemwasdesignedandimplementedinthispaper,andformaliz

5、ationmethodWaSbroughtintoanalyzetheprotocolinordl薯toproveit’ssafhyperformance．Inthepaper,thedesignprinciplesofthecommunicationprotocoloftheCBTCsystemw雠expatiated．Firstly,safetyrequirementsandcapabilitytarg哟oftlaeprotocolwcirl。analyzedaccordingtothedema

6、ndsoftheCBTCsystemattheasl僦tofsafeinformationmmsferring；thenthesafetyrelatede．ommunieadonstandardwasintroduced．andtheprotocoloftheCBTCsystemⅥ∞designedhierarchicallyusingtlacsafetydefeneesprovidedinthestandard．Inthepaper,formalizationlanguageCPN．andCPNT

7、oolswc陀chosentobuildthemodelsoftheprotocolfromtoptobottom．Firstly,thetopmodeloftheprotocoloftheCBTCsystanWaSbuilt；岫themodelingprocessofsinglelinkprotocolWaSseriouslystudied．Startingwiththebasalmodel，theconsummatemodeloftheprotocolWaSobtainedbyaddingeac

8、hsafetydefencestepbystcp．TheprotocoloftheCBTCsystem1,ttllSvalidatedandanalyzedbasedOnthebuiltmodelsbyCPNTools．AccordingtOtheanalysismethodsofsafetycommunicationprotocol，thebuiltmodelswereessentiallybrokeadownandpredigestedfirstly,thedyn