Constrained Chain Property Patterns
Constrained Chain Property Patterns
Intent
To describe a variant of response and precedence chain
patterns that restrict user specified events from occurring
between pairs of states/events in the chain sequences.
Consecutive pairs of states/events in chain sequences are
refered to as links. This pattern allows specification of
the absence of states/events from individual links.
Example Mappings
This variant of chain patterns can be applied to any kind of
response or precedence chain. Here we illustrate mappings for
the constrained 1-2 response chain.
Examples and Known Uses
Constrained chain patterns are surprisingly useful. Some of our recent
work with model checking of GUI software used CTL mappings for
constrained 1-2 response patterns with global scope
(e.g., AG(P -> AF(S & !Z & AX(A[!Z U T])))).
In the following, user indicates that the user is allowed
to interact with the GUI, select, print, help, ok, ... are interactions
that the user can perform, and error, address are system responses.
- When a system error message is displayed the only allowable action is
user acknowledgement via the 'ok' button.
AG(error -> AF(user & !(print | help | ...) &
AX(A[!(print | help | ...) U ok])))
- When the user selects a customer the address information is displayed
before the user is allowed another interaction .
AG(select -> AF(!user & AX(A[!user U address])))
The latter example had !user filling the role of both
S and !Z in the mapping and it was simplified.
Constraining Other Chain Mappings
Introducing constraints into mappings for chain links depends on
the formalism and scope of the mapping.
In LTL or CTL with global and after scopes, the future operators (i.e.,
<>X in LTL and AF(X) in CTL) can be expanded
to their until equivalents (i.e., true U X in LTL and
A[true U X]), then the true can be replaced by the
negation of the constraining formula.
In LTL or CTL with before, between, and after-until scopes, untils
are used for expressing each link and these can be selectively
constrained by conjoining the negation of the constraining
formula on the left of the until operator.
In QREs for all scopes, the interval between link endpoints
is expressed with a [- ...] operator. Adding the constraining
formula as an argument of this operator achieves the link constraint.
Relationships
Aside from the obvious relationship with the
Chain patterns, constrained
chains are similar to
Absence patterns in the sense
that each link constraint is like a small absence pattern (with a
between scope).
This is an Order pattern.