基于时间自动机的ECA规则系统建模与交互问题验证
| 摘要 | 第4-5页 |
| Abstract | 第5-6页 |
| 1 绪论 | 第9-16页 |
| 1.1 研究背景 | 第9-11页 |
| 1.2 问题研究及现状 | 第11-13页 |
| 1.3 研究目的和意义 | 第13-14页 |
| 1.4 论文的组织结构 | 第14-16页 |
| 2 ECA规则系统的时间自动机模型 | 第16-21页 |
| 2.1 时间自动机理论及UPPAAL概述 | 第16-19页 |
| 2.1.1 时间自动机理论 | 第16-17页 |
| 2.1.2 UPPAAL介绍 | 第17-19页 |
| 2.2 ECA规则系统特征分析 | 第19页 |
| 2.3 ECA规则系统模型定义 | 第19-20页 |
| 2.4 ECA规则系统交互问题验证 | 第20页 |
| 2.5 本章小结 | 第20-21页 |
| 3 基于时间自动机的ECA规则系统建模 | 第21-28页 |
| 3.1 事件建模 | 第21-25页 |
| 3.1.1 和事件建模 | 第22-23页 |
| 3.1.2 或事件建模 | 第23-24页 |
| 3.1.3 顺序事件建模 | 第24-25页 |
| 3.2 条件和动作建模 | 第25-26页 |
| 3.3 优先级和时间约束建模 | 第26-27页 |
| 3.4 本章小结 | 第27-28页 |
| 4 基于时间自动机的ECA规则系统交互问题验证 | 第28-40页 |
| 4.1 不一致性问题及终止性问题验证 | 第28-31页 |
| 4.1.1 规则执行自动机 | 第28-29页 |
| 4.1.2 规则调度自动机 | 第29-31页 |
| 4.2 正确性问题验证 | 第31-39页 |
| 4.2.1 Absence模式验证 | 第33-36页 |
| 4.2.2 Response模式验证 | 第36-39页 |
| 4.3 本章小结 | 第39-40页 |
| 5 案例分析及规则验证 | 第40-51页 |
| 5.1 案例介绍 | 第40-43页 |
| 5.2 案例ECA规则模型构建 | 第43-45页 |
| 5.3 案例交互问题验证模型构建 | 第45-47页 |
| 5.3.1 终止性和不一致性验证模型构建 | 第45-46页 |
| 5.3.2 正确性验证模型构建 | 第46-47页 |
| 5.4 验证结果分析 | 第47-50页 |
| 5.4.1 不一致性问题验证结果 | 第47-48页 |
| 5.4.2 终止性问题验证结果 | 第48-49页 |
| 5.4.3 正确性问题验证结果 | 第49-50页 |
| 5.5 本章小结 | 第50-51页 |
| 结论 | 第51-53页 |
| 参考文献 | 第53-57页 |
| 附录A 基于时间自动机的ECA规则模型 | 第57-60页 |
| 附录B 基于时间自动机的需求验证模型 | 第60-63页 |
| 攻读硕士学位期间发表学术论文情况 | 第63-64页 |
| 致谢 | 第64-65页 |
