学位论文 > 优秀研究生学位论文题录展示

基于时间自动机的RBC控车流程研究

作　者: 童超
导　师: 杨扬
学　校: 西南交通大学
专　业: 交通信息工程及控制
关键词: 铁路信号 RBC 形式化语言 时间自动机 UPPAAL 建模
分类号: U284.48
类　型: 硕士论文
年　份: 2009年
下　载: 111次
引　用: 3次
阅　读: 论文下载
 

内容摘要


本论文研究的CTCS-3级列控RBC(Radio Block Center)地面子系统是铁路信号列车控制中一个基于无线通信的实时控车系统,其控车功能是CTCS-3级列控系统功能的核心组成部分。研究的主要内容是基于时间自动机理论,在UPPAAL这种目前最先进的实时系统建模分析验证工具中,对RBC系统进行分析,建模,验证。论文最终对RBC系统控车流程的特性进行了验证,对于保证RBC系统控车流程的安全性、减少系统开发周期及开发成本都有着重要的实际意义。论文完成的主要内容包括绪论、形式化语言及时间自动机理论介绍、RBC系统功能需求分析、RBC系统时间自动机模型建立、在UPPAAL中对RBC系统功能特性的验证:第一章.概述了列车控制系统在国内外的发展与现状,提出了RBC系统形式化建模的目的和意义。第二章.介绍了形式化语言建模的优缺点及阐明了选择时间自动机对RBC系统建模的原因。第三章.通过详细分析RBC系统控车的功能需求,单独建立消息重发流程,根据列车运行要求把RBC控车分为四个流程:列车登录流程,正常控车流程,RBC交接流程,列车注销流程。第四章.介绍了基于时间自动机理论模型检验工具UPPAAL的使用方法。对RBC系统的五个流程以及其他外部设备分别在UPPAAL中建立了时间自动机模型。第五章.通过设置通道和全局变量,构造了时间自动机的积,使用UPPAAL对RBC系统控车流程的时间自动机模型进行了分析验证;使用模拟器,模拟了RBC控制列车运行过程,分析RBC控制列车运行过程中的状态变化;使用验证器,通过快速搜索整个系统的状态空间,验证RBC系统控车流程的活性和正确性等各项特性。

全文目录


摘要  6-7
Abstract  7-11
第1章 绪论  11-16
  1.1 研究背景  11-13
    1.1.1 欧洲列车控制系统现状  11-12
    1.1.2 中国列车控制系统现状  12-13
  1.2 CTCS-3级RBC控车系统建模的目的和意义  13-14
  1.3 论文的主要工作和章节安排  14-16
第2章 形式化描述方法  16-27
  2.1 形式化方法  16-19
    2.1.1 形式化方法概述  16-17
    2.1.2 形式化方法选择  17-18
    2.1.3 形式化模型验证  18
    2.1.4 形式化建模优点  18-19
  2.2 时间自动机  19-27
    2.2.1 自动机概述  19-20
    2.2.2 时间自动机  20-23
    2.2.3 时间自动机简例  23-24
    2.2.4 时间自动机可达性分析  24-25
    2.2.5 时间自动机优点  25-27
第3章 RBC控车流程分析与设计  27-45
  3.1 CTCS-3级列控RBC系统介绍  27-31
    3.1.1 CTCS-3级列控系统  27-28
    3.1.2 地面RBC子系统  28-31
  3.2 RBC子系统功能需求分析  31-33
  3.3 RBC系统控车流程分析与设计  33-45
    3.3.1 消息重新发送流程  35-37
    3.3.2 列车登陆流程  37-38
    3.3.3 正常控车流程  38-40
    3.3.4 RBC移交流程  40-43
    3.3.5 列车注销流程  43-45
第4章 基于UPPAAL的RBC控车流程建模  45-64
  4.1 时间自动机建模工具UPPAALL介绍  45-50
    4.1.1 UPPAAL结构简介  46-47
    4.1.2 UPPAAL理论模型  47-50
  4.2 RBC控车流程建模  50-60
    4.2.1 消息重发模型  50-52
    4.2.2 列车登陆模型  52-54
    4.2.3 正常控车模型  54-56
    4.2.4 RBC移交模型  56-59
    4.2.5 列车注销模型  59-60
  4.3 其他子系统简单建模  60-64
    4.3.1 车载模块简单模型  60-62
    4.3.2 地面其他模块简单模型  62-64
第5章 RBC控车模型功能验证  64-75
  5.1 在UPPAAL中构造时间自动机的积  64-65
  5.2 消息重发流程系统模型验证  65-68
    5.2.1 模型仿真  65-66
    5.2.2 模型仿真结果验证  66-68
  5.3 RBC控车系统流程模型验证  68-75
    5.3.1 模型仿真  68-72
    5.3.2 模型仿真结果验证  72-75
结论  75-76
致谢  76-77
参考文献  77-80
攻读硕士学期间发表的学术论文及科学实践  80

相似论文

  1. 基于SVM的常压塔石脑油干点软测量建模研究,TE622.1
  2. 非正交面齿轮齿面建模及加工误差分析,TH132.41
  3. 混凝土高拱坝三维非线性有限元坝肩稳定分析研究,TV642.4
  4. HID灯整流效应的研究,TM923.32
  5. 面向SMDA的服务建模方法及工具实现,TP311.52
  6. 导弹虚拟试验可视化技术研究,TP391.9
  7. 飞行模拟中飞行管理计算机系统CDU组件设计与仿真,TP391.9
  8. 基于测量的Internet链路延迟建模,TP393.4
  9. 基于测量的Internet延迟分析与建模,TP393.4
  10. 空中目标抗干扰识别跟踪系统,TN215
  11. 军队后勤物资管理系统设计与实现,TP311.52
  12. 内衣人台的雏形设计,TS941.2
  13. 拖拉机电控液压动力转向系统的转向机构及液压系统设计,S219.02
  14. 数学建模在高中数学教学中的实践与探索,G633.6
  15. 面向RIA开发模型的研究,TP311.5
  16. 虚拟手术中建模与仿真关键技术研究,TP391.41
  17. 基于模型的小麦根系可视化研究,S512.1
  18. 近红外光谱分析技术在尖椒叶片生长信息获取中的应用,S641.3
  19. 高丛蓝莓组培体系及种子萌发率的建模研究,S663.9
  20. 板球系统的控制算法研究,TP13
  21. 环流MBR处理头孢菌素中间体废水的运行效果及影响因素,X787

中图分类: > 交通运输 > 铁路运输 > 铁路通信、信号 > 铁路信号 > 区间闭塞与机车信号系统 > 列车运行自动化
© 2012 www.xueweilunwen.com