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

基于时间自动机模型的CBTC系统安全计算机平台的形式化验证

作　者: 郭志良
导　师: 郜春海
学　校: 北京交通大学
专　业: 交通信息工程及控制
关键词: 实时系统 安全计算机 时间自动机 模型验证 UPPAAL
分类号: U284.48
类　型: 硕士论文
年　份: 2010年
下　载: 87次
引　用: 1次
阅　读: 论文下载
 

内容摘要


众多工业控制领域要求其计算机控制系统具有高可靠、高可用和高安全的运行基础。安全计算机系统常用于军事、航空航天、工业控制、银行、通信等安全苛求(safety-critical)领域,以避免由于计算机的失效造成重大事故。基于通信的列车运行控制(Communications-Based Train Control, CBTC)系统是当今世界列车运行控制系统的发展趋势,各主要发达国家都相继开发出自己的CBTC系统。在CBTC系统中,地面区域控制中心的主要组成部分是区域控制器ZC以及数据存储单元DSU,其中ZC管辖区域中所有列车的车载控制器VOBC将列车所在位置和速度等信息发到安全计算机平台之上的ZC应用程序中,经过保证安全的计算后再将移动授权MA发往VOBC控制列车的下一步运行,而DSU子系统包括了其它列车控制子系统使用的所有数据库和配置文件,它的应用软件也需要搭建在安全计算机平台之上。二乘二取二冗余结构的安全计算机平台是提高系统安全性、可靠性的一种重要解决方式。CBTC列控系统的安全计算机平台采用二乘二取二冗余结构,它是一个实时系统,控制过程需要考虑时间因素。本文分析CBTC系统安全计算机平台系统的组成结构,提取出系统的功能约束,采用基于时间自动机理论的建模验证工具UPPAAL建立系统的自动机网络模型,进行仿真分析,验证系统的功能性、实时性、安全性要求。

全文目录


致谢  5-6
中文摘要  6-7
ABSTRACT  7-10
1 引言  10-16
  1.1 研究背景和对象  10-14
    1.1.1 安全计算机国内外研究现状  10-11
    1.1.2 CBTC系统安全计算机平台  11-13
    1.1.3 形式化方法的引入  13-14
  1.2 研究内容  14
  1.3 本文的组织结构  14-16
2 时间自动机及其验证工具UPPAAL  16-21
  2.1 时间自动机理论  16-18
    2.1.1 时间自动机定义  16-17
    2.1.2 时间自动机网络  17-18
  2.2 时间自动机理论的研究进展  18
  2.3 自动验证工具UPPAAL  18-21
    2.3.1 UPPAAL的构成与特点  18-19
    2.3.2 UPPAAL需求规范语言  19-21
3 安全计算机平台系统的结构与功能分析  21-37
  3.1 系统结构  21-22
  3.2 各组成模块的功能  22
  3.3 二取二功能的实现  22-31
    3.3.1 二取二的系统结构  22-23
    3.3.2 二取二通道的工作模式  23-24
    3.3.3 二取二的主要功能  24-31
      3.3.3.1 数据比较的实现  24-27
      3.3.3.2 任务同步的实现  27-30
      3.3.3.3 对二取二通道的安全控制  30-31
  3.4 二乘功能的实现  31-37
    3.4.1 两个通道的输入一致性控制  31
    3.4.2 对主通道的状态跟随  31-33
    3.4.3 备通道处于跟随状态的保证  33-35
    3.4.4 主备通道之间的切换  35-37
4 基于时间自动机的系统建模  37-46
  4.1 系统功能分析  37-39
    4.1.1 二取二通道间工作模式的切换  37-38
    4.1.2 二取二双机的同步  38-39
  4.2 系统的时间自动机网络模型  39-46
    4.2.1 处理单元PU自动机模型  39-41
    4.2.2 容错安全管理单元FTSM自动机模型  41-44
    4.2.3 自动机模型间的通道及变量  44-46
5 基于UPPAAL的仿真与验证  46-52
  5.1 系统仿真  46-47
  5.2 系统验证与分析  47-52
    5.2.1 系统功能属性的验证  48-49
    5.2.2 系统实时属性的验证  49-50
    5.2.3 系统安全属性的验证  50
    5.2.4 验证过程分析  50-52
6 总结与展望  52-54
  6.1 总结  52
  6.2 展望  52-54
参考文献  54-57
图索引  57-58
表索引  58-59
作者简历  59-61
学位论文数据集  61

相似论文

  1. 仿真系统模型验证方法和工具研究,TP391.9
  2. 基于ARM的嵌入式实时操作系统的设计与开发,TP316.2
  3. 多核系统中基于温度限制的节能调度算法研究,TP332
  4. 基于光纤通道的文件级数据共享系统的设计与实现,TP333
  5. 基于DSP的嵌入式星载相机控制器的研究,V445.8
  6. 多处理器单调速率任务调度算法研究,TP332
  7. 面向方面的实时系统建模及实现方法研究,TP316.2
  8. 草畜平衡和精准管理模型在肃南县绵羊生产中的应用研究,S826
  9. 基于计算机视觉的机车乘务员驾驶疲劳监测研究,TP274
  10. 基于UPPAAL的电子商务协议安全性分析,TP393.08
  11. 基于时间自动机的模型验证技术,TP301.1
  12. 实时嵌入式系统VxWorks安全机制的研究与实现,TP316.2
  13. 基于MDE的UML模型到形式化模型的转换方法研究,TP311.52
  14. 闪拍系统的设计与实现,TP311.52
  15. 多处理器全局FP调度算法的研究,TP332
  16. 分布式信息化平台中嵌入式实时中间件研究,TP368.1
  17. 嵌入式实时系统ARTs-OS的动态内存管理研究,TP333.1
  18. 柔性工作流过程模型的研究,TP311.52
  19. IF对实时软件设计图形模型的验证,TP311.52
  20. 基于PI演算的CRM系统的设计与实现,TP311.52

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