Errata for `Design and Validation of Computer Protocols' [trivial typos not listed] CHAPTER 2, page 26 - Example of a Shorter Error Scenario ============================================================ A duplicate message can be accepted after even a single transmission error occurs. E.g.: (A) (B) ~ ~ | | | ack 'z' /-----------<---------+ +-----------/ | accept(z) | | +-----------\ ack 'a' -> err | | \----------->--------+ | | | nak 'z' /-----------<--------+ +------------/ | accept(z) | | CHAPTER 3, page 61/62 - Revised CRC-Algorithm (Bits renumbered in more standard right to left order.) ============================================================ The following C program, by Don Mitchell of AT&T Bell Laboratories, generates a lookup table for an arbitrary checksum polynomial. Input for the routine is an octal number, specified as an argument, that encodes the generator polynomial. In the version of the program shown here, compliments of Ned W. Rhodes, Software Systems Group, bits are numbered from zero to r-1, with bit zero corresponding to the right-most bit, and r the degree of the generator polynomial. (In Mitchell's original algorithm the bits in the message and generator polynomial were reversed.) The r-th bit itself is omitted from the code word, since it is implicit in the length. Using this program takes two separate steps. First, the program is compiled and run to generate the lookup tables. Then the checksum generation routine can be compiled, with the precalculated lookup tables in place. On a UNIX system, the program is compiled as $ cc -o crc_init crc_init.c Lookup tables for the two most popular CRC-polynomials can now be produced as follows: $ crc_init 0100005 > crc_16.h $ crc_init 010041 > crc_ccitt.h This is the text of crc_init.c: main(argc, argv) int argc; char *argv[]; { unsigned long crc, poly; int n, i; sscanf(argv[1], "%lo", &poly); if (poly & 0xffff0000) { fprintf(stderr, "polynomial is too large\n"); exit(1); } printf("/*\n * CRC 0%o\n */\n", poly); printf("static unsigned short crc_table[256] = {\n"); for (n = 0; n < 256; n++) { if (n % 8 == 0) printf(" "); crc = n << 8; for (i = 0; i < 8; i++) { if (crc & 0x8000) crc = (crc << 1) ^ poly; else crc <<= 1; crc &= 0xFFFF; } if (n == 255) printf("0x%04X ", crc); else printf("0x%04X, ", crc); if (n % 8 == 7) printf("\n"); } exit(0); } The table can now be used to generate checksums: unsigned short cksum(s, n) register unsigned char *s; register int n; { register unsigned short crc=0; while (n-- > 0) crc = crc_table[(crc>>8 ^ *s++) & 0xff] ^ (crc<<8); return crc; } CHAPTER 4, page 81 - Typo ============================================================ old< Taking the modulo M effect into account, this becomes: valid(m) = ( 0 < p - m <= W ) || ( 0 < p - M - m <= W ) new> Taking the modulo M effect into account (p is always smaller than M), this becomes: valid(m) = ( 0 < p - m <= W ) || ( 0 < p + M - m <= W ) ERROR, Page 83, Figure 4.14 =========================== should not "accept:i" if (a==e) is false CHAPTER 5, error/typos =========================== Page 96, bottom The mutual exclusion algorithm attributed to Dekker is really a simplication of Dekker's algorithm that is known as Peterson's algorithm. Dekker's original solution is modeled in Promela like this: #define true 1 #define false 0 #define Aturn 1 #define Bturn 0 bool x, y, t; proctype A() { do :: x = true; if :: y == true && t == Bturn -> x = false; (t == Aturn) :: y == false -> break fi od; /* critical section */ t = Bturn; x = false } proctype B() { do :: y = true; if :: x == true && t == Aturn -> y = false; (t == Bturn) :: x == false -> break fi od; /* critical section */ t = Aturn; y = false } init { run A(); run B() } =========================== Page 98, last paragraph old> "If the receive operation tries to retrieve more parameters than are available, the value of the extra parameters is undefined; if it receives fewer than the number of parameters that was sent, the extra information is lost." new> "It is always an error if the receive operation tries to retrieve a different number of parameters than the corresponding channel declaration specifies." =========================== Page 99, last line of "init", middle of page: old< qname!qforb new> qname[0]!qforb Page 100, delete last line on page: old< byte name; /* delete */ Page 103, in the Dijkstra example: old< chan sema = [0] of { bit }; new> chan sema = [0] of { mtype }; Page 108, "init" section, top of page: old< chan Ain = [2] of { byte }; chan Bin = [2] of { byte }; chan Aout = [2] of { byte }; chan Bout = [2] of { byte }; new> chan Ain = [2] of { byte, byte }; chan Bin = [2] of { byte, byte }; chan Aout = [2] of { byte, byte }; chan Bout = [2] of { byte, byte }; =========================== Page 107, last sentence of first paragraph Section 5.12: old< discussed in Section 2.4. new> discussed in Section 2.3. =========================== Page 110, exercise 5-3: old< Revise the two programs from Section 5.6 new> Revise the two programs from Section 5.8 CHAPTER 6 TYPO, page 117 ======================= old< chan sema[0] of {bit}; new> chan sema = [0] of {bit}; SERIOUS OMISSION, Section 6.4, page 116-117: ================================================= The treatment of formalizing system invariants in a 1-statement monitor process is correct only if the model does not contain any timeout statements. If it does, the statements in the model that would be executed after a timeout expires are not checked (since assert is always executable, it would always be executed before the timeout expires under default timeout heuristics used in spin). there are two possible solutions: - disable the default timeout heuristics for a fully exhaustive search for all possible choices of timeouts (brute force) to do this, include a single line #define timeout skip as the first line of your model - and nothing else has to change - use a safer formalization of the system invariant, using a never claim. the simples formalization is: never { do :: assert(invariant) od } which checks the truth of the invariant for every reachable state, independent of timeouts. another way would be to use the implicit matching behavior of a never claim, without an explicit assertion: never { do :: (invariant) /* things are fine, the invariant holds */ :: !(invariant) -> break /* invariant fails - match */ od } CLARIFICATION, page 118, Section 6.5 ==================================== The validator SPIN does not enforce the second criterion for a proper endstate, i.e., the emptiness of all channels. It does enforce the revised first criterion from the bottom of page 118. TYPO, page 121 middle: ================================================= old< never { do :: skip od -> P -> !Q } new> never { do :: skip :: break od -> P -> !Q } ADDED EXPLANATIONS (throughout page 121 and onw.): ================================================= A terminating claim is matched, and the corresponding correctness property thereby violated, if and when the claim body terminates. A non-terminating claim is matched, and the corresponding correctness property violated, if and when an acceptance cycle is detected. SPECIFYING TEMPORAL CLAIMS The body of a temporal claim is defined just like PROMELA proctype bodies. This means that all control flow struc- tures, 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 boolean condition. Specifically, this means that the statements inside temporal claims should be free of side-effects. For reference, the PROMELA statements with side-effects are: assignments, assertions, sends, receives, and printf statements. Temporal claims are used to express system behaviors that are considered undesirable or illegal. We say that a temporal claim is matched if the undesirable behavior can be realized, and thus our correctness claim can be violated. The most useful application of temporal claims is in combination with acceptance labels. There are then two ways to match a temporal claim, depending on whether the undesirable behavior defines terminating or cyclic execution sequences. For a terminating execution sequence, a temporal claim is matched only when it can terminate (reaches the 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 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. ERROR, page 124, top ======================= old< :: len(receiver) == 0 new> :: skip /* allow any time delay */ ERROR, page 125, top ======================= the claim can of course always be violated (== matched), whether timeout is redefined or not. CHAPTER 7 ERROR, page 139, bottom ======================= old< Pr(Burst >= 17) = 0.08 . e ^ { -0.08 . 17 } = 0.007 new> Pr(Burst >= 17) = 0.009 . e ^ { -0.009 . 17 } = 0.007 ERROR, page 156, middle ======================= old< flow_to_dll[n]!sync_ack,0 new> flow_to_dll[n]!sync_ack,m (and move the new line up to precede: "m=0;") old< flow_to_ses[n]!sync_ack,0 new> flow_to_ses[n]!sync_ack,m old< To avoid circularity, the synchronization messages do not carry sequence numbers. new> The sync_ack message echos the session number of the sync message. ERROR, page 156, bottom ======================= old< || (0 || (0 if new> :: skip -> 0 new> :: ans!small new> :: ans!great new> fi CHAPTER 11 ERROR, page 224, algorithm "analyze()" ====================================== old< q = element from W; new> q = last element from W; further down: ============= old< If states are stored in set W in first-in first-out order, the algorithm performs a breadth-first search of the state space tree. new> If states are stored in set W in first-in last-out (i.e., stack) order, the algorithm performs a depth-first search of the state space tree. further down: ============= old< If states are stored in first-in last-out (i.e., stack) < order, this changes into a depth-first search. new> If states are stored and removed in first-in first-out order, this changes into a breadth-first search (element q must be deleted upon retrieval from set W in this type of algorithm). Page 227, top ============= old< q = element from W; new> q = last element from W; Page 237, bottom ================ old< after removing states 4, 3, and 2 from the stack... new> after removing states 4, and 3 from the stack... CHAPTER 13 Page 315, 2nd para in 13.9 ========================== The first two sentences of this paragraph are incorrect. At the low end, just 1 state would be stored in the hash-array, taking up 2 bits of storage out of N available bits; at the high end, all N bits would be set at the end of the run, and (allowing overlaps) we cannot have seen more than N states. This leads to a possible range of values for the hash factor of N/2 >= hf >= 1 For full state space storage the hash factor is meaningless. CHAPTER 14 Page 331, lines 86, 88, and 94 ============================== See the corrections described for CHAPTER 7, page 156. APPENDIX C ============================== Page 387-388 The syntax of remote referencing has changed in SPIN Version 2.0. Remote referencing to local variables is no longer allowed (page 387, 5th line from below). The syntax for referencing the state of another process has changed from (page 388, 3rd line): same[2]:here to: same[2]@here =end errata=