| 致谢 | 第1-7页 |
| 中文摘要 | 第7-9页 |
| ABSTRACT | 第9-15页 |
| 1 引言 | 第15-31页 |
| ·研究背景 | 第15-16页 |
| ·问题的提出 | 第16-20页 |
| ·安全通信的需求 | 第16-18页 |
| ·安全通信协议的作用 | 第18-20页 |
| ·安全通信协议验证需要解决的问题 | 第20-26页 |
| ·安全通信协议的验证方法需要解决的问题 | 第20-23页 |
| ·安全通信协议验证的研究现状及评述 | 第23-24页 |
| ·安全通信协议验证方法的提出 | 第24-26页 |
| ·研究意义 | 第26-27页 |
| ·研究内容 | 第27-31页 |
| 2 通信协议验证方法综述 | 第31-43页 |
| ·通信协议的Petri网仿真分析 | 第31-37页 |
| ·基于时间的Petri网 | 第32-34页 |
| ·基于层次的Petri网 | 第34-35页 |
| ·通信协议Petri网仿真分析存在的问题 | 第35-37页 |
| ·通信协议形式化验证方法 | 第37-41页 |
| ·基于网络的方法 | 第38页 |
| ·基于逻辑的方法 | 第38-40页 |
| ·通信协议形式化验证存在的问题 | 第40-41页 |
| ·仿真与形式化方法结合验证 | 第41页 |
| ·本章小结 | 第41-43页 |
| 3 安全通信协议的逻辑特性验证方法的研究 | 第43-69页 |
| ·论基础 | 第43-48页 |
| ·有色Petri网相关定义 | 第43-46页 |
| ·CTL基础知识 | 第46-48页 |
| ·基于CPN的安全通信协议的逻辑特性验证方法的实现 | 第48-56页 |
| ·安全通信协议功能的描述 | 第48-51页 |
| ·基于CPN的安全通信协议逻辑模型的建立方法 | 第51-54页 |
| ·基于ASK-CTL的安全通信协议逻辑特性的验证方法 | 第54-56页 |
| ·基于CPN的安全通信协议逻辑特性的验证 | 第56-66页 |
| ·基于CPN的安全通信协议逻辑模型的提取 | 第56-61页 |
| ·基于ASK-CTL的安全通信协议逻辑特性的验证 | 第61-66页 |
| ·本章小结 | 第66-69页 |
| 4 安全通信协议的时间特性验证方法的研究 | 第69-93页 |
| ·安全通信协议性能的描述 | 第69页 |
| ·基于CPN的安全通信协议时间特性验证方法 | 第69-75页 |
| ·基于CPN的安全通信协议的时间模型的建立 | 第70-71页 |
| ·基于CPN的安全通信协议的时间特性的验证 | 第71-75页 |
| ·随机条件下基于CPN的安全通信协议的时间特性验证方法 | 第75-92页 |
| ·含随机因素的安全通信协议的CPN模型 | 第75-78页 |
| ·基于CPN的安全通信协议的时间特性的仿真 | 第78-92页 |
| ·本章小结 | 第92-93页 |
| 5 基于CPN的CBTC安全通信协议的验证 | 第93-123页 |
| ·CBTC安全通信协议介绍 | 第93-97页 |
| ·基于CPN的CBTC安全通信协议验证 | 第97-121页 |
| ·CBTC安全通信协议验证需求的描述 | 第97页 |
| ·CBTC安全通信协议的CPN模型 | 第97-102页 |
| ·基于CPN的CBTC安全通信协议验证的实现 | 第102-120页 |
| ·CBTC安全通信协议验证结果的分析 | 第120-121页 |
| ·本章小结 | 第121-123页 |
| 6 总结和展望 | 第123-127页 |
| ·研究成果 | 第123-124页 |
| ·论文创新点 | 第124页 |
| ·展望 | 第124-127页 |
| 参考文献 | 第127-135页 |
| 作者简历、教育背景、攻读博士期间参与科研工作及发表的论文 | 第135-139页 |
| 学位论文数据集 | 第139页 |
