| 摘要 | 第1-5页 |
| ABSTRACT | 第5-10页 |
| 第一章 绪论 | 第10-14页 |
| ·课题背景 | 第10-11页 |
| ·课题来源和内容 | 第11-12页 |
| ·国内外研究的现状和发展态势 | 第12页 |
| ·论文的结构 | 第12-14页 |
| 第二章 相关的技术和工具 | 第14-23页 |
| ·模型驱动体系结构（MDA） | 第14-15页 |
| ·体系结构分析设计语言AADL 及开发工具集 | 第15-17页 |
| ·Matlab 建模工具Simulink 和Stateflow | 第17-19页 |
| ·建模工具Simulink | 第17-18页 |
| ·建模工具Stateflow | 第18页 |
| ·代码生成工具Real-Time Workshop | 第18-19页 |
| ·NXT 机器人平台和嵌入式汽车电子操作系统规范OSEK/VDX | 第19-21页 |
| ·硬件组件 | 第19-20页 |
| ·软件组件 | 第20-21页 |
| ·机器定理自动证明器PVS | 第21-22页 |
| ·本章小结 | 第22-23页 |
| 第三章 总体设计 | 第23-33页 |
| ·系统设计 | 第23-28页 |
| ·系统总体框架 | 第28-30页 |
| ·系统流程图 | 第30-32页 |
| ·本章小结 | 第32-33页 |
| 第四章 平台无关模块 | 第33-39页 |
| ·工具 | 第33页 |
| ·方案 | 第33-34页 |
| ·AADL FunctionList 模块库的设计 | 第34-35页 |
| ·平台无关模块代码生成器 | 第35-38页 |
| ·RTW 的配置 | 第37页 |
| ·RTW 生成程序 | 第37-38页 |
| ·本章小结 | 第38-39页 |
| 第五章 平台相关模块 | 第39-65页 |
| ·工具 | 第39页 |
| ·方案 | 第39-42页 |
| ·体系结构分析设计语言AADL 的元模型 | 第40-41页 |
| ·OSEK 的元模型 | 第41-42页 |
| ·AADL 属性集OSEK 和转换规则描述 | 第42-48页 |
| ·AADL2C 转换规则 | 第43-47页 |
| ·AADL201L 转换规则 | 第47-48页 |
| ·平台相关模块代码生成器 | 第48-57页 |
| ·信息采集模块 | 第49-52页 |
| ·规则映射模块 | 第52-57页 |
| ·平台相关模块代码生成器接口 | 第57-58页 |
| ·平台相关模型的可靠性分析（基于PVS） | 第58-60页 |
| ·可靠性分析实例 | 第60-63页 |
| ·经典的读写者问题 | 第60-62页 |
| ·验证读写者问题 | 第62-63页 |
| ·本章小结 | 第63-65页 |
| 第六章 整合模块 | 第65-74页 |
| ·整合工具 | 第65页 |
| ·整合方案 | 第65-66页 |
| ·代码整合具体的实现 | 第66-71页 |
| ·Java 执行MATLAB 命令 | 第66-67页 |
| ·Makefile 的自动生成 | 第67-69页 |
| ·编译和下载 | 第69-71页 |
| ·创建NXT 嵌入式生产线的应用程序向导 | 第71-72页 |
| ·本章小结 | 第72-74页 |
| 第七章 系统测试 | 第74-81页 |
| ·系统运行测试 | 第74-78页 |
| ·平台无关过程 | 第74-76页 |
| ·平台相关过程 | 第76页 |
| ·代码整合过程 | 第76-77页 |
| ·下载运行过程 | 第77-78页 |
| ·系统运行测试结果 | 第78页 |
| ·系统性能测试 | 第78-79页 |
| ·本章小结 | 第79-81页 |
| 第八章 展望 | 第81-83页 |
| ·课题总结 | 第81页 |
| ·课题特点 | 第81-82页 |
| ·课题的不足和展望 | 第82-83页 |
| 致谢 | 第83-84页 |
| 参考文献 | 第84-87页 |
