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.
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.