4检索范围中国知网百度webofscience(SCIE)IEEESpringerLINK安全关键系统通信协议调研报告(2015.4.12)1调研题目安全关键系统通信协议的建模与分析2任务说明1)查阅国外的相关文献；2)补充通信协议中的具体网络3)阅读标准EN50159；3关键字检索词：CBTC；安全关键系统；安全通信协议；EN50159；safetycommunicationprotocol检索策略：无线*通信；总线*通信；以太网*通信；CBTC*communicationprotocol；safety*protocolverification/test/model/simulation/design/analysis*(safety)communicationprotocol;http://www.cnki.net/http://www.baidu.com/http://apps.webofknowledge.com/http://ieeexplore.ieee.org/Xplore/home.jsphttp://link.springer.com/ELSEVIERScienceDirect(SDOL)http://www.sciencedirect.com/在不同关键词组合下，检索范围内，近三年的文献总数5主要的检索文献[1]BSEN50159Railwayapplications—Communication,signalingandprocessingsystems-Safety-relatedcommunicationintransmissionsystems[S].[2]安全通信与安全通信标准EN50159J].铁路通信信号工程技术，2014.-1-【年份】2009【摘要】Verificationandconformancetestingforprotocolspecification,thekeypartoftheprotocoldevelopmentprocess,arecomplementarytechnologiesemployedtoincreaseconfidencethatasystemwillfunctionasstatedinitsspecifications.Inthispaper,weverifythesafetyandlivenessoftheprotocolspecifiedfortheLabeledTransitionSystem（LTS）byusingmodel-checkingmethodandimplementingthetestingtool,whichexperimentallydemonstratesthepresenceofdeadlockandreachabilityfromtheinitialstatetoarandomstate.Implementingthetestingtoolcanusemodalmu-calculustoassesswhetherprotocolmodelproperties,presentedbymodallogic,meetprotocolspecifications.Inaddition,weproposeaconformancetestingtooltocheckcorrectimplementationofsequencesthathavebeenderivedbytheUIOmethodfromthespecificationoftheprotocolbeingverified.ThisgeneratingtoolusestheC++languageintheMicrosoftWindowsNTenvironment.【篇名】Compositionalverificationofacommunicationprotocolforaremotelyoperatedaircraft【作者】AlwynE.Goodloe,CesarA.Munoz【期刊类型】ScienceofComputerProgramming【年份】2013【摘要】Thispaperpresentstheformalspecificationandverificationofacommunicationprotocolbetweenagroundstationandaremotelyoperatedaircraft.Theprotocolcanbeseenastheverticalcompositionofprotocollayers,whereeachlayerperformsinputandoutputmessageprocessing,andthehorizontalcompositionofdifferentprocessesconcurrentlyinhabitingthesamelayer,whereeachprocessshouldsatisfyadistinctdeliveryrequirement.Acompositionaltechniqueisusedtoformallyprovethattheprotocolsatisfiestheserequirements.Althoughtheprotocolitselfisnotnovel,themethodologyemployedinitsverificationextendsexistingtechniquesbyautomatingthetediousandusuallycumbersomepartoftheproof,therebymakingtheiterativedesignprocessofprotocolsfeasible.【篇名】基于工业以太网的列车通信网络研究【作者】张建斌【学位类型】硕士【授予单位】北京交通大学【导师】谭南林【年份】2011【摘要】:传统以太网通信的非实时和非确定性限制了其在列车通信网络中应用。改变以太网通信驱动和调度机制可使之成为适合列车通信的实时以太网。本文深入研究了影响以太网实时性和确定性通信的因素后提出了解决方案,并在设计的实验平台上进行了验证。本文以星型网络为基础研究了共享式和交换式以太网的实时特性,得出交换式以太网符合列车通信网络组网要求。分析了时间触发架构的通信机制并引入以太网中,分时复用的通信方法保证了以太网的通信的实时性和确定性,在此基础上提出以太网确定性通信的调度机制,并分析计算了通信网络的宏观调度周期。为了建立基于时间触发机制的以太网通信网络,本文在IEEEI588时钟同步协议基础上...
