| 摘要 | 第1-5页 |
| ABSTRACT | 第5-8页 |
| 图表清单 | 第8-10页 |
| 注释表 | 第10-11页 |
| 第一章 绪论 | 第11-15页 |
| ·课题研究背景及意义 | 第11-12页 |
| ·当前研究现状及选题依据 | 第12-13页 |
| ·论文的研究内容 | 第13-15页 |
| 第二章 基于模型的形式化验证方法 | 第15-24页 |
| ·形式化验证方法概述 | 第15-16页 |
| ·基于模型的形式化验证方法 | 第16-17页 |
| ·系统动态行为描述模型 | 第17-23页 |
| ·接口自动机及其扩展模型 | 第17-21页 |
| ·接口自动机网络模型 | 第21-22页 |
| ·图形化建模工具JFLAP 简介 | 第22-23页 |
| ·本章小结 | 第23-24页 |
| 第三章 基于场景规约的即时验证 | 第24-35页 |
| ·UML 交互概观图描述及建模工具 | 第24-27页 |
| ·UML 交互概观图描述 | 第24-26页 |
| ·图形化建模工具Topcased 简介 | 第26-27页 |
| ·相关验证问题及即时验证算法描述 | 第27-34页 |
| ·非实时功能行为的即时验证 | 第27-29页 |
| ·实时功能行为的即时验证 | 第29-30页 |
| ·资源性质的即时验证 | 第30-33页 |
| ·能耗性质的即时验证 | 第33-34页 |
| ·本章小结 | 第34-35页 |
| 第四章 T-CBESD 扩展概述及输入接口的扩展设计与实现 | 第35-48页 |
| ·现有模型验证工具的分析 | 第35-37页 |
| ·T-CBESD 工具扩展概述 | 第37-42页 |
| ·扩展设计的基本思想 | 第37-39页 |
| ·工具界面的重新设计与实现 | 第39-42页 |
| ·输入接口的扩展设计与实现 | 第42-47页 |
| ·UML 交互概观图模型预处理模块 | 第42-45页 |
| ·接口自动机模型预处理模块 | 第45-47页 |
| ·本章小结 | 第47-48页 |
| 第五章 即时验证模块的设计与实现 | 第48-57页 |
| ·非实时功能行为即时验证模块的设计与实现 | 第49-51页 |
| ·实时行为即时验证模块的设计与实现 | 第51-53页 |
| ·资源性质即时验证模块的设计与实现 | 第53-55页 |
| ·能耗性质即时验证模块的设计与实现 | 第55-56页 |
| ·本章小结 | 第56-57页 |
| 第六章 实例应用与分析 | 第57-65页 |
| ·火灾预警系统实例分析 | 第57-61页 |
| ·通信构件组合系统实例分析 | 第61-64页 |
| ·本章小结 | 第64-65页 |
| 第七章 总结与展望 | 第65-67页 |
| ·总结 | 第65-66页 |
| ·展望 | 第66-67页 |
| 参考文献 | 第67-71页 |
| 致谢 | 第71-72页 |
| 在学期间的研究成果及发表的学术论文 | 第72页 |