详情

原文传递基于CPN的CBTC系统区域控制器建模与验证

论文题名：	基于CPN的CBTC系统区域控制器建模与验证
关键词：	列车运行控制系统;区域控制器;UML扩展机制;有色Petri网;安全分析
摘要：	随着通信技术、计算机技术和控制技术的迅速发展，城市轨道交通信息的传输方式已由有线传输转变为无线通信，基于通信的列车运行控制系统(CommunicationBasedTrainControl,CBTC)逐渐成为我国城市轨道交通的重要组成部分。区域控制器(ZoneController,ZC)通过与CBTC系统的其他子系统频繁进行信息交互来为列车生成移动授权(MovementAuthorization,MA)，是CBTC系统不可或缺的安全控制设备。分析区域控制器的结构和功能，构建满足ZC移交安全性和实时性的模型，有利于列车在线路上安全、高效的运行。论文在原有建模方法的基础上采用统一建模语言(UnifiedModelingLanguage,UML)和层次时间有色Petri网(HierarchicalTimedColoredPetriNet,HTCPN)相结合的方法对ZC移交场景下CBTC子系统之间的信息交互过程进行建模与验证，并根据得到的模型对ZC移交场景进行安全分析，具体研究工作如下：　　(1)根据中国城市轨道交通协会制定的《城市轨道交通CBTC信号系统行业技术规范—产品规范》分析CBTC系统的基本构成和工作原理，借助流程图重点分析区域控制器的移交过程和移交场景下移动授权的生成，并根据两个功能的需求构建UML用例图、顺序图、状态图和活动图。　　(2)利用UML的扩展机制将构建的活动图节点扩展为可执行中间模型节点，结合XML技术将可执行中间模型转换为层次时间有色Petri网模型。再借助Petri网的仿真验证工具CPNTools中的状态空间报告和ASK-CTL公式对转换后的HTCPN模型进行验证。验证结果表明：HTCPN模型的系统属性和动态属性正常，符合ZC移交场景的功能需求。　　(3)利用UML扩展机制对ZC状态转移图和列车状态转移图的节点进行标记扩展并根据转换规则生成PHAVer模型。采用故障整合算法将PHAVer模型和故障模型整合为包含故障的PHAVer模型。利用前向可达集计算原理和故障监视器模型对包含故障的PHAVer模型进行仿真计算，找出危及系统安全的故障事件割集，并根据相关故障组合对ZC移交场景进行安全分析。　　(4)利用全路径覆盖优化算法(AllPathsCoveredOptimizationAlgorithm,APCO)对HTCPN模型生成的状态空间可达图进行路径搜索，并借助XML技术将搜索结果转换为测试案例框架。参考《TCMAET04012.1-2018城市轨道交通基于通信的列车运行控制系统互联互通测试规范》和重庆十号线线路情况，选取故障事件作为测试案例对象并在CBTC通用测试平台上进行测试。测试结果表明，经过全路径覆盖优化算法搜索得到的故障测试案例符合城市轨道交通测试规范要求和ZC移交场景功能需求。　　通过模型仿真和案例测试的结果可知，采用UML和HTCPN相结合的方法建立的模型既能保证在数学上具有严谨性，又能清晰描述整个ZC移交和移动授权生成的过程，通过HTCPN模型状态空间可达图计算得到的测试案例也符合测试规范要求，证明了该集成建模方法的切实性，为CBTC系统其它功能或场景的建模和测试提供了参考。
作者：	孙维正
专业：	交通运输工程
导师：	旷文珍;朱明
授予学位：	硕士
授予学位单位：	兰州交通大学
学位年度：	2022