Promela |
Declarator |
never |
NAME
never -
declaration of a temporal claim.
SYNTAX
never { sequence }
DESCRIPTION
A
never claim can be used to define system behavior that, for whatever
reason, is of special interest.
It is most commonly used to specify behavior that should never
happen.
The claim is defined as a series of propositions, or boolean
expressions, on the system state that must become true
in the sequence specified for the behavior of interest to be matched.
A never claim can be used to match either finite or infinite behaviors. Finite behavior is matched if the claim can reach its final state (that is, its closing curly brace). Infinite behavior is matched if the claim permits an $omega#-acceptance cycle. Never claims, therefore, can be used to verify both safety and liveness properties of a system.
Almost all Promela language constructs can be used inside a claim declaration. The only exceptions are those statements that can have a side effect on the system state. This means that a never claim may not contain assignment or message passing statements. Side effect free channel poll operations, and arbitrary condition statements are allowed.
Never claims can either be written by hand or they can be generated mechanically from LTL formula, see the manual page for ltl .
There is a small number of predefined variables and functions that may only be used inside never claims. They are defined in separate manual pages, named _last , enabled , np_ , pc_value , and remoterefs .
EXAMPLES
In effect, when a
never claim is present, the system and the claim execute in lockstep.
That is, we can think of system execution as always consisting of
a pair of transitions: one in the claim and one in the system, with
the second transition coming from any one of the active processes.
The claim automaton always executes first.
If the claim automaton does not have any executable transitions,
no further move is possible, and the search along this path stops.
The search will then backtrack so that other executions can be explored.
This means that we can easily use a never claim to define a search restriction; we do not necessarily have to use the claim only for the specification of correctness properties. For example, the claim
never /* [] p */ { do :: p od }would restrict system behavior to those states where property p holds.
We can also use a search restriction in combination with an LTL property. To prove, for instance, that the model satisfies LTL property <>q , we can use the never claim that is generated with the Spin command (using the negation of the property):
$ spin -f '!<> q'Using the generated claim in a verification run can help us find counterexamples to the property. If we want to exclude non-progress behaviors from the search for errors, we can extend the LTL formula with the corresponding restriction, as follows:
$ spin -f '!( ([]<> !np_) -> (<> q) )'Note that we must now include the restriction as a precondition before we take the negation. If we move the negation operator inwards, the above formula can be seen to be equivalent to:
$ spin -f '([]<> !np_) && ([] !q)'
Alternatively, if we wanted to restrict the search to only non-progress behaviors, we can negate the precondition and write:
$ spin -f '!( !([]<> !np_) -> (<> q) )'which can also be written as:
$ spin -f '(<>[] np_ && [] !q)'The claim automaton must be able to make its first transition, starting in its initial claim state, from the global initial system state of the model. This rule can sometimes have unexpected consequences, especially when remote referencing operations are used. Consider, for instance, the following $roman model: sup 1#
1. The example is from Rob Gerth.
byte aap; proctype noot() { mies: skip } init { aap = run noot() }with the never claim defined as follows:
never { do :: noot[aap]@mies -> break :: else od }The intent of this claim is to say that the process of type noot , with pid aap , cannot ever reach its state labeled mies . If this happened, the claim would reach its final state, and a violation would be flagged by the verifier. We can predict that this property is not satisfied, and when we run the verifier it will indeed report a counterexample, but the counterexample is created for a different reason.
In the initial system state the never claim is evaluated for the first time. In that state only the init process exists. To evaluate expression noot[aap]@mies the value of variable aap is determined, and it is found to be zero (since the variable was not assigned to yet, and still has its default initial value). The process with pid zero is the init process, which happens to be in its first state. The label mies also points to the first state, but of a process that has not been created yet. Accidentally, therefore, the evaluation of the remote reference expression yields true, and the claim terminates, triggering an error report. The simulator, finally, on replaying the error trail, will reveal the true nature of this error in the evaluation of the remote reference.
A correct version of the claim can be written as follows:
never { true; do :: noot[aap]@mies -> break :: else od }In this version we made sure that the remote reference expression is not evaluated until the process that is referred to exists (that is, after the first execution step in the init process is completed).
Note that it is not possible to shortcut this method by attempting the global declaration:
byte aap = run noot(); /* an invalid initializer */In this case, with only one process of type noot , we can also avoid using variable aap by using the shorter remote reference:
noot@miesTo translate an LTL formula into a never claim, we have to consider first whether the formula expresses a positive or a negative property. A positive property expresses a good behavior that we would like our system to have. A negative property expresses a bad behavior that we claim the system does not have. A never claim is normally only used to formalize negative properties (behaviors that should never happen), which means that positive properties must be negated before they are translated into a claim.
Suppose that the LTL formula <>[]p , with p a boolean expression, expresses a negative claim (that is, it is considered a correctness violation if there exists any execution sequence in which eventually p can remain true infinitely long). This can be written in a never claim as:
never { /* <>[]p */ do :: true /* after an arbitrarily long prefix */ :: p -> break /* p becomes true */ od; accept: do :: p /* and remains true forever after */ od }Note that in this case the claim does not terminate and also does not necessarily match all system behaviors. It is sufficient if it precisely captures all violations of our correctness requirement, and no more.
If the LTL formula expressed a positive property, we first have to invert it to the corresponding negative property. For instance, if we claim that immediately from the initial state forward the value of p remains true, the negation of that property is: ![]p which can be translated into a never claim. The requirement says that it is a violation if p does not always remain true.
never { /* ![]p = <>!p*/ do :: true :: !p -> break od }In this specification, we have used the implicit match of a claim upon reaching the final state of the automaton. Since the first violation of the property suffices to disprove it, we could also have written:
never { do :: !p -> break :: else od }or, if we abandon the correspondence with LTL and Buchi automata for a moment, even more tersely as:
never { do :: assert(p) od }
NOTES
It is good practice to confine the use of
accept labels to
never claims.
Spin automatically generates the
accept labels within the claim when it generates claims from LTL formulae on
run-time option
-f .
The behavior specified in a never claim is matched if the claim can terminate, that is, if execution can reach the closing curly brace of the claim body. In terms of Buchi acceptance, this means that in a search for liveness properties, the final state of the claim is interpreted as the implicit acceptance cycle:
accept_all: do :: true odThe dummy claim
never { true }therefore always matches, and reports a violation, after precisely one execution step of the system. If a never claim contains no accept labels, then a search for cycles with run-time option -a is unnecessary and the claim can be proven or disproven with a simple search for safety properties. When the verifier is used in breadth-first search mode, only safety properties can be proven, including those expressed by never claims.
SEE ALSO
_last
accept
assert
enabled
ltl
notrace
np_
pc_value
poll
progress
remoterefs
trace
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 4 May 2015) |