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.
Event-condition-action (ECA) [
Termination, guaranteeing that the system does not remain “busy” internally
forever without responding to external events, and confluence , ensuring that any
possible interleaving of a set of triggered rules yields the same final result, are
fundamental correctness properties. While termination has been studied extensively
and many algorithms have been proposed to verify it, confluence is particularly
challenging due to a potentially large number of rule interleavings [
Researchers began studying these properties for active databases in the early
90’s [
To overcome these limitations, dynamic analysis approaches using model
checking tools such as SMV [
Our approach transforms a set of ECA rules into a PN, then dynamically
verifies termination and confluence and, if errors are found, provides concrete
counterexamples to help debugging. It uses our tool SmArT, which supports PNs
with priorities to easily model ECA rules with priorities. Moreover, a single
PN can naturally describe both the ECA rules as well as their nondeterministic
concurrent environment and, while our MDD-based symbolic model-checking
algorithms [
The rest of the paper is organized as follows: Sect. 2 recalls Petri nets; Sect. 3 introduces our syntax for ECA rules; Sect. 4 describes the transformation of ECA rules into a Petri net; Sect. 5 presents algorithms for termination and confluence; Sect. 6 shows experimental results; Sect. 7 concludes.
As an intermediate step in our approach, we translate a set of ECA rules into a
self-modifying Petri net [
The PN defines a discrete-state model (Spot, Sinit, A, {N t : t ∈ A} ). The potential state space is Spot = NP (in practice we assume that the reachable set of markings is finite or, equivalently, that there is a finite bound on the number of tokens in each place, but we do not require to know this bound a priori). Sinit ⊆ Spot is the set of initial states, { xinit} in our case (assuming an arbitrary finite initial set of markings is not a problem). The set of (asynchronous) model events is A = T . The next-state function for transition t is Nt, such that Nt(m) = { m0} , where m0 is as denfied above if transition t is enabled in marking m, and Nt(m) = ∅ otherwise. Thus, the next-state function for a particular PN transition is deterministic, although the overall behavior remains nondeterministic due to the choice of which transition should fire when multiple transitions are enabled. 3
ECA rules have the format “ on events if condition do actions.” If the events
are activated and the boolean condition is satisfied, the rule is triggered and its
actions will be performed. In active DBMSs, events are normally produced by
explicit database operations such as insert and delete [
= rel_op := ≥ | ≤ | assignment := env_var into loc_var [, assignment] “ /” is integer division “ number” is a constant ∈ N ext_ev_decl := external ext_ev [ activated when env_var rel_op number ] [ read (assignment) ] int_ev_decl := internal int_ev ext_evs := ext_ev | (ext_evs or ext_evs) | (ext_evs and ext_evs) int_evs := int_ev | (int_evs or int_evs) | (int_evs and int_evs) condition := (condition or condition) | (condition and condition) |
not condition | exp rel_op exp action := increase (loc_var, exp) | decrease (loc_var, exp) |
set (loc_var, exp) | activate (int_ev) actions := action | (actions seq actions) | (actions par actions) ext_rule := on ext_evs [if condition] do actions int_rule := on int_evs [if condition] do actions [with priority number] system := [env_vars]+[loc_vars]∗ [ext_ev_decl]+[int_ev_decl]∗ [ext_rule]+[int_rule]∗
Environmental variables are used to represent environment states that can only be measured by sensors but not directly modified by the system. For instance, if we want to increase the temperature in a room, the system may choose to turn on a heater, eventually achieving the desired effect, but it cannot directly change the value of the temperature variable. Thus, environmental variables capture the nondeterminism introduced by the environment, beyond the control of the system. Instead, local variables can be both read and written by the system. These may be associated with an actuator, a record value, or an intermediate value describing part of the system state; we provide operations to set (absolute change) their value to an expression, or increase or decrease (relative change) it by an expression; these expressions may depend on environmental variables.
Events can be combinations of atomic events activated by environmental or internal changes. We classify them using the keywords external and internal. An external event can be activated when the value of an environmental variable crosses a threshold; at that time, it may take a snapshot of some environmental variables and read them into local variables to record their current values. Only the action of an ECA rule can instead activate internal events. Internal events are useful to express internal changes or required actions within the system. These two types of events cannot be mixed within a single ECA rule. Thus, rules are external or internal, respectively. Then, we say that a state is stable if only external events can occur in it, unstable if actions of external or internal rules are being performed (including the activation of internal events, which may then trigger internal rules). The system is initially stable and, after some external events trigger one or more external rules, it transitions to unstable states where internal events may be activated, triggering further internal rules. When all actions complete, the system is again in a stable state, waiting for environmental changes that will eventually trigger external events.
The condition portion of an ECA rule is a boolean expression on the value of environmental and local variables; it can be omitted if it is the constant true.
The last portion of a rule specifies which actions must be performed, and in which order. Most actions are operations on local variables which do not directly affect environmental variables, but may cause some changes that will conceivably be reflected in their future values. Thus, all environmental variables are readonly from the perspective of an action. Actions can also activate internal events. Moreover, to handle complex action operations, the execution semantics can be specified as any partial order described by a series-parallel graph; this is obtained through an appropriate nesting of seq operators, to force a sequential execution, and par operators, to allow an arbitrary concurrency. The keyword with priority enforces a priority for internal rules. If no priority is specified, the default priority of an internal rule is 1, the same as that of external rules.
We now discuss the choices of execution semantics for our language, to
support the modeling of reactive systems. The first choice is how to couple the
checking of events and conditions for our ECA rules. There are (at least) two
options: immediate and deferred. The event-condition checking is immediate if
the corresponding condition is immediately evaluated when the events occur,
it is deferred if the condition is evaluated at the end of a cycle with a
predefined frequency. One critical requirement for the design of reactive systems is
that the system should respond to external events from the environment [
Another important choice is how to handle and model the concurrent and nondeterministic nature of reactive systems. We introduce the concept of batch for external events, similar to the concept of transaction in DBMSs. Formally, the boundary of a batch of external events is defined as the end of the execution of all triggered rules. Then, the system starts to receive external events and immediately evaluates the corresponding conditions. The occurrence of an external event closes a batch if it triggers one or more ECA rules; otherwise, the event is added to the current batch. Once the batch closes and the rules to be triggered have been determined, the events in the current batch are cleaned-up, to prevent multiple (and erroneous) triggerings of rules. For example, consider ECA rules ra: “ on a do · · · ” and rac: “ on (a and c) do · · · ”, and assume that the system finishes processing the last batch of events and is ready to receive external events for the next batch. If external events occur in the sequence “ c, a, . . .”, event c alone cannot trigger any rule so it begins, but does not complete, the current batch. Then, event a triggers both rule ra and rac, and thus, closes the current batch. Both rules are triggered and will be executed concurrently. This example shows how, when the system is in a stable state, the occurrence of a single external event may trigger one or more ECA rules, since there is no “contention” within a batch on “using” an external event: rule ra and rac share event a and both rules are triggered and executed. If instead the sequence of events is “ a, c, . . .”, event a by itself constitutes a batch, as it triggers rule ra. This event is then discarded by the clean-up so, after executing ra and any internal rule (recursively) triggered by it, the system returns to a stable state and the subsequent events “ c, . . .” begin the next batch. Under this semantic, all external events in one batch are processed concurrently. Thus, unless there is a termination error, the system will process all triggered rules, including those triggered by the activation of internal events during the current batch, before considering new external events. This batch definition provides maximum nondeterminism on event order, which is useful to discover design errors in a set of ECA rules.
We also stress that, in our semantics, the system is frozen during rule execution and does not respond to external events. Thus, rule execution is instantaneous, while in reality it obviously requires some time. However, from a verification perspective, environmental changes and external event occurrences are nondeterministic and asynchronous, thus our semantic allows the verification process to explore all possible combinations without missing errors due to the order in which events occur and environmental variables change. 3.1
We now illustrate the expressiveness of our ECA rules on a running example: a light control subsystem in a smart home for senior housing. Fig. 2 lists the requirements in plain English (R1 to R5). Using motion and pressure sensors, the system attempts to reduce energy consumption by turning off the lights in unoccupied rooms or if the occupant is asleep. Passive sensors emit signals when an environmental variable value crosses a significant threshold. The motion sensor measure is expressed by the boolean environmental variable Mtn. The system also provides automatic adjustment for indoor light intensity based on an outdoor light sensor, whose measure is expressed by the environmental variable ExtLgt ∈ { 0, ..., 10} . A pressure sensor detects whether the person is asleep and is expressed by the boolean environmental variable Slp. environmental Mtn, ExtLgt, Slp
local lMtn, lExtLgt, lSlp, lgtsTmr, intLgts external SecElp read (Mtn into lMtn, ExtLgt into lExtLgt, Slp into lSlp) MtnOn activated when Mtn = 1 MtnOff activated when Mtn = 0 ExtLgtLow activated when ExtLgt ≤ 5
LgtsOff, LgtsOn, ChkExtLgt, ChkMtn, ChkSlp internal (R1) When the room is unoccupied for 6 minutes, turn off lights if they are on. r1 on MtnOff if (intLgts > 0 and lgtsTmr = 0) do set (lgtsTmr, 1) on SecElp if (lgtsTmr ≥ 1 and lMtn = 0) r2 do increase (lgtsTmr, 1)
on SecElp if (lgtsTmr = 360 and lMtn = 0) r3 do ( set (lgtsTmr, 0) par activate (LgtsOff ) )
on LgtsOff do ( set (intLgts, 0) par activate (ChkExtLgt) ) r4 (R2) When lights are off, if external light intensity is below 5, turn on lights.
on ChkExtLgt if (intLgts = 0 and lExtLgt ≤ 5) r5 do activate (LgtsOn) (R3) When lights are on, if the room is empty or a person is asleep, turn off lights. r6 on LgtsOn do ( set (intLgts, 6) seq activate (ChkMtn) )
on ChkMtn if (lSlp = 1 or (lMtn = 0 and intLgts ≥ 1) ) r7 do activate (LgtsOff ) (R4) If the external light intensity drops below 5, check if the person is asleep and set the lights intensity to 6. If the person is asleep, turn off the lights. r8 on ExtLgtLow do ( set (intLgts, 6) par activate (ChkSlp) ) r9 on ChkSlp if (lSlp = 1) do set (intLgts, 0) (R5) If the room is occupied, set the lights intensity to 4.
r10 on MtnOn do ( set (intLgts, 4) par set (lgtsTmr, 0) )
MtnOn, MtnOff , and ExtLgtLow are external events activated by the environmental variables discussed above. MtnOn and MtnOff occur when Mtn changes from 0 to 1 or from 1 to 0, respectively. ExtLgtLow occurs when ExtLgt drops below 6. External event SecElp models the system clock, occurs every second, and takes a snapshot of the environmental variables into local variables lMtn, lExtLgt, and lSlp, respectively. Additional local variables lgtsTmr and intLgts are used. Variable lgtsTmr is a timer for R1, to convert the continuous condition “the room is unoccupied for 6 minutes” into 360 discretized SecElps events. Rule r1 initializes lgtsTmr to 1 whenever the motion sensor detects no motion and the lights are on. The timer then increases as second elapses, provided that no motion is detected (rule r2). If the timer reaches 360, internal event LgtsOff is activated to turn off the lights and to reset lgtsTmr to 0 (rule r3). Variable intLgts acts as an actuator control to adjust the internal light intensity.
Our ECA rules contain internal events to model internal system actions or checks not observable from the outside. LgtsOff , activated by rule r3 or r7, turns the lights off and activates another check on outdoor light intensity through internal event ChkExtLgt (rule r4). ChkExtLgt activates LgtsOn if lExtLgt ≤ 5
EnvMotOn 0 if(tk(MtnOn)=0)
MtnOn (rule r5). ChkSlp is activated by rule r8 to check whether a person is asleep. If true, the event triggers an action that turns the lights off (rule r9). Internal event ChkMtn, activated by rule r6, activates LgtsOff if the room is unoccupied and all lights are on, or if the room is occupied but the occupant is asleep (rule r7). 4
We now explain the procedure to transform a set of ECA rules into a PN. First, we put each ECA rule into a regular form where both events and condition are disjunctions of conjunctions of events and relational expressions, respectively. All rules in Fig. 2 are in this form. While this transformation may in principle cause the expressions for events and conditions to grow exponentially large, each ECA rule usually contains a small number of events and conditions, hence this is not a problem in practice. Based on the immediate event-condition checking assumption, a rule is triggered iff “ trigger ≡ events ∧ condition” holds.
Next, we map variables and events into places, and use PN transitions to model event testing, condition evaluation, and action execution. Any change of variable values is achieved through input and output arcs with appropriate cardinalities. Additional control places and transitions allow the PN behavior to be organized into “phases”, as shown next. ECA rules r1 through r10 of Fig. 2 are transformed into the PN of Fig. 3 (dotted transitions and places are duplicated and arcs labeled “ if (cond)” are present only if cond holds). 4.1
This phase models the occurrence of external events, due to environment changes over which the system has no control. The PN firing semantics perfectly matches the nondeterministic asynchronous nature of these changes. For example, in Fig. 3, transitions EnvMotOn and EnvMotOff can add or remove the token in place Mtn, to nondeterministically model the presence or absence of people in the room (the inhibitor arc from place Mtn back to transition EnvMotOn ensures that at most one token resides in Mtn). Firing these environmental transitions might nondeterministically enable the corresponding external events. Here, firing EnvMotOn generates the external event MtnOn by placing a token in the place of the same name, while firing EnvMotOff generates event MtnOff , consistent with the change in Mtn. To ensure that environmental transitions only fire if the system is in a stable state (when no rule is being processed) we assign the lowest priority, 0, to these transitions. As the system does not directly affect environmental variables, rule execution does not modify them. However, we can take snapshots of these variables by copying the current number of tokens into their corresponding local variables using marking-dependent arcs. For example, transition EnvSecElp has an output arc to generate event SecElp, and arcs connected to local variables to perform the snapshots, e.g., all tokens in lMtn are removed by a reset arc (an input arc that removes all tokens from its place), while the output arc with cardinality tk(Mtn) copies the value of Mtn into lMtn. 4.2
This phase starts when trigger ≡ events ∧ condition holds for at least one external ECA rule. If, for rule rk, events and condition consist of nd and nc disjuncts, respectively, we define nd · nc test transitions rkTsti,j with priority P + 2, where i and j are the index of a conjunct in events and one in condition, while P ≥ 1 is the highest priority used for internal rules (in our example, all internal rules have default priority P = 1). Then, to trigger rule rk, only one of these transitions, e.g., r7Tst1,1 or r7Tst1,2, needs to be fired (we omit i and j if nd = nc = 1). Firing a test transition means that the corresponding events and conditions are satisfied and results in placing a token in each of the triggered places rkTrg1, . . . , rkTrgN , to indicate that Rule rk is triggered, where N is the number of outermost parallel actions (recall that par and seq model parallel and sequential actions). Thus, N = 1 if rk contains only one action, or an outermost sequential series of actions. Inhibitor arcs from rkTrg1 to test transitions rkT sti,j ensure that, even if multiple conjuncts are satisfied, only one test transition rfies. The firing of test transitions does not “consume” external events, thus we use double-headed arrows between them. This allows one batch to trigger multiple rules, conceptually “at the same time.” After all enabled test transitions for external rules have fired, place Ready contains one token, indicating that the current batch of external events can be cleared: transition CleanUp, with priority P + 1, fires and removes all tokens from external and internal event places using reset arcs, since all the rules that can be triggered have been marked. This ends the triggering phase and closes the current batch of events. 4.3
This phase executes all actions of external rules marked in the previous phase. It may further result in triggering and executing internal rules. Transitions in this phase correspond to the actions of rules with priority in [1, P ], the same as that of the corresponding rule. An action activates an internal event by adding a token to its place. This token is consumed as soon as a test transition of any internal rule related to this event fires. This is different from the way external rules “use” external events. Internal events not consumed in this phase are cleared when transition CleanUp fires in the next batch. When all enabled transitions of the performing phase have fired, the system is in a stable state where environmental changes (transitions with priority 0) can again happen and the next batch starts. 4.4
The algorithm in Fig. 4 takes external and internal ECA rules Rext, Rint, with
priorities in [1, P ], environmental and local variables Venv, Vloc, and external
and internal events Eext, Eint, and generates a PN. After normalizing the rules
and setting P to the highest priority among the rule priorities in Rint, it maps
environmental variables Venv, local variables Vloc, external events Eext, and
internal events Eint, into the corresponding places (Lines 5, 6, and 8). Then, it
creates phase control place Ready, transition CleanUp, and reset arcs for CleanUp
(Lines 4-5). We use arcs with marking-dependent cardinalities to model
expressions. For example, together with inhibitor arcs, these arcs ensure that each
variable v ∈ Venv remains in its range [vmin, vmax] (Lines 8-10). These arcs also
model the activated when portion of external events (Line 17), rule
conditions (Line 33), and assignments of environmental variables to local variables
(Lines 19-20 and lines 14-15). The algorithm models external events and
environmental changes (Lines 11-24); it connects environmental transitions such as
tvInc and tvDec to their corresponding external event places, if any, with an arc
TransformECAintoPN (Rext, Rint, Venv, Vloc, Eext, Eint)
1 normalize Rext and Rint into regular form and set P to the highest rule priority
2 create a place Ready • to control “phases” of the net
3 create transition CleanUp with priority P +1 and Ready − [
Next, rules are considered (Lines 25-40). A rule with nd event disjuncts and
nc condition disjuncts generates nd · nc testing transitions. To model the
parallelsequential action graph of a rule, we use mutually recursive procedures (Fig. 5
and Fig. 6). Procedure SeqSubGraph first tests all atomic actions, such as “set”,
ParSubGraph(Pars, Pre, p) • Pars: parallel actions, Pre: prefix
1 for each l ∈ { 1, 2} do • according to the syntax Pars2 has two components
2 create place PreActlTrglSeql and transition PreActl w/priority p
3 create Pre − [
The first step towards verifying correctness properties is to define Sinit, the set
of initial states, corresponding to all the possible initial combinations of system
variables (e.g., ExtLgt can initially have any value in [
To this end, we add an initialization phase that puts a nondeterministically chosen legal number of tokens in each place corresponding to an environmental variable. This phase is described by a subnet consisting of a transition InitEnd InitEnd 4
Init
InitExtLgt 4
InitSlp 4 InitMtn 4 10 with priority P + 3, a place Init with one initial token, and an initializing transition with priority P +3 for every environmental variable, to initialize the number of tokens in the corresponding place. Fig. 7 shows this subnet for our running example. We initialize the Petri net by assigning the minimum number of tokens to every environmental variable place and leaving all other places empty, then we let the initializing transitions nondeterministically add a token at a time, possibly up to the maximum legal number of tokens in each corresponding place. When InitEnd fires, it disables the initializing transitions, freezes the nondeterministic choices, and starts the system’s normal execution.
This builds the set of initial states, ensuring that the PN will explore all possible initial states, and avoids the overhead of manually starting the PN from one legal initial marking at a time. Even though the overall state space might be larger (it equals the union of all the state spaces that would be built starting from each individual marking), this is normally not the case, and, anyway, having to perform just one state space generation is obviously enormously better.
After the initialization step, we proceed with verifying termination and
confluence using our tool SmArT, which provides symbolic reachability analysis and
CTL model checking with counterexample generation [
A set G of ECA rules satisfies termination if no infinite sequence of internal events can be triggered in any possible execution of G. This can be expressed in CTL as ¬ EF(EG(unstable)), stating that there is no cycle of unstable states reachable from an initial, thus stable, state.
Both traditional breadth-first-search (BFS) and saturation-based [
A set G of ECA rules satisfying termination also satisfies confluence if, for any legal batch b of external events and starting from any particular stable state s, the system eventually reaches a unique stable state.
We stress that what constitutes a legal batch b of events depends on state s,
since the condition portion of one or more rules might affect whether b (or
a subset of b) can trigger a rule (thus close a batch). Given a legal batch b
occurring in stable state s, the system satisfies confluence if it progresses from s
by traversing some (nondeterministically chosen) sequence of unstable states,
eventually reaching a stable state uniquely determined by b and s. Checking
confluence is therefore expensive [
The brute force algorithm ConfExplicit in Fig. 9 enumerates unstable states
and generates reachable states only from unstable states using constrained
saturation [
Termination (time: sec, memory: MB) Model PN t PN c PN 1 PN 2 PN 3
PN 4 Model PN c PN 1 PN 2 PN 3 PN 4
|S rch| 9.665 9.497 states (all other unstable reachable states are by definition reachable from this frontier). However, we stress that these, as most symbolic algorithms, are heuristics, thus they are not guaranteed to work better than the simpler approaches.
Next, we introduce a fully symbolic algorithm to check confluence in Fig. 10.
It first generates the transition transitive closure (TC) set from Nint using
constrained saturation [
Table 1 reports results for a set of models run on an Intel Xeon 2.53GHz workstation with 36GB RAM under Linux. For each model, it shows the state space size (|S rch| ), the peak memory (Mp), and the final memory ( Mf ). For termination, it shows the time used to verify the property (Tt) and to find the shortest ... lgtsTmr = 1 r6Act1 r6Trg1= 1 lgtsTmr = 1 LgtsOn=1 r6Tst lgtsTmr = 1 r6Trg1Seq1= 1 intLgts = 6 lgtsTmr = 1 ChkMtn = 1 intLgts = 6 ... ... ... counterexample (Tc). For confluence, it reports the best runtime between our two explicit algorithms (Tbe) and for our symbolic algorithm (Ts). Memory consumption accounts for both decision diagrams and operation caches.
Net PN t is the model corresponding to our running example, and fails the
termination check. Even though the state space is not very large,
counterexample generation is computationally expensive [
We then run SmArT on PN c to verify confluence, and found 72,644 bad states. Fig. 12 shows one of these unstable states, s0, reaching two stables states, s1 and s2. External event ExtLgtLow closes the batch in s0 and triggers rule r8, which sets intLgt to 6 and activates internal event ChkSlp, which in turn sets intLgt to 0 (we omit intermediate unstable states from s0 to s1 and to s2). We correct rules r8 and r9, replacing them with r0 : on ExtLgtLow if lSlp=0 8 do set (intLgt, 6) and r90: on ExtLgtLow if lSlp=1 do set (intLgt, 0); resulting in model PN fc. Checking this new model against for confluence, we find that the number of bad states decreases from 72,644 to 24,420. After investigation, we determine that the remaining problem is related to rules r2 and r3. After changing rule r1 to on SecElp if ((lgtsTmr ≥ 1 and lgtsTmr ≤ 359) and lMtn = 0) do increase (lgtsTmr, 1), the model passes the check. This demonstrates the effectiveness of counterexamples to help a designer debug a set of ECA rules.
We then turn our attention to larger models, which extend our original model
by introducing four additional rules and increasing variable ranges. In PN 1 and
PN 2, the external light variable ExtLgt ranges in [
Verifying termination and confluence of ECA rule bases for reactive systems is challenging due to their highly concurrent and nondeterministic nature. We proposed an approach to verify these properties using a self-modifying PN with inhibitor arcs and priorities. Our approach is general enough to give precise answers to questions about other properties, certainly those that can be expressed in CTL. As an application, we showed how a light control system can be captured by our approach, and we verified termination and conuflence for this model using SmArT. In the future, we would like to improve our approach in the following ways. The confluence algorithm must perform constrained state space generation starting from each unstable state, which is not efficient if Sunst is large. In that case, a simulation-based falsification approach might be more suitable, using intelligent heuristic sampling and searching strategies. However, this approach is sound only if the entire set Sunst is explored. Another direction to extend our work is the inclusion of abstraction techniques to reduce the size of the state space.
Work supported in part by UC-MEXUS under grant Verification of active rule bases using timed Petri nets and by the National Science Foundation under grant CCF-1018057.