ECA Rules System Modeling And Interaction Problem Verification Based On Timed Automata

ECA (Event-Condition-Action) rule was firstly proposed in the active database. It means that when the event is detected and the conditions are met, then, appropriate action is taken. ECA rules make the description and management of system behavior focus on the rules themselves, rather than execute separately by a plurality of different programs. The system of ECA rules has higher maintenance and reconfiguration, which has been applied in pervasive computing areas. ECA rules-based system has very attractive features, for example:it is easy to change the system behavior by inserting or changing the rules and is able to respond to the interrupt. However, it has not been widely applied. One important reason is that the behavior of the system based on ECA rules is difficult to analyze, and this difficulty comes from the interaction of rules. The interaction among rules may make the system behavior unpredictable or unsafe. Therefore, it is particularly necessary to provide effective analysis and validation before the implementation of the rule system, so as to discovery potential interaction problems in the rule set and provide help on the improvement and optimization of system.The timed automata is an important formal description and verification technique, which has strong intuition and can be implemented in combination and conversion with other formal methods. And it has been widely used for system modeling and verification. This article takes pervasive computing as a research background and starts from the actual demand, proposing a method of system modeling of ECA rules and interaction problem verification. Fully take advantages of ECA rules modeling and verification of timed automata. Firstly, this paper summarized the research status at home and abroad, on this basis, we summed up the lack of existing research and the direction to improvement. Then, the system model of ECA rules is defined, which is based on timed automata. The events of ECA rules are modeled as actions in timed automata, conditions modeled as defending formula, actions modeled as methods of directed edge, rule priority modeled as data variables, and time constraints modeled as clock variables. Next, the rule system interaction problem is converted to model validation problem based on timed automata. Through the establishment of rule schedule automata and rule execution automata, converting termination and inconsistency issues to corresponding safety and activity issues in the model validation of time automata. Meanwhile, the correctness problem is converted to reachability problem by modeling common patterns of requirements specification as corresponding models in time automata. These models can constitute a network of timed automata, depicting the running process of ECA rules system completely. The process performs as a state transition path. Finally, combined with a timed automata modeling validation tool namely UPPAAL, and intelligent assistance system of elderly people with dementia as an example, feasibility and validity of the method is verified.Research shows that timed automata can better portray related features of ECA rule system, which can also effectively find the potential interaction issues that among ECA rules, so as to help develop ECA rule system to some extent and provide an effective basis for improvement for developer. Experimental results show that this method has a certain theoretical and practical value.