声明
1 绪论
1.1 论文研究背景及意义
1.2 论文国内外研究现状
1.3 论文主要研究内容及结构安排
2 CBTC系统移动授权功能及时间自动机理论
2.1 CBTC系统移动授权功能
2.2 时间自动机理论
2.3 小结
3 移动授权功能的形式化建模
3.1 移动授权功能逻辑分析
3.2 移动授权功能时间自动机模型的建立
3.3 移动授权功能时间自动机网络
3.4 小结
4 各场景下移动授权功能的形式化分层建模
4.1 各场景下移动授权功能模型的分层结构
4.2 各场景下移动授权功能时间自动机模型的建立
4.3 各场景下移动授权功能时间自动机网络
4.4 小结
5 基于UPPAAL的仿真与验证
5.1 验证工具UPPAAL
5.2 移动授权功能模型的仿真与验证
5.3 各场景下移动授权功能分层模型的仿真与验证
5.4 小结
结论
致谢
参考文献
攻读学位期间的研究成果
兰州交通大学;
