trunk/verif/Spin/Doc/Book91_Ch6_add.txt

   1 An appendix to Chapter 6 of the book: some extra explanation on pid's
   2 and on temporal claims.  Updated for Spin Version 2.0 - January 1995.
   3
   4 PROCESS IDs
   5
   6 In Spin 2.0 and later the never claim can refer to the control state
   7 of any process, but not to their local variables.
   8 This functionality is meant to be used for building correctness assertions
   9 with never claims.  It should never be used for anything else.
  10 An example is
  11         Receiver[pid]@place
  12 where `place' the name of a label within `proctype Receiver,' and
  13 `pid' is the value returned by the run statement that instantiated the
  14 copy of the Receiver proctype that we are interested in.
  15
  16 There is a misleading suggestion in the book that says that you can
  17 usually guess the `pid's.  Wiser is to always use the explicit value
  18 returned by the `run()' statement that instantiated the proces.
  19 Processes started with the `active' prefix obtain instantiation
  20 numbers starting at value 1, in the order in which they appear in the
  21 specification.  Each process also has a local variable _pid that
  22 holds its own instantiation number.
  23
  24 SPECIFYING TEMPORAL CLAIMS
  25
  26 The body of a temporal claim is defined just like PROMELA proctype bodies.
  27 This means that all control flow structures, such as if-fi selections,
  28 do-od repetitions, and goto jumps, are allowed.
  29 There is, however, one important difference:
  30
  31         Every statement inside a temporal claim is (interpreted as) a condition.
  32         A never claim should therefore never contain statements that can
  33         have side-effects (assignments, communications, run-statements, etc.)
  34
  35 Temporal claims are used to express behaviors that are considered undesirable
  36 or illegal.  We say that a temporal claim is `matched' if the undesirable
  37 behavior can be realized, and thus the claim violated.
  38
  39 The recommended use of a temporal claim is in combination with acceptance labels.
  40 There are two ways to `match' a temporal claim, depending on whether the
  41 undesirable behavior defines a terminating or a cyclic execution sequence.
  42
  43 o A temporal claim is matched when it terminates (reaches its closing curly brace).
  44   That is, the claim can be violated if the closing curly brace of the PROMELA
  45   body of the claim is reachable for at least one execution sequence.
  46
  47 o For a cyclic execution sequence, the claim is matched only when an explicit
  48   acceptance cycle exists.  The acceptance labels within temporal claims
  49   are user defined, there are no defaults.  This means that in the absence of
  50   acceptance labels no cyclic behavior can be matched by a temporal claim.
  51   It also means that to check a cyclic temporal claim, acceptance labels should
  52   only occur within the claim and not elsewhere in the PROMELA code.
  53
  54
  55 SEMANTICS
  56
  57 The normal system behavior of a PROMELA system is defined as the
  58 `asynchronous product' of the behaviors of the individual processes.
  59 Given an arbitrary system state, its successor states are obtained
  60 in two steps.  In the first step all the executable (atomic) statements in the
  61 individual processes are identified.  In the second step, each one of these
  62 statements is executed.
  63 Each single execution produces a successor state in the asynchronous product.
  64 The complete system behavior is thus defined recursively and
  65 represents all possible interleavings of the individual process behaviors.
  66 Call this asynchronous product machine the `global machine'.
  67
  68 The addition of a temporal claim defines an additional `synchronous product'
  69 of this global machine with the state machine that defines the temporal
  70 claim.  Call the latter machine the `claim machine', and call the new
  71 synchronous product the `labeled machine'.
  72
  73 Every state in the labeled machine is a pair (p,q) with p a state in the global
  74 machine and q a state in the claim machine.  Every transition in the labeled
  75 machine is similarly defined by a pair (r,s) with r a transition in the global
  76 machine and s a transition in the claim machine.
  77 In other words, every transition in the `synchronous' product is a joint move
  78 of the global machine and the claim machine.
  79 (By contrast, every transition in an `asynchronous' product would correspond
  80 to a single transition in either the global machine or the claim machine, thus
  81 interleaving transitions instead of combining them.)
  82
  83 Since all statements in the claim machine are boolean propositions, the second
  84 half of the transition pair (r,s) is either true or false.
  85 Call all transitions where this proposition is true `matching transitions'.
  86 In a matching transition proposition s evaluates to true in state system state r.
  87 Notice that the claim machine has at least one stop state E, the state
  88 at the closing curly brace of the claim body.
  89
  90 The semantics of temporal claims can now be summed up as follows.
  91
  92 o If the labeled machine contains any sequence of matching transitions only,
  93   that connects its initial state with a state (p,E) for any p, the temporal
  94   claim can be matched by a terminating sequence (a correctness violation).
  95
  96 o If the labeled machine contains any cycle of matching transitions only, that
  97   passes through an acceptance state, the temporal claim can be matched by a
  98   cyclic sequence.
  99
 100
 101 EXAMPLES
 102
 103 Listed below are the equivalent PROMELA definitions for the three basic
 104 temporal properties defined by Zohar Manna & Amir Pnueli in
 105 ``Tools and Rules for the Practicing Verifier'' Stanford University,
 106 Report STAN-CS-90-1321, July 1990, 34 pgs.
 107
 108 The following descriptions are quoted from Manna & Pnueli:
 109
 110         ``There are three classes of properties we [...] believe to cover
 111         the majority of properties one would ever wish to verify.''
 112
 113         1. Invariance
 114         ``An invariance property refers to an assertion p, and requires that p
 115         is an invariant over all the computations of a program P, i.e. all
 116         the states arising in a computation of P satisfy p.  In temporal
 117         logic notation, such properties are expressed by [] p, for a state
 118         formula p.''
 119
 120         Corresponding Temporal Claim in PROMELA:
 121         never {
 122                 do
 123                 :: p
 124                 :: !p -> break
 125                 od
 126         }
 127
 128         2. Response
 129         ``A response property refers to two assertions p and q, and
 130         requires that every p-state (a state satisfying p) arising in
 131         a computation is eventually followed by a q-state.
 132         In temporal logic notation this is written as p -> <> q.''
 133
 134         Corresponding Temporal Claim in PROMELA:
 135         never {
 136                 do
 137                 :: true
 138                 :: p && !q -> break
 139                 od;
 140         accept:
 141                 do
 142                 :: !q
 143                 od
 144         }
 145
 146         Note that using (!p || q) instead of `skip' would check only the
 147         first occurrence of p becoming true while q is false.
 148         The above formalization checks for all occurrences, also future ones.
 149         Strictly seen, therefore, the claim above uses a common interpretation
 150         of the formula, requiring it to hold always, or: [] { p -> <> q }
 151
 152         3. Precedence
 153         ``A simple precedence property refers to three assertions p, q, and r.
 154         It requires that any p-state initiates a q-interval (i.e. an interval
 155         all of whose states satisfy q) which, either runs to the end of the
 156         computation, or is terminated by an r-state.
 157         Such a property is useful to express the restriction that, following
 158         a certain condition, one future event will always be preceded by
 159         another future event.
 160         For example, it may express the property that, from the time a certain
 161         input has arrived, there will be an output before the next input.
 162         Note that this does not guarantee [require] that the output will actually
 163         be produced. It only guarantees [requires] that the next input (if any)
 164         will be preceded by an output.  In temporal logic, this property is
 165         expressed by p -> (q U r), using the unless operator (weak until) U.
 166
 167         Corresponding Temporal Claim in PROMELA:
 168
 169         never {
 170                 do
 171                 :: true         /* to match any occurrence */
 172                 :: p &&  q && !r -> break
 173                 :: p && !q && !r -> goto error
 174                 od;
 175                 do
 176                 ::  q && !r
 177                 :: !q && !r -> break
 178                 od;
 179         error:  skip
 180         }
 181
 182         Strictly again, this encodes: [] { p -> (q U r) }
 183         To match just the first occurence, replace 'true' with (!p || r).