| <中文摘要> | 第1页 |
| <关键词> | 第3-4页 |
| <英文摘要> | 第4-5页 |
| <英文关键词> | 第5-8页 |
| 第一章 引 言 | 第8-15页 |
| ·反应系统 | 第8-10页 |
| ·实时和混成系统 | 第10-11页 |
| ·本文的目标、贡献和组成 | 第11-15页 |
| 第二章 线性时序逻辑LTL简介 | 第15-22页 |
| ·线性时序逻辑LTL | 第15-18页 |
| ·LTL公式的可满足性的判定 | 第18-22页 |
| 第三章 连续语义线性时序逻辑LTLC | 第22-42页 |
| ·预备概念 | 第22-24页 |
| ·LTLC的语法 | 第24-25页 |
| ·LTLC的语义 | 第25-30页 |
| ·利用LTLC/B－公式表示有穷状态反应系统 | 第30-36页 |
| ·LTLC/B－公式的可满足性判定 | 第36-41页 |
| ·小结 | 第41-42页 |
| 第四章 实时系统 | 第42-75页 |
| ·基本概念 | 第42-43页 |
| ·时间模块及其验证 | 第43-57页 |
| ·时间模块的模型检查与LTLC/R公式的可满足性判定 | 第57-74页 |
| ·小结 | 第74-75页 |
| 第五章 混成系统 | 第75-99页 |
| ·基本概念 | 第75-77页 |
| ·混成模块 | 第77-80页 |
| ·使用LTLC验证混成系统的性质 | 第80-86页 |
| ·多速率成模块的样本模型检查 | 第86-98页 |
| ·小结 | 第98-99页 |
| 第六章 相关工作 | 第99-103页 |
| ·实时逻辑 | 第99-102页 |
| ·实时和混成系统的验证 | 第102-103页 |
| 第七章 总结 | 第103-105页 |
| 攻读博士学位期间发表和录用的文章 | 第105-106页 |
| 致 谢 | 第106-107页 |
| <引文> | 第107-115页 |