Property Specification Pattern Notes

The patterns provided in this system cover a broad range of requirements for real systems. Your requirement, however, may require you to adapt existing patterns slightly to better express your intended property. There are a number of ways in which this variation can take place, e.g., parameterization of patterns, combination of patterns, and variation in pattern scopes.

Pattern Parameterization

Pattern mappings are presented in terms of place-holder symbols (e.g. P,Q,R,S) that are to be replaced by users when writing actual specifications. These place holders are filled with descriptions of specific system states or events of interest. These descriptions can be more complex than just a single proposition or event name. Here are a few typical examples:

For Logics (e.g., CTL, LTL)

Purely propositional formula can always be used to describe a state. This includes simple negations, disjunctions, conjunctions and implications.
State-formulae that include temporal operators can also be used (e.g., []!init responds to init globally would be
    [](init -> <>[]!init)
Care must be taken in using such state-formulae, since the meaning of the resulting specification can be quite subtle. This is especially true when using scopes that may have an end point, i.e., before, between and after-until. Consider a requirement that before the first shutdown state we would like it to be the case that requests are responded to. We know that a succesful response has the form:
    [](request -> <>respond)
and we might be tempted to use this as a parameter in a before-scope universality pattern. The resulting formula:
    <>shutdown -> (([](request -> <>respond)) U shutdown)
however, does not express the correct requirement. In particular the <> operator when embedded in the scope does not take into account the fact that the search for respond should terminate upon encountering shutdown. One can modify this by expanding the <> to its until form, e.g., true U respond, then requiring that throughout the search the shutdown is absent (this is similar to the constrained response discussed below). The resulting formula is:
    <>shutdown -> (([](request -> (!shutdown U respond))) U shutdown)

For QREs

Each portion of a specification "matches" some portion of program behavior. This "matching", which is inherent to an automata based specification model, means that a portion of input is consumed for each portion of a specification. This has some implications for the way's that patterns can be parameterized.

Choice among a collection of events (e.g., disjunction) can be handled relatively simply by using symbol classes (e.g., [x,y,z]).
Requiring a sequence of events is also simple (e.g., x;y;z), although such a sequence implies that there are no intervening events in the sequence.
Notions of conjunction (i.e. having all of a collection of events occur) are significantly more complex to specify. In this case it is necessary to explicitly describe the possible orderings of the constituent events (e.g., x;y, y;x). The same caveat about intervening events holds here as well.
Given the "matching" as consumption model of QREs, it is not possible to "look ahead" in the computation to formulate descriptions of certain points in the execution (e.g., as the lookahead for r in the LTL formula <>r -> !q U r does).

Pattern Combinations

A system's specification usually consists of a collection of property specifications.

Conjunctions

It is most often the case that all such property specifications should hold. In this case, one could simply check all specifications individually and require that all are successful. For the logical formalisms, an alternative is to conjoin the individual specifications into a single larger specification. While this is semantically equivalent, it may be the case that a larger specification is less efficient to verify (e.g., the cost of LTL to Buchi automaton construction can be large for automata-based model checkers). For this reason, preserving, and verifing, the individual property specifications is suggested.

Disjunctions

There are two views of a pair (or more generally a collection) of alternative individual property specifications:

system behaviors all correspond to one specification or they all correspond to the other specification
some of the system behaviors correspond to one specification and the rest of the behaviors correspond to the other specification

The first of these alternatives corresponds to the checking of individual property specifications independently and disjoining the results. This is true for all specification formalisms. The latter situation can be achieved in formalisms that allow specifications to be disjoined under the same universal path quantifier.

For LTL and QREs there is an implicit outer universal path quantifier, thus checking of a top-level disjunction of specifications will achieve these semantics. To achieve the first alternative (above) one must check LTL and QRE specifications separately.

This is not the case for CTL, where two specifications cannot be disjoined directly under the same path quantifier. A top-level disjunction CTL achieves the first alternative and the second cannot be achieved directly (although one might be able to rewrite a combined version of the two specifications).

Scope Variations

Most event-based formalisms use some version of an interleaved model of concurrent computation. In such formalisms, two events cannot coincide. Event-delimited scopes are thus open at both ends: an event that occurs within the scope cannot occur at the same time as an event that marks the beginning or end of the scope. For state-based formalisms, the situation is different. Consider, for instance, a scope that begins with a state in which proposition Q holds and ends with the next state in which R holds. If we want to specify that proposition P does not hold within this scope, we have to decide what should happen if P is true at either of the states marking the endpoints of the scope.

We have chosen to define scopes for state-based formalisms that include the state marking the beginning of the scope but do not include the state marking the end of the scope. Thus, for example, the LTL version of this specification would be
[]((Q & o<>R) -> (!P & o((!P) U (R | [](!P)))))
which requires that P be false in the state where Q holds but does not require P to be false when R becomes true. We chose these closed-left/open-right scopes because they are relatively easy to encode in specifications and beacuse they work for the real property specifications we studied.

It isn't very hard, however, to modify the mappings to open the scope on the left or close it on the right. An LTL specification of the "P is absent between Q and R" property with a scope that is open on the left would simply remove the first !P:
[]((Q & o<>R) -> (o((!P) U (R | [](!P)))))
allowing P to hold at the state marking the beginning of the scope. Similarly, to close the scope on the right, we have to require !P to hold until a state in which both R and !P are true:
[]((Q & o<>R) -> (!P & o((!P) U ((R & (!P))| [](!P)))))

Similar modifications can be made to adjust all the mappings for the various versions of the scopes.

Constrained Order Patterns

Order related patterns describe sequencing relationships between specified states or events. It is sometimes the case that one wishes to specify not only the sequencing relationship, but that the region between the states or events in that relationship is free of some other events. We provide constrained chain patterns to address this issue for precedence and response chains.

The plain response pattern also has a constrained variation. For example, one can restrict Z from the region between P and the S that responds to it in LTL, but converting the <> to its U equivalent then embedding !Z in its left operand. The global response mapping:

[](P -> <>S)

becomes:

[](P -> (true U S))

and finally:

[](P -> (!Z U S))

A similar transformation to the <> in the after scope can be applied. The before, between and after-until scope versions of the LTL response mappings already unfold the <> to its U form. In these cases, one need only embed the !Z in the proper place (which is identified by looking for the S appearing as the right operand of the U). For example, the between response mapping :

[]((Q & <>R) -> (P -> (!R U S)) U R)

becomes:

[]((Q & <>R) -> (P -> ((!R & !Z) U S)) U R)

Modifications for mappings in other formalisms can be applied as well. Global and between scope versions of constrained response in CTL are:

AG(P -> A[!Z U S])

AG(Q -> !E[!R U (P & !R & (E[!S U R] | E[Z U S]))])

The global version mirrors the LTL modifications. The between scope version is different because the CTL spec is expressed in terms of the lack of a violating sequence. In this case, we must enumerate the possible violating sequences, i.e., a missing response E[!S U R] or the occurrence of a constrained state before the response E[Z U S].

Global and between scope versions of constrained response as QREs are:

[-P]*; (P; [-S,Z]*; S; [-P]*)*

[-Q]*; (Q; [-P,R]*; (P; [-S,R,Z]*; S; [-P,R]*)*; R; [-Q]*)*; (Q; [-R]*)?

Multiple propositions can embedded in the constraint by using conjunction in the logics and by listing multiple events in QREs.

It is important to note that constrained response is different from absence with a between scope. The latter, which in LTL is:

[]((Q & <>R) -> !P U R)

does not require the closing of the scope (which corresponds to the responding state).