ATS系统内部通信协议的设计及形式化验证
| 致谢 | 第1-6页 |
| 中文摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 绪论 | 第11-18页 |
| ·课题研究背景 | 第12-15页 |
| ·列车自动监控系统概述 | 第12-14页 |
| ·ATS系统内部通信协议 | 第14-15页 |
| ·符号模型检验技术及工具 | 第15-16页 |
| ·选题目的及意义 | 第16-17页 |
| ·本文的结构安排 | 第17-18页 |
| 2 形式化验证方法 | 第18-28页 |
| ·形式化验证方法概述 | 第18-20页 |
| ·符号模型检验 | 第20-23页 |
| ·符号模型检验概述 | 第20-21页 |
| ·Kripke结构 | 第21-22页 |
| ·计算树逻辑CTL | 第22-23页 |
| ·符号模型检验工具SMV | 第23-27页 |
| ·SMV工具简介 | 第23-24页 |
| ·SMV工作原理 | 第24-25页 |
| ·SMV语言 | 第25-26页 |
| ·使用SMV发现的问题 | 第26-27页 |
| ·小结 | 第27-28页 |
| 3 ATS系统内部通信协议的设计 | 第28-45页 |
| ·Rational Rose设计工具简述 | 第28-29页 |
| ·ATS系统内部通信协议需求分析及设计策略 | 第29-33页 |
| ·结构需求分析 | 第29-30页 |
| ·数据传输需求分析 | 第30-31页 |
| ·链路状态需求分析 | 第31页 |
| ·设计策略 | 第31-33页 |
| ·ATS系统内部通信协议架构设计及模块划分 | 第33-36页 |
| ·总体结构 | 第33-34页 |
| ·模块划分及功能描述 | 第34-36页 |
| ·ATS系统内部通信协议模块设计 | 第36-44页 |
| ·类图设计 | 第36-37页 |
| ·通信传输类库初始化 | 第37-38页 |
| ·数据发送序列图 | 第38-39页 |
| ·数据接收 | 第39页 |
| ·数据处理流程 | 第39-40页 |
| ·将数据插入上传数据列表 | 第40-42页 |
| ·数据上传流程 | 第42-43页 |
| ·关键数据报文的发送 | 第43页 |
| ·关键数据报文的接收 | 第43-44页 |
| ·小结 | 第44-45页 |
| 4 ATS系统内部通信协议的形式化验证 | 第45-62页 |
| ·临界区操作状态迁移模型及形式化验证 | 第45-51页 |
| ·临界区操作状态迁移模型 | 第45-47页 |
| ·验证结果及分析 | 第47-49页 |
| ·对改进后的状态迁移模型验证结果及分析 | 第49-51页 |
| ·数据冗余处理状态迁移模型及验证 | 第51-54页 |
| ·数据冗余处理状态迁移图模型 | 第51-52页 |
| ·验证结果及分析 | 第52-54页 |
| ·关键数据报文处理状态迁移模型及形式化验证 | 第54-61页 |
| ·发送方状态迁移图模型 | 第55-56页 |
| ·接收方状态迁移图模型 | 第56页 |
| ·信道状态迁移图模型 | 第56-58页 |
| ·验证结果及分析 | 第58-61页 |
| ·小结 | 第61-62页 |
| 5 总结与展望 | 第62-64页 |
| ·工作总结 | 第62页 |
| ·工作展望 | 第62-64页 |
| 参考文献 | 第64-66页 |
| 图索引 | 第66-67页 |
| 作者简历 | 第67-69页 |
| 学位论文数据集 | 第69页 |
