| 摘要 | 第3-4页 |
| abstract | 第4-5页 |
| 主要符号对照表 | 第8-9页 |
| 第1章 绪论 | 第9-20页 |
| 1.1 研究背景 | 第9-13页 |
| 1.2 研究现状 | 第13-17页 |
| 1.3 研究思路 | 第17-18页 |
| 1.4 论文贡献 | 第18-19页 |
| 1.5 论文结构 | 第19-20页 |
| 第2章 基于有色Petri网的嵌入式软件建模与验证 | 第20-43页 |
| 2.1 引言 | 第20-21页 |
| 2.2 相关工作 | 第21-22页 |
| 2.3 基础背景 | 第22-26页 |
| 2.4 嵌入式系统软件 | 第26-27页 |
| 2.5 针对嵌入式系统软件特征的建模 | 第27-29页 |
| 2.6 MVB系统中板卡通讯实现建模案例 | 第29-41页 |
| 2.6.1 背景介绍 | 第29-32页 |
| 2.6.2 基于有色Petri网的模型表示 | 第32-36页 |
| 2.6.3 模型的仿真分析 | 第36-38页 |
| 2.6.4 模型的验证 | 第38-41页 |
| 2.7 本章小结 | 第41-43页 |
| 第3章 扩展的Petri网计算模型 | 第43-67页 |
| 3.1 引言 | 第43-44页 |
| 3.2 相关工作 | 第44页 |
| 3.3 交互式Petri网计算模型 | 第44-59页 |
| 3.3.1 图形示例 | 第45-52页 |
| 3.3.2 模型文法 | 第52-59页 |
| 3.4 计算模型执行语义 | 第59-61页 |
| 3.5 计算模型形式语义 | 第61-65页 |
| 3.6 状态空间遍历和属性验证 | 第65-66页 |
| 3.7 本章小结 | 第66-67页 |
| 第4章 集成开发环境 | 第67-90页 |
| 4.1 引言 | 第67-70页 |
| 4.2 Tsmart-IPNEX功能组成 | 第70-78页 |
| 4.2.1 图形化模型编辑器 | 第70-73页 |
| 4.2.2 交互式模型仿真器 | 第73-77页 |
| 4.2.3 模型检测工具集成 | 第77页 |
| 4.2.4 代码综合工具 | 第77-78页 |
| 4.3 Tsmart-IPNEX应用案例 | 第78-84页 |
| 4.4 Tsmart-IPNEX用户交互界面 | 第84-89页 |
| 4.4.1 创建项目 | 第84-85页 |
| 4.4.2 图形化建模 | 第85-86页 |
| 4.4.3 交互仿真 | 第86-88页 |
| 4.4.4 模型验证 | 第88-89页 |
| 4.4.5 代码生成 | 第89页 |
| 4.5 本章小结 | 第89-90页 |
| 第5章 结束语 | 第90-92页 |
| 5.1 工作总结 | 第90-91页 |
| 5.2 研究展望 | 第91-92页 |
| 插图索引 | 第92-95页 |
| 表格索引 | 第95-96页 |
| 参考文献 | 第96-101页 |
| 致谢 | 第101-103页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第103页 |