基于时间自动机的cbtc区域控制子系统形式化建模与验证

《基于时间自动机的cbtc区域控制子系统形式化建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、ｌＵ２８３．２：密级中图分类号：公开ＵＤＣ：本校编号：讀Ｗ交遺乂聲硕±学位论文拖文题目：基于时间自动机的ＣＢＴＣ区滅控制子系统飛式，化＃搖与３合证研究生姑名：帘欢欢学号：０２１２４４１学校指导教师姓名；副教捻；炼永刚职称申请学位等级：工学硕壬学位专业：交通信息工程及控制２０１５．６．１２论文答辩日期论文提交日期；；２０１５．６．８独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研究成ｉ果，除了文中特别加ｔ＾？标注和致谢

2、之处外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含获得兰州交通大学或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均己在论文中作了明确的说明并表示了谢意。、学位论文作者签名巧＾义签字日期；户｜至年＾月Ｉ日；学位论文版权使用授权书本学位论文作者完全了解兰州巧通大学有关保留、使用学位论文的规定。特授权兰州巧通大学可レッ将学位论文的全部或部分内容编入有关数据库进行检索，并采用影目Ｐ、缩印或扫描等复制手段保存、汇编Ｗ供查阅和借阅。同意学校向国家有关部口或机

3、构送交论文的复印件和磁盘。（保密的学位论文在解密后适用本授权说明）学位论文作者签名；：％Ａ导师签名心聲ｊ签字日期年＾月）＞日签字日期：２＾＾年６月／又日硕士学位论文基于时间自动机的CBTC区域控制子系统形式化建模与验证FormalModelingandVerificationofCBTCZoneControllerBasedonTimeAutomation作者姓名：贺欢欢学科、专业：交通信息工程及控制学号：0212441指导教师：陈永刚副教授完成日期：2015年4月12日兰州交通大学LanzhouJiaot

4、ongUniversity兰州交通大学硕士学位论文摘要随着城市化脚步的逐渐加快，CBTC(Communications-BasedTrainControl,基于通信的列车控制)系统已经成为当今世界城市轨道交通列控系统的发展趋势。ZC(ZoneController,区域控制器)作为CBTC系统的核心设备，是实现列车安全追踪的关键，其可靠性直接关系到列车是否能安全运行。为了及时并准确发现系统设计缺陷，在系统开发早期使用一种工具对系统进行描述和验证就显得尤为重要。形式化方法是以精确的数学语言分析和验证系统的技术和工具。本文采用形式化方

5、法对ZC进行建模和验证，目的在于保证ZC设计的正确性和安全性。首先，论文分析了当前主流的形式化方法，根据安全苛求系统的设计要求，提出了形式化方法时间自动机理论及其自动验证工具UPPAAL。其次，在对CBTC的基本结构和运行原理进行分析的基础上，对本文的重点ZC的工作原理进行深入的分析，提出了系统的功能和性能需求。由于ZC是一个复杂实时系统，可将其按照功能划分为四大模块：列车管理、移动授权、ZC切换以及ZC与CBTC其他子系统信息交互。然后分别对它们的流程进行了设计。根据列车在CBTC区域运行的流程设计，利用时间自动机分别对ZC的

6、功能进行建模，通过设置通道和共享变量实现几个时间自动机的通信，将其组成为一个完整的时间自动机网络模型。最后，利用UPPAAL对所建模型进行模拟得到消息序列图，分析了列车在CBTC区域运行过程中状态的变化以及各子系统间的通信。然后应用BNF语句提炼出系统的功能和性能需求，并成功地进行了验证。验证结果表明时间自动机的形式化方法对实时系统的分析和验证有一定的可行性，能够为CBTC的继续研究提供参考。关键词：城市轨道交通；CBTC；时间自动机；ZC论文类型：应用技术研究-I-基于时间自动机的CBTC区域控制子系统形式化建模与验证Abst

7、ractWiththegraduallyacceleratingpaceofurbanization,communicationbasedtraincontrol(CBTC)systemhasbecamethedevelopmenttrendofcityrailtransittraincontrolsysteminthepresentworld.AsthecoreequipmentofCBTCsystem,zonecontroller(ZC)isthekeytorealizethesafetraintracking,itsrel

8、iabilityisdirectlyrelatedtothesafetyoftrainoperation.Inordertodiscoversystemdesigndifficiencetimelyandaccurately,itisparticularlyim