| 摘要 | 第5-6页 |
| Abstract | 第6-7页 |
| 第一章 绪论 | 第11-17页 |
| 1.1 研究背景及意义 | 第11-12页 |
| 1.2 研究现状 | 第12-15页 |
| 1.3 本文主要研究内容 | 第15-16页 |
| 1.4 本文的框架结构 | 第16-17页 |
| 第二章 相关技术概述 | 第17-31页 |
| 2.1 嵌入式工业控制系统的概述 | 第17页 |
| 2.2 UML建模语言及扩展 | 第17-22页 |
| 2.2.1 UML简介 | 第18-19页 |
| 2.2.2 UML顺序图 | 第19-20页 |
| 2.2.3 UML顺序图及扩展 | 第20-22页 |
| 2.3 时间自动机 | 第22-25页 |
| 2.3.1 时间自动机的语法和语义 | 第22-24页 |
| 2.3.2 时间自动机的网络语法和语义 | 第24页 |
| 2.3.3 时间自动机的网络建模 | 第24-25页 |
| 2.4 形式化验证方法 | 第25-31页 |
| 2.4.1 形式化验证的方法 | 第25-26页 |
| 2.4.2 基于时间自动机的验证 | 第26-27页 |
| 2.4.3 模型分析验证工具UPPAAL | 第27-31页 |
| 第三章 基于时间自动机的嵌入式工业控制系统模型生成方法 | 第31-39页 |
| 3.1 系统UML模型转化时间自动机模型的方法 | 第31-33页 |
| 3.1.1 UML顺序图的时间自动机构造 | 第31-32页 |
| 3.1.2 时间约束的模型构造 | 第32-33页 |
| 3.2 时间自动机模型自动生成方法 | 第33-39页 |
| 3.2.1 任务关系映射 | 第33-34页 |
| 3.2.2 时间自动机对于模型的引用 | 第34-36页 |
| 3.2.3 时间自动机模型的生成方法 | 第36-39页 |
| 第四章 基于时间自动机的嵌入式工业控制系统实例建模 | 第39-55页 |
| 4.1 UML模型转化的时间自动机方法场景建模 | 第39-50页 |
| 4.1.1 嵌入式工业控制系统实例的场景概述 | 第39-43页 |
| 4.1.2 嵌入式工业控制系统实例的场景切换规则 | 第43-44页 |
| 4.1.3 嵌入式工业控制系统实例的运营场景建模 | 第44-50页 |
| 4.2 嵌入式工业控制系统的自动机模型 | 第50-55页 |
| 4.2.1 时间自动机自动转换模型的场景对象 | 第50-51页 |
| 4.2.2 时间自动机自动转换模型的实例建模 | 第51-55页 |
| 第五章 时间自动机模型在UPPAAL上的验证及分析 | 第55-67页 |
| 5.1 时间自动机网络的构建与验证 | 第55-59页 |
| 5.1.1 时间自动机网络的构建 | 第56-57页 |
| 5.1.2 时间自动机网络的验证 | 第57-59页 |
| 5.2 嵌入式工业控制系统的时间自动机模型验证 | 第59-61页 |
| 5.3 仿真结果的比较分析 | 第61-67页 |
| 第六章 总结 | 第67-69页 |
| 致谢 | 第69-71页 |
| 参考文献 | 第71-77页 |
| 附录A 攻读学位期间发表论文目录 | 第77-79页 |
| 附录B 攻读学位期间参与的研究工作 | 第79页 |
