| 摘要 | 第1-7页 |
| ABSTRACT | 第7-9页 |
| 第一章 绪论 | 第9-17页 |
| ·形式验证 | 第9-12页 |
| ·软件和系统的可视化建模 | 第12-13页 |
| ·本文的主要研究内容 | 第13-15页 |
| ·本文的结构 | 第15-17页 |
| 第二章 并发和实时系统的模型检验技术 | 第17-29页 |
| ·时态逻辑和模型检验 | 第17-19页 |
| ·基于自动机理论的模型检验方法 | 第19-21页 |
| ·Symbolic模型检验 | 第21页 |
| ·模型检验的优化技术 | 第21-24页 |
| ·实时系统模型检验 | 第24-25页 |
| ·Statecharts模型检验 | 第25-26页 |
| ·存在的问题和发展方向 | 第26-29页 |
| 第三章 通过EHA表示UML Statecharts | 第29-43页 |
| ·统一建模语言UML | 第30-34页 |
| ·UML的结构 | 第30-31页 |
| ·UML的建模机制 | 第31-33页 |
| ·UML的主要特点 | 第33-34页 |
| ·UML Statecharts | 第34-37页 |
| ·UML Statecharts的语法 | 第34-35页 |
| ·UML Statecharts的语义 | 第35-37页 |
| ·UML Statecharts对应的EHA | 第37-39页 |
| ·EHA的形式操作语义 | 第39-43页 |
| 第四章 UML Statecharts的模型检验方法 | 第43-57页 |
| ·从UML Statecharts到Büchi自动机 | 第43-48页 |
| ·有穷字和无穷字上的自动机 | 第43-45页 |
| ·广义Büchi自动机 | 第45页 |
| ·EHA到Büchi自动机的生成算法 | 第45-48页 |
| ·用LTL公式描述UML模型的性质 | 第48-49页 |
| ·LTL公式到Büchi自动机的转换 | 第49-54页 |
| ·UML Statecharts的模型检验算法 | 第54-57页 |
| ·Büchi自动机的乘积 | 第54页 |
| ·Büchi自动机的判空 | 第54-57页 |
| 第五章 UML Statecharts的切片模型检验 | 第57-70页 |
| ·程序切片的概念与方法 | 第57-60页 |
| ·顺序程序切片 | 第57-59页 |
| ·并发程序切片 | 第59-60页 |
| ·EHA中的依赖关系 | 第60-64页 |
| ·EHA切片的生成 | 第64-68页 |
| ·从LTL公式中提取切片准则 | 第68-70页 |
| 第六章 并发多对象系统的验证 | 第70-82页 |
| ·并发多对象系统的建模 | 第70-71页 |
| ·同步和异步系统的验证 | 第71-75页 |
| ·同步系统的并发组合验证 | 第75-79页 |
| ·UML Statecharts的层次组合验证 | 第79-82页 |
| 第七章 模型检验工具UML-MC的设计与实现 | 第82-92页 |
| ·UML-MC的体系结构 | 第82-83页 |
| ·UML-MC的设计与实现 | 第83-88页 |
| ·UML模型接口 | 第84-85页 |
| ·EHA的文件格式 | 第85-86页 |
| ·系统用例图 | 第86页 |
| ·类图 | 第86-88页 |
| ·顺序图 | 第88页 |
| ·基于UML的软件测试和验证环境 | 第88-92页 |
| 第八章 结束语 | 第92-95页 |
| ·本文的主要贡献 | 第92-93页 |
| ·下一步研究工作 | 第93-95页 |
| 攻读博士学位期间发表的论文 | 第95-97页 |
| 致谢 | 第97-99页 |
| 参考文献 | 第99-107页 |
| 附录: 相关定理和推论的证明 | 第107-116页 |
