FeaVer: Logic Properties

Temporal logic

The model checker that performed the verifications for the FeaVer system in the background (Spin) contains efficient on-the-fly search algorithms for omega regular properties. This broad class of properties includes all basic safety and liveness properties, and all those properties that can be specified in the linear temporal logic made famous by Amir Pnueli (←) and Leslie Lamport (→) in the late seventies and early eighties as the formalism of choice for reasoning about the behaviors of distributed systems.

A temporal logic formula is built from simple operand symbols, such as p and q, that are used to represent events or state conditions on the system being verified, and normal boolean operators such as logical negation "!", logical or "\/," logical and "/\," and logical implication "->." Round braces are used for grouping, as in (p /\ q). In addition, though, a temporal formula can also contain operators that allow us to claim a causal relation between events of between the existence of state conditions in time. There are three basic temporal operators that can be used for this purpose: the box operator "[]", which is pronounced "always," the diamond operator <>, pronounced "eventually," and the "until" operator U.

A sample temporal formula that contains all three temporal operators is:

	[] (p -> <> (q U r))
which means:
    It is "always" the case that whenever p holds this implies that "eventually" the condition q will hold and that it will hold at least "until" condition r holds as well.
Note in particular that if p never holds the formula is trivially satisfied, because (p -> s) by definition means (!p \/ s).

Test automata

Before the model checker Spin performs a verification task, it will first convert any temporal logic formula into a test automaton, which is then used directly in the actual model checking process. This means that the user also has the option to specify test automata directly, if this can simplify the task. The figure on the right gives an example of a property that was derived by Spin from a temporal formulae. To perform the model checking "test" itself this automata is interpreted in a special way. The model checker will search for all system executions that can traverse the red states infinitely often. Now clearly some of the states colored red in this figure cannot be traversed infinitely often, no matter what happens, because they are not contained in a cycle (see the two red states at the top of this figure). The other two could potentially be part of a cycle if the conditions on the edges in the cycle can be shown to hold in the proper sequence arbitrarily often. The existence of such an execution corresponds to the underlying temporal logic formulae to be satisfied. FeaVer uses this capability of Spin to trap property violations, by formulating all properties as undesired executions of the system: classes of behavior that one way or another break a required system property, such as valid feature behavior.

Time diagrams

A third, more informal but equivally effective, way of specifying properties is with the help of timing diagrams that list the particular sequence of events or conditions that we are interested in to verify systems behavior. We may, for instance, want to verify that some condition t (defined elsewhere) will inevitably occur each time that four other events or conditions have occured in a systems execution. If there is any possibility for t to not occur under these circumstances, this is considered to be a violation and we want the model checker to report an example of back to us. Optionally we can identify, possibly overlapping or nested, intervals in which certain constraints (c1 to c3 in the figure) are added on the executions of interest. A constraint could stipulate, for instance, the absence of specific sets of events or conditions. The occurence of events within the constraints is not considered an error, but merely an indication that we are not interested in those particular variants of executions in checking these properties.

In a call processing application, for instance, we could check the correct operation of a feature called Call Forwarding Don't Answer (CFDA) in this way. We define 2 events that always precede a critical 3rd. The first event is the arrival of a ring request from a remote switch, targeted to the local phone subscriber with the CFDA feature enabled. The second event is the occurrence of a timeout condition, which indicates that the subscriber did not answer the ring, and the critical 3rd event, that is now required to follow, is the forwarding message that hands of the call in accordance with the CFDA specification. Constraints can be used in this case to limit the types of executions to those in which the subscriber is never busy, and where the incoming call is never aborted by the caller before the timeout occurs.

Back to Main Page