基于时间自动机的ECA规则系统建模与交互问题验证

摘要

ECA(Event-Condition-Action)规则首先在主动数据库中提出，它的含义是当检测到事件发生时，如果条件符合，执行相应的动作。ECA规则使系统行为的说明和管理集中于规则本身，而不是由多个不同的程序分别执行。基于ECA规则的系统具有较高的维护性和重构性，目前已在普适计算等领域得到广泛应用。ECA规则的系统有很吸引人的特征，如通过插入或改变规则的方式改变系统行为，并且能够对中断做出反应。但由于规则之间的交互问题导致规则系统的行为难以分析，由此引起系统行为的不可预测，使得基于ECA规则的系统难以得到广泛应用。因此在规则系统实施之前，为其提供有效的分析和验证，发现规则集合中存在的潜在交互问题，为系统的改进和优化提供帮助就显得尤为必要。
　　时间自动机是一种重要的形式化描述和验证技术，它具有直观性强的特点，并且支持和其它形式化方法的组合和转换。目前已被广泛用于系统建模和验证。本文以普适计算为研究背景，从实际需求出发，提出基于时间自动机的ECA规则系统建模和交互问题验证的方法，充分利用ECA规则系统的特点及时间自动机验证方面的优势。本文首先总结了国内外相关研究现状，在此基础上总结了研究工作存在的不足以及改进的方向。其次定义了基于时间自动机的ECA规则系统模型。文中将ECA规则中的事件建模、条件建模以及行动建模分别转换为时间自动机中动作、保卫公式以及有向边中的赋值操作。并将规则的优先级建模转换为时间自动机中的数据变量，时间约束建模转换为时间自动机中时钟变量。然后本文将规则系统交互问题验证转换为时间自动机模型验证问题。通过建立规则调度自动机和规则执行自动机，将终止性和不一致性等问题转换为对应的时间自动机模型验证中安全性和活性问题。同时，将常用的需求规范模式建模转换为对应的时间自动机模型，将正确性问题转换为时间自动机模型可达性问题。由上述时间自动机模型构成时间自动机网络，完整地刻画了ECA规则系统的运行过程。系统的运行过程表现为时间自动机网络模型上状态变迁通路。最后结合时间自动机建模验证工具UPPAAL，以阿尔茨海默病智能辅助系统为例，验证方法的可行性和有效性。
　　本文的研究说明，时间自动机能够较好的刻画ECA规则系统的相关特性。利用时间自动机建模方法，能够有效发现ECA规则间潜在的交互问题，并在一定程度上辅助ECA规则系统开发，并为开发人员提供改进建议。实验结果证明该方法具有一定的理论和应用价值。

目录

声明

摘要

1 绪论

1．1 研究背景

1．2 问题研究及现状

1．3 研究目的和意义

1．4 论文的组织结构

2 ECA规则系统的时间自动机模型

2．1 时间自动机理论及UPPAAL概述

2．1．1 时间自动机理论

2．1．2 UPPAAL介绍

2．2 EGA规则系统特征分析

2．3 ECA规则系统模型定义

2．4 ECA规则系统交互问题验证

2．5 本章小结

3 基于时间自动机的ECA规则系统建模

3．1 事件建模

3．1．1 和事件建模

3．1．2 或事件建模

3．1．3 顺序事件建模

3．2 条件和动作建模

3．3 优先级和时间约束建模

3．4 本章小结

4 基于时间自动机的ECA规则系统交互问题验证

4．1 不一致性问题及终止性问题验证

4．1．1 规则执行自动机

4．1．2 规则调度自动机

4．2 正确性问题验证

4．2．1 Absence模式验证

4．2．2 Response模式验证

4．3 本章小结

5 案例分析及规则验证

5．1 案例介绍

5．2 案例ECA规则模型构建

5．3 案例交互问题验证模型构建

5．3．1 终止性和不一致性验证模型构建

5．3．2 正确性验证模型构建

5．4 验证结果分析

5．4．1 不一致性问题验证结果

5．4．2 终止性问题验证结果

5．4．3 正确性问题验证结果

5．5 本章小结

结论

参考文献

附录

攻读硕士学位期间发表学术论文情况

致谢