+++ /dev/null
-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).
projects / lttv.git / blobdiff