| 摘要 | 第1-5页 |
| ABSTRACT | 第5-11页 |
| 第一章 绪论 | 第11-15页 |
| ·课题研究背景 | 第11-12页 |
| ·国内外研究现状及选题依据 | 第12-13页 |
| ·国内外研究现状 | 第12页 |
| ·选题依据 | 第12-13页 |
| ·论文组织结构 | 第13-15页 |
| 第二章 AADL的Z扩充 | 第15-30页 |
| ·Z语言简介 | 第15-17页 |
| ·AADL简介 | 第17-18页 |
| ·AADL组件 | 第18-22页 |
| ·软件组件 | 第18-20页 |
| ·执行平台组件 | 第20-22页 |
| ·系统组件 | 第22页 |
| ·AADL组件交互 | 第22-24页 |
| ·组件特征 | 第23页 |
| ·连接 | 第23-24页 |
| ·带数据约束的AADL规范（Z-AADL） | 第24-29页 |
| ·本章小结 | 第29-30页 |
| 第三章 面向Z-AADL的模型检测及实例 | 第30-51页 |
| ·ZIA规范简介 | 第30-34页 |
| ·接口自动机 | 第30-32页 |
| ·带Z的接口自动机（ZIA规范） | 第32页 |
| ·时间自动机 | 第32-33页 |
| ·基于连续时间的ZIA规范（CT-ZIA） | 第33-34页 |
| ·Z-AADL模型规范到基于连续时间的ZIA规范的转换 | 第34-36页 |
| ·有穷域自动机的构造 | 第36-39页 |
| ·等价域划分 | 第37-39页 |
| ·域自动机构造过程 | 第39页 |
| ·模型检测算法 | 第39-45页 |
| ·RT-DCL语法及语义定义 | 第39-40页 |
| ·转换过程的正确性 | 第40-42页 |
| ·模型检测算法 | 第42-45页 |
| ·系统实例 | 第45-50页 |
| ·问题描述 | 第45-47页 |
| ·CT-ZIA模型及其域自动机 | 第47-49页 |
| ·电器阀门系统的性质验证 | 第49-50页 |
| ·本章小结 | 第50-51页 |
| 第四章 Z-AADL的概率扩充 | 第51-59页 |
| ·概率系统 | 第51-54页 |
| ·Z-AADL的概率扩充 | 第51-54页 |
| ·基于离散时间的DT-PZIA | 第54-55页 |
| ·基于离散时间的DT-ZIA | 第54-55页 |
| ·概率Z-AADL模型的形式化转换 | 第55-58页 |
| ·本章小结 | 第58-59页 |
| 第五章 面向概率Z-AADL的模型检测及实例 | 第59-70页 |
| ·基于离散时间的CTML时序逻辑 | 第59-61页 |
| ·CTML语法 | 第59-60页 |
| ·CTML语义 | 第60-61页 |
| ·DT-ZIA的有界域 | 第61-62页 |
| ·DT-ZIA的验证算法 | 第62-63页 |
| ·实例验证 | 第63-69页 |
| ·认证电子邮件协议 | 第63页 |
| ·建模与验证 | 第63-67页 |
| ·机载大气数据系统的建模与验证 | 第67-69页 |
| ·本章小结 | 第69-70页 |
| 第六章 总结与展望 | 第70-72页 |
| ·论文总结 | 第70-71页 |
| ·未来工作展望 | 第71-72页 |
| 参考文献 | 第72-76页 |
| 致谢 | 第76-78页 |
| 在学期间的研究成果及发表的学术论文 | 第78页 |