convert from svn repository: remove tags directory

[lttv.git] / trunk / verif / Spin / Doc / Book.Ch6.add

An appendix to Chapter 6 of the book: some extra explanation on pid's
and on temporal claims.  Updated for Spin Version 2.0 - January 1995.

PROCESS IDs

In Spin 2.0 and later the never claim can refer to the control state
of any process, but not to their local variables.
This functionality is meant to be used for building correctness assertions
with never claims.  It should never be used for anything else.
An example is
	Receiver[pid]@place
where `place' the name of a label within `proctype Receiver,' and
`pid' is the value returned by the run statement that instantiated the
copy of the Receiver proctype that we are interested in.

There is a misleading suggestion in the book that says that you can
usually guess the `pid's.  Wiser is to always use the explicit value
returned by the `run()' statement that instantiated the proces.
Processes started with the `active' prefix obtain instantiation
numbers starting at value 1, in the order in which they appear in the
specification.  Each process also has a local variable _pid that
holds its own instantiation number.

SPECIFYING TEMPORAL CLAIMS

The body of a temporal claim is defined just like PROMELA proctype bodies.
This means that all control flow structures, such as if-fi selections,
do-od repetitions, and goto jumps, are allowed.
There is, however, one important difference:

	Every statement inside a temporal claim is (interpreted as) a condition.
	A never claim should therefore never contain statements that can
	have side-effects (assignments, communications, run-statements, etc.)

Temporal claims are used to express behaviors that are considered undesirable
or illegal.  We say that a temporal claim is `matched' if the undesirable
behavior can be realized, and thus the claim violated.

The recommended use of a temporal claim is in combination with acceptance labels.
There are two ways to `match' a temporal claim, depending on whether the
undesirable behavior defines a terminating or a cyclic execution sequence.

o A temporal claim is matched when it terminates (reaches its closing curly brace).
  That is, the claim can be violated if the closing curly brace of the PROMELA
  body of the claim is reachable for at least one execution sequence.

o For a cyclic execution sequence, the claim is matched only when an explicit
  acceptance cycle exists.  The acceptance labels within temporal claims
  are user defined, there are no defaults.  This means that in the absence of
  acceptance labels no cyclic behavior can be matched by a temporal claim.
  It also means that to check a cyclic temporal claim, acceptance labels should
  only occur within the claim and not elsewhere in the PROMELA code.


SEMANTICS

The normal system behavior of a PROMELA system is defined as the
`asynchronous product' of the behaviors of the individual processes.
Given an arbitrary system state, its successor states are obtained
in two steps.  In the first step all the executable (atomic) statements in the
individual processes are identified.  In the second step, each one of these
statements is executed.
Each single execution produces a successor state in the asynchronous product.
The complete system behavior is thus defined recursively and
represents all possible interleavings of the individual process behaviors.
Call this asynchronous product machine the `global machine'.

The addition of a temporal claim defines an additional `synchronous product'
of this global machine with the state machine that defines the temporal
claim.  Call the latter machine the `claim machine', and call the new
synchronous product the `labeled machine'.

Every state in the labeled machine is a pair (p,q) with p a state in the global
machine and q a state in the claim machine.  Every transition in the labeled
machine is similarly defined by a pair (r,s) with r a transition in the global
machine and s a transition in the claim machine.
In other words, every transition in the `synchronous' product is a joint move
of the global machine and the claim machine.
(By contrast, every transition in an `asynchronous' product would correspond
to a single transition in either the global machine or the claim machine, thus
interleaving transitions instead of combining them.)

Since all statements in the claim machine are boolean propositions, the second
half of the transition pair (r,s) is either true or false.
Call all transitions where this proposition is true `matching transitions'.
In a matching transition proposition s evaluates to true in state system state r.
Notice that the claim machine has at least one stop state E, the state
at the closing curly brace of the claim body.

The semantics of temporal claims can now be summed up as follows.

o If the labeled machine contains any sequence of matching transitions only,
  that connects its initial state with a state (p,E) for any p, the temporal
  claim can be matched by a terminating sequence (a correctness violation).

o If the labeled machine contains any cycle of matching transitions only, that
  passes through an acceptance state, the temporal claim can be matched by a
  cyclic sequence.


EXAMPLES

Listed below are the equivalent PROMELA definitions for the three basic
temporal properties defined by Zohar Manna & Amir Pnueli in
``Tools and Rules for the Practicing Verifier'' Stanford University,
Report STAN-CS-90-1321, July 1990, 34 pgs.

The following descriptions are quoted from Manna & Pnueli:

	``There are three classes of properties we [...] believe to cover
	the majority of properties one would ever wish to verify.''

	1. Invariance
	``An invariance property refers to an assertion p, and requires that p
	is an invariant over all the computations of a program P, i.e. all
	the states arising in a computation of P satisfy p.  In temporal
	logic notation, such properties are expressed by [] p, for a state
	formula p.''

	Corresponding Temporal Claim in PROMELA:
	never {
		do
		:: p
		:: !p -> break
		od
	}

	2. Response
	``A response property refers to two assertions p and q, and
	requires that every p-state (a state satisfying p) arising in
	a computation is eventually followed by a q-state.
	In temporal logic notation this is written as p -> <> q.''

	Corresponding Temporal Claim in PROMELA:
	never {
		do
		:: true
		:: p && !q -> break
		od;
	accept:
		do
		:: !q
		od
	}

	Note that using (!p || q) instead of `skip' would check only the
	first occurrence of p becoming true while q is false.
	The above formalization checks for all occurrences, also future ones.
	Strictly seen, therefore, the claim above uses a common interpretation
	of the formula, requiring it to hold always, or: [] { p -> <> q }

	3. Precedence
	``A simple precedence property refers to three assertions p, q, and r.
	It requires that any p-state initiates a q-interval (i.e. an interval
	all of whose states satisfy q) which, either runs to the end of the
	computation, or is terminated by an r-state.
	Such a property is useful to express the restriction that, following
	a certain condition, one future event will always be preceded by
	another future event.
	For example, it may express the property that, from the time a certain
	input has arrived, there will be an output before the next input.
	Note that this does not guarantee [require] that the output will actually
	be produced. It only guarantees [requires] that the next input (if any)
	will be preceded by an output.  In temporal logic, this property is
	expressed by p -> (q U r), using the unless operator (weak until) U.

	Corresponding Temporal Claim in PROMELA:

	never {
		do
		:: skip		/* to match any occurrence */
		:: p &&  q && !r -> break
		:: p && !q && !r -> goto error
		od;
		do
		::  q && !r
		:: !q && !r -> break
		od;
	error:	skip
	}

	Strictly again, this encodes: [] { p -> (q U r) }
	To match just the first occurence, replace skip with (!p || r).