声明
注释表
缩略词
第一章 绪论
1.1 概述
1.2 国内外研究现状
1.3 论文研究动机与目标
1.4 论文主要研究工作
1.5 论文组织结构
第二章 嵌入式软件形式化模型Z-MARTE
2.1 Z-MARTE模型概述
2.2 Z-MARTE时间模型设计
2.3 Z-MARTE结构模型设计
2.4 Z-MARTE可信构造型设计
2.5 Z-MARTE行为模型设计
2.6 实例研究
2.7 Z-MARTE模型可信性质的确认
2.8 本章小结
第三章 基于Z-MARTE的模型检测方法
3.1 Z-MARTE行为模型的一种时序逻辑
3.2 有限域Z-MARTE行为模型上的模型检测
3.3 实例研究
3.4 本章小结
第四章 基于Z-MARTE的风险评估方法
4.1 嵌入式软件的对象-消息-角色模型OMR
4.2 RAMES风险评估方法
4.3 实例研究
4.4 本章小结
第五章 基于Z-MARTE的建模与验证原型系统
5.1 系统框架与流程设计
5.2 全局数据结构设计
5.3 Z-MARTE模型转换机制
5.4 Z-MARTE模型解析机制
5.5 实例研究
5.6 本章小结
第六章 总结与展望
6.1 研究工作总结
6.2 进一步研究工作
参考文献
致谢
在学期间的研究成果及发表的学术论文
附录1 定理3.1证明过程
附录2 XSLT样式表定义