探索cbtc中轨旁安全计算机的设计与形式化验证

《探索cbtc中轨旁安全计算机的设计与形式化验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京交通大学硕士学位论文CBTC中轨旁安全计算机的设计与形式化验证姓名：袁彬彬申请学位级别：硕士专业：交通信息工程及控制指导教师：唐涛20080501中文摘要摘要：随着计算机越来越多的应用于安全苛求系统中，计算机能否长期安全、可靠、稳定的运行成为人们关注的中心，这促使着越来越多的人开始研究和设计安全计算机。而系统的安全性必须在设计阶段充分考虑，以免由于设计的缺陷导致整个系统存在安全隐患。所以在系统的设计过程中，根据安全苛求系统的“v"型的开发框架，采用形式化的方法对系统的安全性进行建模分析，验证系统设计的正确性和完备性是必要的。论文以基于通信的列车控

2、制(CBTC)系统中ZC应用和DSU应用作为应用背景，以CBTC系统中ZC应用和DSU应用所使用的安全计算机平台为例。详细分析了安全计算机平台需求，在此基础上确定了系统结构，然后设计其硬件结构和软件的调度策略。论文引入有色Petri网，根据安全性设计思想，在系统的设计阶段对安全计算机平台进行形式化建模。首先介绍了有色Petri网的形式化层次化建模的方法，然后根据系统结构，采用“自上而下"的层次建模方法对系统建立的顶层模型和各级子模型，子模型包括“主”“备”通道模型、通道内单机模型、容错和安全管理单元(FTSM)模型和通信控制器模型。在所建模型的基础上

3、，研究了CPN的状态空间分析和仿真性能分析两种方法在模型分析的应用。利用状态空间分析验证了容错和安全管理单元(FTSM)模块的有界性、活性等动态行为属性和逻辑功能的正确性；利用仿真分析完成了系统同步过程的性能分析，得出系统同步的时间参数，对系统调度时间的选取具有指导意义。通过对安全计算机进行建模和分析，可以验证对我们系统设计是否合理，对系统设计的完善提供参考和指导。关键词：安全计算机；有色Petri网(CPN)；建模与分析；分类号：TP309．1ABSTRACTABS’l’RAC’l’：Withcomputerswidelyapplyinginthe

4、safety-criticalsystems，whethercomputerscatlsafety,reliable，steadyrunningbecamethefocusofpeople．Thissituationurgesmoreandmorepeoplestarttostudyanddesignsafetycomputer．Thesafetyofasystemmustbefullyconcerned，forfearthedisfigurementofdesignwillberesultinthehiddensafetytroubleexisti

5、nginthesystem．Accordingtothesafetycriticalsystemdevelopmentframework，applyingtheformalmethodtobuildthesystemmodelanalyzethesafetyofthesystemandvalidatethedesignofthesystemisnecessary．ZCandDSUofCBTCsystemarethebackgroundsofthispaper,illustratingthesafetycomputersusedinZCandDSU．F

6、irstlyweanalyzedtherequirementsofsafetycomputerindetails．Onthebase，weconfirmedthestructureofsafetycomputerandthendesignedthehardwareandsoftwareschedulingstrategy．TheColoredPetriNets(CPN)wasbroughtintobuildthemodelofsafetycomputerplatformbasingonsafetydesignideainthedesignphase．

7、Themodelingmethodwasintroducedfirstly,andthenthehierarchicalmodelsofthesafetycomputerwerebuiltbasedonthestructuredesign．Themodelcontainsthetopmodelandsonmodelswhicharecomprisedofmodelof‘host’and‘standby’channel，modelofsinglemachine，modelofFTSM，modelofcommunicatecontroller,etc．O

8、nthebasisofthemodels，thestatespaceanalysisandsimulatio