Symbolic verification of ECA rules.
Xiaoqing Jin, Yousra Lembachar, Gianfranco Ciardo · 2013
Abstract. Event-condition-action (ECA) rules specify a decision making process and are widely used in reactive systems and active database systems. Applying formal verification techniques to guarantee properties of the designed ECA rules is essential to help the error-prone procedure of collecting and translating expert knowledge. The nondeterministic and concurrent semantics of ECA rule execution enhance expressiveness but hinder analysis and verification. We then propose an approach to analyze the dynamic behavior of a set of ECA rules, by first translating them into an extended Petri net, then studying two fundamental correctness properties: termination and confluence. Our experimental results show that the symbolic algorithms we present greatly improve scalability.