Specifying Invariance Properties

Invariance properties can be specified in LTL as generic safety properties of the type [] p where p is a property of a system state.
    p must be a side-effect-free expression that can be evaluated to true or false in any given system state. If p is an integer expression, the value zero is interpreted as false and any non-zero value is interpreted as true.


An efficient general method to specify an invariant property is to define a never claim of the following form:
	never { do :: assert(p) od }
An easy alternative is also to generate the never claim from the negated LTL property ![]p. The resulting never claim would then be equivalent to the following:
	never { do :: !p -> break :: true od }
This time the violation is caught when the end of the claim is reached, so instead of an assertion violation the error will now be reported as a match of the claim, but the result is the same.

If a never claim is already being used to check another property, which cannot easily be extended with the invariant check, an easy alternative is to add a special purpose invariant checking process to the model, as follows.

	active proctype invariant() { atomic { !p -> assert(p) } }
Note that, similar to the pattern used in the second never claim, this process cannot terminate unless the assertion can indeed fail.

The best method would be to avoid the addition of either a never claim or a user-defined process but to simply extend the existing model with process level assertions that are placed immediately following only those statements in the model that could in principle cause a violation of the invariant (e.g., after every statement that modifies a variable that is referenced in the invariant property).


There are several alternative methods to define invariant properties, but they are usually less efficient than the few we mentioned above. Consider, for instance, the following definition of an invariant process:
	active proctype invariant() { do :: assert(p) od }
The disadvantage of this method is that the presence of an invariant process of this type will have the effect that the system as a whole can no longer deadlock: there is always one transition left to execute. This also means that the special predefined boolean variable timeout can no longer become true at any system state.

We could avoid the latter problem by removing the do-loop and use the following simple form:

	active proctype invariant() { assert(p) }
This works correctly, but it now causes the verifier to explore two transitions for every reachable state, instead of one: the evaluation of the presumably valid assertion and the subsequent death of the process, which can now terminate. This version, therefore, introduces more overhead than is necessary. There is one trick one can apply to avoid the death of the process, and with that the creation of additional system states, which is to create the invariant process as the first running process in the system. Because processes can only die in last-in-first out order, this would secure that the terminated invariant process cannot die and disappear until all other processes have died first.
Another problem with this version is though that it is not compatible with the use of timeouts in the model itself. Note that once the system comes to a stop (the point where a timeout becomes executable), the assertion will be executed before the timeout, and it cannot be checked after the timeout. So generally, these alternatives are best avoided.
Go to Spin Home Page July 17, 2004