Promela Reference -- assert(4)

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:

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:

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: If the statement is reached nonetheless, it will be reported as an assertion violation. A statement of this type is comparable to the infamous 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:

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

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

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

SEE ALSO
ltl
never
timeout
trace


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)