| 摘要 | 第1-4页 |
| Abstract | 第4-6页 |
| 目录 | 第6-8页 |
| 第一章 绪论 | 第8-12页 |
| 1．1 研究背景 | 第8-9页 |
| 1．2 研究现状 | 第9-11页 |
| 1．3 本文的组织 | 第11-12页 |
| 第二章 基于时间自动机的规范验证方法 | 第12-26页 |
| 2．1 时间自动机的定义 | 第12-16页 |
| 2．1．1 转换系统 | 第12-13页 |
| 2．1．2 时间语言 | 第13-14页 |
| 2．1．3 时钟约束和时钟解释 | 第14页 |
| 2．1．4 时间自动机的定义 | 第14-16页 |
| 2．2 确定的时间自动机 | 第16-17页 |
| 2．2．1 时间Büchi自动机 | 第16页 |
| 2．2．2 确定的时间自动机 | 第16-17页 |
| 2．3 基于时间自动机的实时系统的规范和验证方法研究 | 第17-26页 |
| 2．3．1 区域自动机 | 第17-21页 |
| 2．3．2 启发式规范验证方法 | 第21-24页 |
| 2．3．3 自动验证工具 | 第24-26页 |
| 第三章 UPPAAL验证技术的研究及改进 | 第26-40页 |
| 3．1 自动验证工具UPPAAL简介 | 第26-29页 |
| 3．1．1 UPPAAL的基本结构 | 第26-27页 |
| 3．1．2 位置分类 | 第27-28页 |
| 3．1．3 通道 | 第28页 |
| 3．1．4 规范说明语言 | 第28-29页 |
| 3．2 UPPAAL的验证技术 | 第29-33页 |
| 3．2．1 UPPAAL的限制技术 | 第30-31页 |
| 3．2．2 UPPAAL的快速验证技术 | 第31-32页 |
| 3．2．3 前向验证算法的分析 | 第32-33页 |
| 3．3 快速验证技术的改进 | 第33-40页 |
| 3．3．1 启发式搜索策略 | 第34-35页 |
| 3．3．2 前向验证算法的改进方法 | 第35-36页 |
| 3．3．3 改进后的前向验证算法 | 第36-40页 |
| 第四章 基于UPPAAL的通讯协议的自动验证实例 | 第40-44页 |
| 4．1 协议的规范说明 | 第40页 |
| 4．2 协议的建模 | 第40-42页 |
| 4．3 协议的规范验证 | 第42-44页 |
| 第五章 时延Petri网到时间自动机的等价转换算法 | 第44-52页 |
| 5．1 时延Petri网的定义 | 第44-45页 |
| 5．2 时间Petri网到时间自动机的语义等价转换算法 | 第45-47页 |
| 5．3 应用实例 | 第47-52页 |
| 5．3．1 铁路岔道系统描述 | 第47-48页 |
| 5．3．2 实验模型的语义等价转换 | 第48-51页 |
| 5．3．3 利用UPPAAL进行系统性质验证 | 第51-52页 |
| 第六章 总结和展望 | 第52-53页 |
| 参考文献 | 第53-58页 |
| 致谢 | 第58-59页 |
| 附录(攻读硕士学位期间发表的论文) | 第59页 |
