We were able to extend five of the nine patterns:
[ Absence ] [ Existence ] [ Universality ] [ Precedence ] [ Response ]
For each of the five scopes, we list four formulas corresponding to
the four combinations of state based and edge based conditions and interval
bounds we have considered:
0. K, N - states,
L, M - states;
1. K, N - states,
L, M - up edges;
2. K, N - up edges, L,
M - states;
3. K, N - up edges, L,
M - up edges;
Combination 0 corresponds to the original formulation made by Matthew
B. Dwyer, George S. Avrunin, and James C. Corbett.
(Property
Specification Patterns for Finite state Verification) , where all of
K,
L, M and N are state based. The remaining three combinations
are our extensions to the pattern system. We assume that multiple events
can happen simultaneously, but only consider closed-left, open-right intervals,
as in the original system.
Also, we consider events K and N to be exclusive in the
Precedence
pattern and inclusive in the Response pattern. We note, however,
that it is perfectly possible to have formulas for all other combinations
of interval bounds. Down edges can be substituted for up edges without
changing the formulas. We have modified several of the 0-formulas (i.e,
state based conditions and intervals) from their original formulation to
remove assumptions of interleaving and make them consistent with the closed-left,
open-right intervals. Note that in the case of the
Universality pattern,
we do not list formulas for edge based events as edges cannot be universally
present