| 1 前言 | 第1-10页 |
| ·研究背景 | 第7-8页 |
| ·研究意义 | 第8页 |
| ·研究内容 | 第8-10页 |
| 2 时间自动机模型 | 第10-17页 |
| ·时间自动机 | 第10-13页 |
| ·时钟 | 第11页 |
| ·时钟约束 | 第11-12页 |
| ·时间自动机的定义 | 第12-13页 |
| ·时间转换表 | 第13-14页 |
| ·时间符号转换图的迁移分析 | 第14-17页 |
| 3 可达性问题的研究 | 第17-32页 |
| ·可达性问题的定义 | 第17-18页 |
| ·可达性问题判定的几种方法 | 第18-32页 |
| ·基于时钟域转换图的可达性分析 | 第19-24页 |
| ·基于时钟域代表的可达性分析 | 第24-27页 |
| ·基于时钟约束的可达性分析 | 第27-32页 |
| 4 基于时钟约束可达性判定的实现和改进 | 第32-43页 |
| ·时钟约束的计算机表述 | 第32-36页 |
| ·一种基于时间约束的后继计算方法 | 第36-38页 |
| ·可达性算法的预处理方法 | 第38-43页 |
| 5 结论和展望 | 第43-44页 |
| 致谢 | 第44-45页 |
| 参考文献 | 第45-49页 |
| 附录一 | 第49页 |