Promela |
Basic Statement |
assert |
NAME
assert -
for stating simple safety properties.
SYNTAX
assert( expr )
EXECUTABILITY
true
EFFECT
none
DESCRIPTION
An
assert statement is similar to
skip in the sense that it is always executable
and has no other effect on the state of the system
than to change the local control state of the process that executes it.
A very desirable side effect of the execution of this statement is,
however, that it can trap violations of simple safety properties
during verification and simulation runs with Spin.
The assert statement takes any valid Promela expression as its argument. The expression is evaluated each time the statement is executed. If the expression evaluates to false (or, equivalently, to the integer value zero), an assertion violation is reported.
Assertion violations can be ignored in a verification run, by invoking the Spin generated verifier with run-time option -A , as in:
$ ./pan -A
EXAMPLES
The most common type of assertion statement is one that
contains just a simple boolean expression on global or
local variable values, for instance, as in:
assert(a > b)A second common use of the assertion is to mark locations in a proctype body that are required, or assumed, to be unreachable, as in:
assert(false)If the statement is reached nonetheless, it will be reported as an assertion violation. A statement of this type is comparable to the infamous
printf("this cannot happen\n");from C programs.
If more than one such assertion is needed, tracking can be made easier by using slight variations of expressions that necessarily will evaluate to false , such as:
assert(1+1 != 2) assert(1>2) assert(2>3)The assert statement can also be used to formalize general system invariants, that is, boolean conditions that are required to be invariantly true in all reachable system states. To express this, we can place the system invariant in an independently executed process, as in:
active proctype monitor() { assert(invariant) }where the name of the proctype is immaterial. Since the process instance is executed independently from the rest of the system, the assertion may be evaluated at any time: immediately after process instantiation in the initial system state, or at any time later in the system execution.
Several observations can be made about this example. First note that the process of type monitor has two states, and that the transition from the first to the second state is always unconditionally executable. This means that during verifications the addition of this specific form of the monitor process will double the size of the reachable state space. We can avoid this doubling by restricting the execution of the assertion to only those cases where it could actually lead to the detection of an assertion violation, for instance, as follows:
active proctype monitor() { atomic { !invariant -> assert(false) } }This also solves another problem with the first version. Note that if our model contains a timeout condition, then the first monitor process would always be forced to execute the assertion before the system variable timeout variable could be set to true. This would mean that the assertion could never be checked beyond the first firing of a timeout . The second version of the monitor does not have this problem.
NOTES
A simulation, instead of a verification, will not necessarily
prove that a safety property expressed with an
assert statement
is valid, because it will check its validity on just a randomly
chosen execution.
Note that placing a system invariant assertion inside a loop, as in
active proctype wrong() { do :: assert(invariant) od }still cannot guarantee that a simulation would check the assertion at every step. Recall that the fact that a statement can be executed at every step does not guarantee that it also will be executed in that way. One way to accomplish a tighter connection between program steps and assertion checks is to use a one-state never claim, for instance, as in:
never { do :: assert(invariant) od }This is an acceptable alternative in verifications, but since never claims are ignored in simulation runs, it would make it impossible to detect the assertion violation during simulations.
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |