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.

• CTL
• LTL
• QRE
• INCA
• GIL

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.