Promela |
BasicStatements |
assert(4) |
NAME
assertion statement
-
for stating simple safety properties.
SYNTAX
assert(
expr )
EXECUTABILITY
True
EFFECT
None
DESCRIPTION
An
assert
statement is similar to the predefined condition statement
skip
in the sense that it is always executable
and has no other effect on the state of the system
than to change the 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 an expression as its argument. The expression is evaluated each time the statement is executed. If the expression evaluates to the boolean value false (or, equivalently, to the integer value zero), a violation of the correctness requirement is reported, but the system execution is not necessarily interrupted.
EXAMPLES
assert(a > b) assert(0)The second type of assert statement above is useful to mark a local state in a proctype that is required, or assumed, to be unreachable. If the statement is reached nonetheless, it will be reported as an assertion violation.
The assert statement can be used to formalize general system invariants, i.e., boolean conditions that are required to be invariantly true in all reachable system states. To express this, it suffices to 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.
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 }
would still not guarantee that a simulation would check the assertion
at every step, because the fact that a statement could be executed
at every step does not guarantee that it will be executed in that way.
One way to accomplish such a tight connection between program steps
and assertion checks would be to use a temporal claim instead
of an asynchronous process:
never { do :: assert(invariant) od }
Alas, this would not work for simulation either, because
temporal claims are not considered by Spin during random simulations.
Simulations are for debugging, not for verification.
SEE ALSO
skip(1), ltl(1), never(2).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |