嵌入式软件可信性建模与验证技术的研究及其应用
| 摘要 | 第4-6页 |
| Abstract | 第6-7页 |
| 注释表 | 第13-14页 |
| 缩略词 | 第14-16页 |
| 第一章 绪论 | 第16-40页 |
| 1.1 概述 | 第16-19页 |
| 1.2 国内外研究现状 | 第19-34页 |
| 1.2.1 嵌入式软件的可信性指标体系 | 第19-21页 |
| 1.2.2 嵌入式软件的半形式化与形式化建模方法 | 第21-29页 |
| 1.2.3 软件模型检测方法 | 第29-31页 |
| 1.2.4 嵌入式软件的风险评估标准与方法 | 第31-34页 |
| 1.3 论文研究动机与目标 | 第34-35页 |
| 1.4 论文主要研究工作 | 第35-37页 |
| 1.5 论文组织结构 | 第37-40页 |
| 第二章 嵌入式软件形式化模型Z-MARTE | 第40-64页 |
| 2.1 Z-MARTE模型概述 | 第40-41页 |
| 2.2 Z-MARTE时间模型设计 | 第41-44页 |
| 2.3 Z-MARTE结构模型设计 | 第44-46页 |
| 2.4 Z-MARTE可信构造型设计 | 第46-47页 |
| 2.5 Z-MARTE行为模型设计 | 第47-49页 |
| 2.6 实例研究 | 第49-57页 |
| 2.6.1 需求描述与半形式化模型 | 第49-51页 |
| 2.6.2 实例的Z-MARTE时间模型 | 第51-52页 |
| 2.6.3 实例的Z-MARTE结构模型 | 第52-54页 |
| 2.6.4 实例的Z-MARTE可信构造型 | 第54-56页 |
| 2.6.5 实例的Z-MARTE行为模型 | 第56-57页 |
| 2.7 Z-MARTE模型可信性质的确认 | 第57-62页 |
| 2.7.1 实时性确认 | 第58-59页 |
| 2.7.2 安全性确认 | 第59-60页 |
| 2.7.3 可靠性确认 | 第60-62页 |
| 2.8 本章小结 | 第62-64页 |
| 第三章 基于Z-MARTE的模型检测方法 | 第64-74页 |
| 3.1 Z-MARTE行为模型的一种时序逻辑 | 第64-66页 |
| 3.1.1 Z-MARTE行为模型的动态语义 | 第64-65页 |
| 3.1.2 时序逻辑公式ZMTL定义 | 第65-66页 |
| 3.2 有限域Z-MARTE行为模型上的模型检测 | 第66-68页 |
| 3.2.1 有限域Z-MARTE行为模型定义 | 第66-67页 |
| 3.2.2 模型检测算法FZMCA的设计 | 第67-68页 |
| 3.3 实例研究 | 第68-71页 |
| 3.4 本章小结 | 第71-74页 |
| 第四章 基于Z-MARTE的风险评估方法 | 第74-96页 |
| 4.1 嵌入式软件的对象-消息-角色模型OMR | 第74-79页 |
| 4.1.1 对象模型的形式化定义 | 第75-76页 |
| 4.1.2 消息模型的形式化定义 | 第76-77页 |
| 4.1.3 角色模型的形式化定义 | 第77-78页 |
| 4.1.4 OMR模型形式化定义 | 第78-79页 |
| 4.2 RAMES风险评估方法 | 第79-86页 |
| 4.2.1 风险环境建立 | 第80页 |
| 4.2.2 风险识别方法 | 第80-81页 |
| 4.2.3 RAOMR风险分析算法 | 第81-86页 |
| 4.2.4 风险处理方法 | 第86页 |
| 4.3 实例研究 | 第86-93页 |
| 4.3.1 实例的风险评估需求 | 第87页 |
| 4.3.2 实例的OMR模型 | 第87-91页 |
| 4.3.3 实例的风险评估过程 | 第91-93页 |
| 4.4 本章小结 | 第93-96页 |
| 第五章 基于Z-MARTE的建模与验证原型系统 | 第96-122页 |
| 5.1 系统框架与流程设计 | 第96-98页 |
| 5.1.1 系统框架设计 | 第96-97页 |
| 5.1.2 系统流程设计 | 第97-98页 |
| 5.2 全局数据结构设计 | 第98-100页 |
| 5.3 Z-MARTE模型转换机制 | 第100-111页 |
| 5.3.1 XML与XSLT | 第101-102页 |
| 5.3.2 基于XSLT的模型转换机制 | 第102-111页 |
| 5.4 Z-MARTE模型解析机制 | 第111-113页 |
| 5.5 实例研究 | 第113-121页 |
| 5.5.1 需求描述 | 第113页 |
| 5.5.2 半形式化模型 | 第113-114页 |
| 5.5.3 实例的模型转换 | 第114-115页 |
| 5.5.4 实例的Z-MARTE模型 | 第115-119页 |
| 5.5.5 模型检测过程 | 第119-121页 |
| 5.6 本章小结 | 第121-122页 |
| 第六章 总结与展望 | 第122-126页 |
| 6.1 研究工作总结 | 第122-123页 |
| 6.2 进一步研究工作 | 第123-126页 |
| 参考文献 | 第126-138页 |
| 致谢 | 第138-140页 |
| 在学期间的研究成果及发表的学术论文 | 第140-142页 |
| 附录1 定理 3.1 证明过程 | 第142-144页 |
| 附录2 XSLT样式表定义 | 第144-147页 |
