探析基于uppaal的rbc系统控车流程建模分析

《探析基于uppaal的rbc系统控车流程建模分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京交通大学硕士学位论文基于UPPAAL的RBC系统控车流程建模分析姓名：谭耿申请学位级别：硕士专业：交通信息工程及控制指导教师：邱宽民20080601中文摘要摘要：RBC系统是中国铁路CTCS一3级列控系统中的重要组成部分，UPPAAL是基于时间自动机理论的实时系统建模分析验证工具，使用UPPAAL分析RBC系统控车流程，可以验证流程的特性，对于保证RBC系统控车流程的安全性有着重要的实际意义。论文完成的主要工作如下：1．介绍了时间自动机理论及其模型检验工具UPPAAL的使用方法。2．通过分析列车在RBC系统控制下的运行过程，把RBC系统控车流程分为五部分：列车登录流程，正常

2、控车流程，RBC交接流程，列车注销流程和消息重发流程。3．基于时间自动机理论对RBC系统控车的五个流程以及其他外部设备分别进行了建模：根据研究对象的特点，在合理的抽象和假设之后，确定了各个模型的状态，状态跳转路径和状态跳转的约束条件，得到了RBC系统控车流程的时间自动机模型。4．使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证：通过设置通道和全局变量，构造了时间自动机的积；使用模拟器，模拟了RBC控制列车运行过程，分析RBC控制列车运行过程中的状态变化；使用验证器，通过快速搜索整个系统的状态空间，验证RBC系统控车流程的活性和J下确性等各项特性。关键词：CTC

3、S．3列控系统；RBC；时间自动机；UPPAAL；建模分析分类号：U284．44ABSTRACTABSTRACT：RBCsystemisanimportantcomponentofChineseTrainControlSystemLecel3(CTCS-3)．UPPAALisamodeling,analyzingandverifyingtoolforreal—timesystembasedonTimedAutomataTheory．ItispossibletoverifysomepropertiesofRBCsystemtrain-controlprocessofRBCbyus

4、ingUPPAAL，anditissignificantforguaranteeingthesafetyoftrain-controlprocess．Themajorworksofthisthesisaresummarizedasfollowing：1．ThisthesisintroducesTimedAutomataTheoryandthemethodofusingthismodel．testtoolUPPAAL．2．Byanalyzingtraineontrolprocess，thereale5partsoftrain—controlprocess：trainloginpr

5、ocess，normalcontrolprocess，RBChandoverprocess，trainlogoutprocessandmessagereserldprocess．Basedonthese5processes，RBCcancontrolatrain．3．Themodelsofthese5processesandotherexternalequipmentbasedonTimedAutomataTheoryareestablished．Afterreasonableabstractandassumption，thestatesofeachprocess，states

6、transitionpathandconstraintsaredeterminedbasedOnTimedAutomataTheory,SOastoobtainthetimedautomatamodelofthe5process．4．UPPAALisusedtoanalyseandverifythese5timedautomatamodels．Bysettingchannelandglobalvariables，theproductoftimedautomataisobtained．ByusingSimulator,theprocessofRBCcontroltrainissi

7、mulated，andanalyzingthestatetransitionofRBCtraincontrolprocessisanalyzed．ByusingVerifier，viaquicklysearchingthewholestatespaceofRBCsystem，activity,validityandohterpropertiesofRBCtraincontrolprocessareverified．KEYWORDS：CTCS-3TrainControlSystem；RBC；T