基于AADL的嵌入式软件形式化验证研究
| 摘要 | 第3-5页 |
| Abstract | 第5-6页 |
| 第1章 绪论 | 第10-14页 |
| 1.1 研究背景及研究意义 | 第10-11页 |
| 1.2 国内外研究现状 | 第11-12页 |
| 1.3 本文研究内容与论文结构 | 第12-14页 |
| 第2章 体系结构分析与设计语言(AADL) | 第14-24页 |
| 2.1 AADL总体介绍 | 第14-15页 |
| 2.2 AADL组件 | 第15-21页 |
| 2.2.1 软件组件 | 第15-18页 |
| 2.2.2 硬件组件 | 第18-20页 |
| 2.2.3 系统组件 | 第20-21页 |
| 2.3 组件交互 | 第21-22页 |
| 2.3.1 端口 | 第21页 |
| 2.3.2 子组件访问 | 第21页 |
| 2.3.3 子程序调用 | 第21页 |
| 2.3.4 参数交互和子程序共享 | 第21-22页 |
| 2.4 本章小结 | 第22-24页 |
| 第3章 基于AADL的ARINC653形式化描述 | 第24-42页 |
| 3.1 ARINC653标准简介 | 第25-28页 |
| 3.1.1 时间和空间分区策略 | 第26-27页 |
| 3.1.2 通信服务 | 第27-28页 |
| 3.1.3 任务管理 | 第28页 |
| 3.2 基于AADL的ARINC653模型定义 | 第28-37页 |
| 3.2.1 层间任务模型 | 第29-33页 |
| 3.2.2 系统层分区模型 | 第33-35页 |
| 3.2.3 系统错误模型 | 第35-37页 |
| 3.3 基于REAL验证形式化的有效性 | 第37-40页 |
| 3.4 本章总结 | 第40-42页 |
| 第4章 基于加权轮转的ARINC653调度 | 第42-50页 |
| 4.1 简介 | 第42-43页 |
| 4.2 基于加权轮转的空间分区模型 | 第43页 |
| 4.3 基于加权轮转的分区调度算法 | 第43-45页 |
| 4.4 基于RMS的分区调度算法 | 第45-47页 |
| 4.5 调度分析 | 第47-48页 |
| 4.6 本章总结 | 第48-50页 |
| 第5章 基于随机petri网的AADL可靠性模型 | 第50-64页 |
| 5.1 简介 | 第50-51页 |
| 5.2 软件可靠性 | 第51-52页 |
| 5.3 PETRI网简介 | 第52-53页 |
| 5.4 AADL到随机PETRI网转换 | 第53-62页 |
| 5.5 可靠性分析方法 | 第62-63页 |
| 5.6 本章总结 | 第63-64页 |
| 第6章 航电系统飞行规划功能实例 | 第64-72页 |
| 6.1 实例描述 | 第64-68页 |
| 6.2 可调度性分析 | 第68-69页 |
| 6.3 可靠性分析 | 第69-70页 |
| 6.4 本章总结 | 第70-72页 |
| 第7章 总结与展望 | 第72-74页 |
| 7.1 本文工作总结 | 第72-73页 |
| 7.2 未来工作展望 | 第73-74页 |
| 参考文献 | 第74-80页 |
| 致谢 | 第80-82页 |
| 攻读硕士期间的研究成果 | 第82页 |
