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