基于时间自动机的列控中心软件形式化建模与验证
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-17页 |
| ·选题背景和意义 | 第11-12页 |
| ·国内外研究现状 | 第12-14页 |
| ·国外研究现状 | 第12-13页 |
| ·国内研究现状 | 第13-14页 |
| ·CTCS-3级列车运行控制系统仿真测试平台介绍 | 第14-15页 |
| ·论文主要工作 | 第15-17页 |
| 2 时间自动机理论和UPPAAL介绍 | 第17-25页 |
| ·形式化方法概述 | 第17-18页 |
| ·时间自动机理论 | 第18-21页 |
| ·时间自动机概述 | 第18-20页 |
| ·可达性分析 | 第20-21页 |
| ·模型分析工具UPPAAL | 第21-24页 |
| ·UPPAAL特征和结构 | 第21-23页 |
| ·UPPAAL的系统描述语言 | 第23-24页 |
| ·本章小结 | 第24-25页 |
| 3 报文编制流程的分层形式化建模 | 第25-47页 |
| ·TCC分层方案的设计 | 第25-31页 |
| ·报文编制流程的分层设计 | 第31-39页 |
| ·相关接口分析 | 第31-34页 |
| ·报文编制的场景分类 | 第34-35页 |
| ·报文编制的功能层设计 | 第35-38页 |
| ·报文编制的计算实现 | 第38-39页 |
| ·报文编制流程分层模型的建立 | 第39-45页 |
| ·接口层模型 | 第39-42页 |
| ·场景层模型 | 第42页 |
| ·功能层模型 | 第42-43页 |
| ·计算层模型 | 第43-45页 |
| ·报文编制流程的时间自动机网络的构建 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 4 基于UML与AT的轨道电路编码流程的建模 | 第47-72页 |
| ·基于UML与AT建模的特点 | 第47-48页 |
| ·轨道电路编码流程的UML类图的建立 | 第48-51页 |
| ·轨道电路编码流程的UML状态图的建立 | 第51-59页 |
| ·TS信息处理 | 第51-54页 |
| ·CI信息处理 | 第54-56页 |
| ·编码模块 | 第56-59页 |
| ·轨道电路编码主逻辑控制模块 | 第59页 |
| ·时间自动机的建模 | 第59-71页 |
| ·TS信息处理 | 第60-63页 |
| ·CI信息处理 | 第63-65页 |
| ·编码模块 | 第65-69页 |
| ·轨道电路编码主逻辑控制模块 | 第69-71页 |
| ·本章小结 | 第71-72页 |
| 5 模型的仿真及验证 | 第72-88页 |
| ·UPPAAL模拟仿真 | 第72-75页 |
| ·UPPAAL验证及错误处理 | 第75-83页 |
| ·功能验证 | 第75-79页 |
| ·软件错误推断检测 | 第79-83页 |
| ·TCC软件实现及验证 | 第83-87页 |
| ·本章小结 | 第87-88页 |
| 6 结论与展望 | 第88-90页 |
| ·结论 | 第88页 |
| ·展望 | 第88-90页 |
| 参考文献 | 第90-93页 |
| 图索引 | 第93-96页 |
| 表索引 | 第96-97页 |
| 作者简历 | 第97-99页 |
| 学位论文数据集 | 第99页 |
