声明
目 录
第 1 章 绪论
1.1 研究背景和意义
1.2 国内外研究现状
1.2.1 模型检测现状
1.2.2 状态空间约简现状
1.3 主要研究内容
1.4 论文结构
第 2 章 相关技术
2.1 模型检测
2.2 系统建模语言SysML
2.2.1 SysML概述
2.2.2 SysML状态图
2.3 模型检测的模型描述
2.3.1 Kripke结构概述
2.3.2 Kripke结构的表示方法
2.4 时序逻辑
2.4.1 线性时序逻辑
2.4.2 计算树时序逻辑
2.5 本章小结
第 3 章 嵌入式软件模型验证系统总体框架研究
3.1 总体技术框架
3.2 嵌入式软件模型验证技术研究
3.2.1 模型转换
3.2.2 嵌入式软件模型验证
3.3 基于邻接矩阵的状态空间约简技术研究
3.4 本章小结
第 4 章 嵌入式软件模型验证工具设计与实现
4.1 嵌入式软件模型验证工具功能及模块组成
4.2 嵌入式软件模型转换模块设计及实现
4.3 嵌入式软件模型验证模块设计及实现
4.4 本章小结
第 5 章 嵌入式软件状态空间约简工具设计与实现
5.1 嵌入式软件状态空间约简工具功能及模块组成
5.2 嵌入式软件状态约简模块设计
5.3 嵌入式软件状态空间约简工具实现
5.4 嵌入式软件模型验证系统功能性测试
5.5 本章小结
第 6 章 嵌入式软件模型验证系统测试与验证
6.1 实验对象背景
6.2 实验目的
6.3 实验环境
6.4 实验数据
6.5 实验步骤
6.6 实验结果及分析
6.7 实验结论
6.8 本章小结
第 7 章 结论与展望
7.1 工作总结
7.2 未来展望
参考文献
致 谢
作者简介
1 作者简历
2 攻读硕士学位期间发表的学术论文
3 参与的科研项目及获奖情况
4 发明专利
学位论文数据集
计算机技术傅磊浙江工业大学硕士学位论文2020夏
浙江工业大学;
