基于csp的城轨cbtc联锁逻辑形式化建模与验证

《基于csp的城轨cbtc联锁逻辑形式化建模与验证》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、ABSTRACTABSTRACT：Withthedevelopmentofcommunicationtechnology，computertechnologyandautomaticcontroltechnology，communicationbasedtraincontroltechnologyhasgraduallybecomethepreferredsolutionforurbantransportationsystem．AsapartoftheCBTCsystem，theinterlockingsystemeffectsonthesafetyandspeedofmetrain，a

2、chievesmanyfunctionsuchasroutecontrol，signalcontrol，intervaltemporaryspeedlimitation，platformhold，trainhold，ESAandSOon．Interlockingcontrollogicisthecoreoftheinterlockingsoftware，itscorrectnessisimportantnotonlyforthedevelopmentbutalsofinalverification．ofinterlockingsoftware．Thisthesisstartsfromco

3、mputerbasedinterlocking，firstlyanalysesandsummarisethefunctionalrequirementsandsecurityrequirementsofCBTCinterlockingsystem．ThedescriptionoftheinterlockinglogicnowalmostrelyingonnaturallanguagewhichisnotuptostandardaIldambiguous．thustheformalmethodwithawell．definedmathematicalfoundationandinferen

4、ceruleshavearousedtheattentionoftheresearchersoftherailtrafficcontrolsystem．Basedonthestudyandcomparisonofthesemethods，thispaperproposesamethodbasedoncommunicatingsequentialprocessestodescribetheurbanrailCBTCinterlockinglogic．Theinterlockingtableistheembodimentoftheinterlocklogicwhichrepresentsth

5、erelationshipbetweenrailwaysignalequipment．Thus，thispaperdescribestheinterlockingrelationshipinthetablewithCSP，treatstheestablishmentoftrainrouteasaconcurrentandinteractiveprocesscomposedoffivesub-processrespectivelyareswitch，signal，user,interlockingsoftwareandsection．SOⅡ1etheentireinterlockingta

6、bleistheparallelcompositionoftheseroutes．Then，usingProBtoverifythefunctionalityandsecurityofthemodelbyanimation，modelchecking，consistencyverification，thusverifythecorrectnessofinterlockinglogicrepresentedinthetable．Finally，thearticleappliesthismethodtomodelingandverificationoninterlockingtableofT

7、ongjisouthStationofBeijingYizhuangsubwaylinetoprovethefeasibilityandcorrectnessofthemethod．KEYWORDS：CBTC；Interlocking；FormalMethod；CSP；LTL；ProBCLASSNo：IJ284．3目录中文摘要⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯．iiiABSTRACT⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯