| 中文摘要 | 第5-7页 |
| Abstract | 第7-8页 |
| 第一章 绪论 | 第13-19页 |
| 1.1 问题描述 | 第13-14页 |
| 1.2 研究意义 | 第14页 |
| 1.3 国内外研究现状 | 第14-16页 |
| 1.4 存在的问题 | 第16-17页 |
| 1.5 本文的研究目标与工作 | 第17页 |
| 1.6 论文的结构 | 第17-19页 |
| 第二章 研究基础 | 第19-33页 |
| 2.1 模型驱动开发(MDD) | 第19页 |
| 2.2 AADL概述 | 第19-23页 |
| 2.2.1 AADL的构件 | 第20-22页 |
| 2.2.2 AADL端口和连接 | 第22页 |
| 2.2.3 AADL语法 | 第22-23页 |
| 2.3 时间自动机网络 | 第23-24页 |
| 2.4 模型开发框架Eclipse Modeling Framework | 第24-25页 |
| 2.5 模型转换语言Atlas Transformation Language | 第25-26页 |
| 2.6 Eclipse插件技术 | 第26页 |
| 2.7 开源工具OSATE | 第26-27页 |
| 2.8 UPPAAL工具 | 第27-31页 |
| 2.8.1 UPPAAL的扩展元素 | 第29-31页 |
| 2.9 本章小结 | 第31-33页 |
| 第三章 满足UPPAAL验证器转换的AADL子集选取 | 第33-47页 |
| 3.1 满足子集选择原则 | 第33-35页 |
| 3.2 AADL子集获取结论 | 第35页 |
| 3.3 AADL组件 | 第35-44页 |
| 3.3.1 AADL软件组件 | 第36-44页 |
| 3.4 组件交互 | 第44-45页 |
| 3.5 本章小结 | 第45-47页 |
| 第四章 AADL到UPPAAL的转换流程设计 | 第47-50页 |
| 4.1 AADL模型转换中的术语 | 第47-48页 |
| 4.1.1 AADL模型转换 | 第47页 |
| 4.1.2 AADL语法转换 | 第47-48页 |
| 4.1.3 AADL语义转换 | 第48页 |
| 4.2 AADL的ATL转换流程 | 第48-49页 |
| 4.3 行为附件的ATL转换流程 | 第49页 |
| 4.4 本章小结 | 第49-50页 |
| 第五章 基于AADL子集到UPPAAL的转换规则设计 | 第50-58页 |
| 5.1 元模型及其获取 | 第50-52页 |
| 5.1.1 元模型 | 第50-51页 |
| 5.1.2 AADL的元模型与UPPAAL的元模型设计 | 第51-52页 |
| 5.2 AADL到UPPAAL的转换规则设计 | 第52-57页 |
| 5.2.1 总体思路 | 第52-53页 |
| 5.2.2 AADL子集到UPPAAL状态机的转换规则设计 | 第53-57页 |
| 5.2.3 上下文与AADL子集转换需要注意的问题 | 第57页 |
| 5.3 本章小结 | 第57-58页 |
| 第六章 BA到UPPAAL的转换规则设计 | 第58-66页 |
| 6.1 总体思路 | 第58页 |
| 6.2 BA到UPPAAL状态机的转换规则设计 | 第58-65页 |
| 6.3 特殊功能 | 第65页 |
| 6.4 本章小结 | 第65-66页 |
| 第七章 规则生成器设计 | 第66-73页 |
| 7.1 规则生成器的提出 | 第66页 |
| 7.2 规则生成器的主要技术路线 | 第66-67页 |
| 7.3 UPPAAL状态机模型元素的子集选取 | 第67-68页 |
| 7.3.1 UPPAAL子集选取 | 第67-68页 |
| 7.3.2 UPPAAL子集选取结论 | 第68页 |
| 7.4 选取的UPPAAL子集元素与代码生成规则 | 第68-71页 |
| 7.5 运行效果 | 第71-72页 |
| 7.6 本章小结 | 第72-73页 |
| 第八章 AADL子集到UPPAAL工具转换系统的设计与实现 | 第73-84页 |
| 8.1 AADL子集到UPPAAL工具转换系统的设计 | 第73-81页 |
| 8.1.1 AADL子集到UPPAAL工具转换系统的需求分析 | 第73-78页 |
| 8.1.2 建议的软件体系结构框架 | 第78-79页 |
| 8.1.3 软件体系结构细化设计 | 第79-81页 |
| 8.2 AADL子集到UPPAAL工具转换系统的实现 | 第81-83页 |
| 8.2.1 XMI格式的模型处理 | 第81页 |
| 8.2.2 模型的预处理 | 第81-82页 |
| 8.2.3 控制ATL转换 | 第82页 |
| 8.2.4 模型的后处理 | 第82-83页 |
| 8.2.5 工具集成 | 第83页 |
| 8.3 本章小结 | 第83-84页 |
| 第九章 案例分析与验证 | 第84-91页 |
| 9.1 生产者与消费者问题 | 第84-86页 |
| 9.1.1 问题描述 | 第84页 |
| 9.1.2 生产者与消费者问题的AADL模型设计 | 第84-86页 |
| 9.2 简单铁路闸道控制问题 | 第86-90页 |
| 9.2.1 问题描述 | 第86-87页 |
| 9.2.2 简单铁路闸道控制问题的AADL模型设计 | 第87-90页 |
| 9.3 本章小结 | 第90-91页 |
| 第十章 总结与展望 | 第91-93页 |
| 10.1 全文总结 | 第91-92页 |
| 10.2 进一步研究展望 | 第92-93页 |
| 参考文献 | 第93-96页 |
| 附录 | 第96-127页 |
| 致谢 | 第127页 |
