3 .\" eqn file | tbl | troff -ms
16 gerard@plan9.bell-labs.com
18 \*V can be used for proving or disproving logical properties
19 of concurrent systems.
20 To render the proofs, a concurrent system is first
21 modeled in a formal specification language called \*P.
22 The language allows one to specify the behaviors
23 of asynchronously executing
24 processes that may interact through synchronous
25 or asynchronous message passing, or through direct
26 access to shared variables.
28 System models specified in this way can be verified
29 for both safety and liveness properties. The specification
30 of general properties in linear time temporal logic is
33 The first part of this manual
34 discusses the basic features of the specification language \*P.
35 The second part describes the verifier \*V.
40 \*P is short for Protocol Meta Language [Ho91].
41 \*P is a \f2modeling\f1 language, not a programming language.
42 A formal model differs in two essential ways from an implementation.
43 First, a model is meant to be an abstraction of a design
44 that contains only those aspects of the design that are
45 directly relevant to the properties one is interested in proving.
46 Second, a formal model must contain things that are typically not part
47 of an implementation, such as worst-case assumptions about
48 the behavior of the environment that may interact with the
49 system being studied, and a formal statement of relevant correctness
50 properties. It is possible to mechanically extract abstract models
51 from implementation level code, as discussed, for instance in [HS99].
53 Verification with \*V is often performed in a series of steps,
54 with the construction of increasingly detailed models.
55 Each model can be verified under different types of
56 assumptions about the environment and for different
57 types of correctness properties.
58 If a property is not valid for the given assumptions about
59 system behavior, the verifier can produce a counter-example
60 that demonstrates how the property may be violated.
61 If a property is valid, it may be possible to simplify the
62 model based on that fact, and prove still other properties.
64 Section 1.1 covers the basic building blocks of the language.
65 Section 1.2 introduces the control flow structures.
66 Section 1.3 explains how correctness properties are specified.
67 Section 1.4 concludes the first part with a discussion of
68 special predefined variables and functions that can be used to
69 express some correctness properties.
71 Up to date manual pages for \*V can always be found online at:
73 http://cm.bell-labs.com/cm/cs/what/spin/Man/
78 A \*P model can contain three different types of objects:
81 \(bu Processes (section 1.1.1),
83 \(bu Variables (section 1.1.2),
85 \(bu Message channels (section 1.1.3).
88 All processes are global objects.
89 For obvious reasons, a \*P model must contain at least one
90 process to be meaningful.
91 Since \*V is specifically meant to prove properties of
92 concurrent systems, a model typically contains more than
95 Message channels and variables, the two basic types of data objects,
96 can be declared with either a global scope or a local scope.
97 A data object with global scope can be referred to by all processes.
98 A data object with a local scope can be referred to by just a
99 single process: the process that declares and instantiates the object.
100 As usual, all objects must be declared in the specification
101 before they are referenced.
105 Here is a simple process that does nothing except print
109 printf("it works\en")
112 There are a few things to note.
114 is a predefined keyword from the language.
115 It can be used to declare and instantiate
116 a single initial process in the model.
117 (It is comparable to the
119 procedure of a C program.)
122 process does not take arguments, but it can
123 start up (instantiate) other processes that do.
125 is one of a few built-in procedures in the language.
126 It behaves the same as the C version.
127 Note, finally, that no semicolon follows the single
129 statement in the above example.
130 In \*P, semicolons are used as statement separators,
131 not statement terminators. (The \*V parser, however, is
132 lenient on this issue.)
134 Any process can start new processes by using another
135 built-in procedure called
139 proctype you_run(byte x)
141 printf("my x is: %d\en", x)
152 is again a keyword that introduces the declaration
153 of a new type of process.
154 In this case, we have named that type
156 and declared that all instantiations of processes
157 of this type will take one argument: a data object
160 that can be referred to within this process by the name
164 can be created with the predefined procedure
166 as shown in the example.
169 statement completes, a copy of the process
170 has been started, and all its arguments have been
171 initialized with the arguments provided.
172 The process may, but need not, have performed
173 any statement executions at this point.
174 It is now part of the concurrent system,
175 and its execution can be interleaved arbitrarily with
176 those of the other, already executing processes.
177 (More about the semantics of execution follows shortly.)
179 In many cases, we are only interested in creating a
180 single instance of each process type that is declared,
181 and the processes require no arguments.
182 We can define this by prefixing the keyword
184 from the process declaration with another keyword:
186 Instances of all active proctypes are created when the
187 system itself is initialized.
188 We could, for instance, have avoided the use of
190 by declaring the corresponding process in the last example
193 active proctype main() {
198 Note that there are no parameters to instantiate in this
199 case. Had they been declared, they would default to a
200 zero value, just like all other data objects
201 that are not explicitly instantiated.
203 Multiple copies of a process type can also be created in
204 this way. For example:
206 active [4] proctype try_me() {
207 printf("hi, i am process %d\en", _pid)
210 creates four processes.
211 A predefined variable
213 is assigned to each running process, and holds
214 its unique process instantiation number.
215 In some cases, this number is needed when a reference
216 has to be made to a specific process.
218 Summarizing: process behavior is declared in
220 definitions, and it is instantiated with either
222 statements or with the prefix
224 Within a proctype declaration, statements are separated
225 (not terminated) by semicolons.
226 As we shall see in examples that follow, instead of the
227 semicolon, one can also use the alternative separator
229 (arrow), wherever that may help to clarify the structure
232 Semantics of Execution
234 In \*P there is no difference between a condition or
235 expression and a statement.
236 Fundamental to the semantics of the language is the
237 notion of the \f2executability\f1 of statements.
238 Statements are either executable or blocked.
239 Executability is the basic means of enforcing
240 synchronization between the processes in a distributed system.
241 A process can wait for an event to happen by waiting
242 for a statement to become executable.
243 For instance, instead of writing a busy wait loop:
245 while (a != b) /* not valid Promela syntax */
246 skip; /* wait for a==b */
249 we achieve the same effect in \*P with the statement
254 Often we indicate that the continuation of an execution
255 is conditional on the truth of some expression by using
256 the alternate statement separator:
262 statements are always executable in \*P.
263 A condition, however, can only be executed (passed) when it holds.
264 If the condition does not hold, execution blocks until it does.
265 There are similar rules for determining the executability
266 of all other primitive and compound statements in the
268 The semantics of each statement is defined in terms of
269 rules for executability and effect.
270 The rules for executability set a precondition on the state
271 of the system in which a statement can be executed.
272 The effect defines how a statement will alter a
273 system state when executed.
275 \*P assumes that all individual statements are executed
276 atomically: that is, they model the smallest meaningful entities
277 of execution in the system being studied.
278 This means that \*P defines the standard asynchronous interleaving
279 model of execution, where a supposed scheduler is free at
280 each point in the execution to select any one of the processes
281 to proceed by executing a single primitive statement.
282 Synchronization constraints can be used to influence the
283 interleaving patterns. It is the purpose of a concurrent system's
284 design to constrain those patterns in such a way that no
285 correctness requirements can be violated, and all service
286 requirements are met. It is the purpose of the verifier
287 either to find counter-examples to a designer's claim that this
288 goal has been met, or to demonstrate that the claim is indeed valid.
292 The table summarizes the five basic data types used in \*P.
296 are synonyms for a single bit of information.
297 The first three types can store only unsigned quantities.
298 The last two can hold either positive or negative values.
299 The precise value ranges of variables of types
303 is implementation dependent, and corresponds
304 to those of the same types in C programs
305 that are compiled for the same hardware.
306 The values given in the table are most common.
318 short $-2 sup 15# .. $2 sup 15 -1#
319 int $-2 sup 31# .. $2 sup 31 -1#
324 The following example program declares a array of
327 and a scalar variable
330 Note that the example relies on the fact that
332 is either 0 or 1 here.
336 * Peterson's algorithm for enforcing
337 * mutual exclusion between two processes
338 * competing for access to a critical section
342 active [2] proctype user()
345 want[_pid] = 1; turn = _pid;
347 /* wait until this condition holds: */
348 (want[1 - _pid] == 0 || turn == 1 - _pid);
358 In the above case, all variables are initialized to zero.
359 The general syntax for declaring and instantiating a
360 variable, respectively for scalar and array variables, is:
362 type name = expression;
363 type name[constant] = expression
365 In the latter case, all elements of the array are initialized
366 to the value of the expression.
367 A missing initializer fields defaults to the value zero.
368 As usual, multiple variables of the same type can be grouped
369 behind a single type name, as in:
373 In this example, the variable
375 is initialized to the value 4; variable
377 and the elements of array
379 are all initialized to zero.
381 Variables can also be declared as structures.
399 introduces two user-defined data types, the first named
403 A single variable named
410 that are not explicitly initialized (in the example, all fields except
412 are initialized to zero.
413 References to the elements of a structure are written as:
415 foo.a[2] = foo.fld2.f + 12
417 A variable of a user-defined type can be passed as a single
418 argument to a new process in
432 Note that even though \*P supports only one-dimensional arrays,
433 a two-dimensional array can be created indirectly with user-defined
434 structures, for instance as follows:
442 This creates a data structure of 16 elements that can be
443 referenced, for instance, as
446 As in C, the indices of an array of
448 elements range from 0 to
453 Expressions must be side-effect free in \*P.
454 Specifically, this means that an expression cannot
455 contain assignments, or send and receive operations (see section 1.1.3).
463 are assignments in \*P, with the same effects.
468 is not a valid assignment, because the right-hand side
469 operand is not a valid expression in \*P (it is not side-effect free).
471 It is also possible to write a side-effect free conditional
472 expression, with the following syntax:
474 (expr1 -> expr2 : expr3)
476 The parentheses around the conditional expression are required to
477 avoid misinterpretation of the arrow.
478 The example expression has the value of \f(CWexpr2\f1 when \f(CWexpr1\f1
479 evaluates to a non-zero value, and the value of \f(CWexpr3\f1 otherwise.
483 variable = expression
485 the values of all operands used inside the expression are first cast to
486 signed integers before the operands are applied.
487 After the evaluation of the expression completes, the value produced
488 is cast to the type of the target variable before the assignment takes place.
492 Message channels are used to model the transfer of data
494 They are declared either locally or globally,
495 for instance as follows:
497 chan qname = [16] of { short, byte }
501 introduces a channel declaration.
502 In this case, the channel is named
504 and it is declared to be capable of storing up
506 Each message stored in the channel is declared here to
507 consist of two fields: one of type
511 The fields of a message can be any one of the basic types
519 or any user-defined type.
520 Message fields cannot be declared as arrays.
522 A message field of type
524 can be used to pass a channel identifier
525 through a channel from one process to another.
531 sends the values of expressions
535 to the channel that we just created. It appends
536 the message field created from the values of the two
537 expressions (and cast to the appropriate types of the
538 message fields declared for
540 to the tail of the message buffer of 16 slots that belongs
543 By default the send statement is only executable if the target
545 (This default semantics can be changed in the verifier into
546 one where the send statement is always executable, but the
547 message will be lost when an attempt is made to append it to
554 retrieves a message from the head of the same buffer,
555 and stores the two expressions in variables
560 The receive statement is executable only if the source channel
563 If more parameters are sent per message than were declared
564 for the message channel, the redundant parameters are lost.
565 If fewer parameters are sent than declared,
566 the value of the remaining parameters is undefined.
567 Similarly, if the receive operation tries to retrieve more
568 parameters than available, the value of the extra parameters is
569 undefined; if it receives fewer than the number of parameters
570 sent, the extra information is lost.
572 An alternative, and equivalent, notation for the
573 send and receive operations is to structure the
574 message fields with parentheses, as follows:
576 qname!expr1(expr2,expr3)
577 qname?var1(var2,var3)
579 In the above case, we assume that
581 was declared to hold messages consisting of three fields.
583 Some or all of the arguments of the receive operation
584 can be given as constants instead of as variables:
586 qname?cons1,var2,cons2
588 In this case, an extra condition on the executability of the
589 receive operation is that the value of all message fields
590 specified as constants match the value of the corresponding
591 fields in the message that is to be received.
593 Here is an example that uses some of the mechanisms introduced
603 proctype B(chan qforb)
606 printf("x = %d\en", x)
611 chan qname = [1] of { chan };
612 chan qforb = [1] of { int };
618 The value printed by the process of type
623 A predefined function
625 returns the number of messages currently
628 Two shorthands for the most common uses of this
633 with the obvious connotations.
635 Since all expressions must be side-effect free,
636 it is not valid to say:
644 We could rewrite the second example (using an atomic sequence,
645 as explained further in section 1.2.1):
647 atomic { (a > b && !full(qname)) -> qname!123 }
649 The meaning of the first example is ambiguous. It could mean
650 that we want the condition to be true if the receive operation
651 is unexecutable. In that case, we can rewrite it without
656 It could also mean that we want the condition
657 to be true when the channel does contain a message with
659 We can specify that as follows:
661 atomic { qname?[0] -> qname?var }
663 The first statement of this atomic sequence is
664 an expression without side-effects that
665 evaluates to a non-zero value only if the
670 would have been executable at that
673 contains at least one message and the oldest
674 message stored consists of one message field
676 Any receive statement can be turned into
677 a side-effect free expression by placing square
678 brackets around the list of all message parameters.
679 The channel contents remain undisturbed by the
680 evaluation of such expressions.
682 Note carefully, however, that in non-atomic sequences
683 of two statements such as
685 !full(qname) -> qname!msgtype
689 qname?[msgtype] -> qname?msgtype
691 the second statement is not necessarily executable
692 after the first one has been executed.
693 There may be race conditions when access to the channels
694 is shared between several processes.
695 Another process can send a message to the channel
696 just after this process determined that it was not full,
697 or another process can steal away the
698 message just after our process determined its presence.
700 Two other types of send and receive statements are used
701 less frequently: sorted send and random receive.
702 A sorted send operation is written with two, instead of one,
703 exclamation marks, as follows:
707 A sorted send operation will insert a message into the channel's buffer
708 in numerical order, instead of in FIFO order.
709 The channel contents are scanned from the first message towards the
710 last, and the message is inserted immediately before the first message
711 that follows it in numerical order.
712 To determine the numerical order, all message fields are
715 The logical counterpart of the sorted send operation
716 is the random receive.
717 It is written with two, instead of one, question marks:
721 A random receive operation is executable if it is executable for \f2any\f1
722 message that is currently buffered in a message channel (instead of
723 only for the first message in the channel).
724 Normal send and receive operations can freely be combined with
725 sorted send and random receive operations.
727 Rendezvous Communication
729 So far we have talked about asynchronous communication between processes
730 via message channels, declared in statements such as
732 chan qname = [N] of { byte }
736 is a positive constant that defines the buffer size.
737 A logical extension is to allow for the declaration
739 chan port = [0] of { byte }
741 to define a rendezvous port.
742 The channel size is zero, that is, the channel
744 can pass, but cannot store, messages.
745 Message interactions via such rendezvous ports are
746 by definition synchronous.
747 Consider the following example:
751 chan name = [0] of { byte, byte };
766 is a global rendezvous port.
767 The two processes will synchronously execute their first statement:
768 a handshake on message
770 and a transfer of the value 124 to local variable
772 The second statement in process
774 will be unexecutable,
775 because there is no matching receive operation in process
780 is defined with a non-zero buffer capacity,
781 the behavior is different.
782 If the buffer size is at least 2, the process of type
784 can complete its execution, before its peer even starts.
785 If the buffer size is 1, the sequence of events is as follows.
788 can complete its first send action, but it blocks on the
789 second, because the channel is now filled to capacity.
792 can then retrieve the first message and complete.
795 becomes executable again and completes,
796 leaving its last message as a residual in the channel.
798 Rendezvous communication is binary: only two processes,
799 a sender and a receiver, can be synchronized in a
800 rendezvous handshake.
802 As the example shows, symbolic constants can be defined
803 with preprocessor macros using
805 The source text of a \*P model is translated by the standard
807 The disadvantage of defining symbolic names in this way is,
808 however, that the \*P parser will only see the expanded text,
809 and cannot refer to the symbolic names themselves.
810 To prevent that, \*P also supports another way to define
811 symbolic names, which are preserved in error reports.
812 For instance, by including the declaration
814 mtype = { ack, msg, error, data };
816 at the top of a \*P model, the names provided between the
817 curly braces are equivalent to integers of type
819 but known by their symbolic names to the \*V parser and the
820 verifiers it generates.
821 The constant values assigned start at 1, and count up.
822 There can be only one
824 declaration per model.
828 So far, we have seen only some of the basic statements
829 of \*P, and the way in which they can be combined to
830 model process behaviors.
831 The five types of statements we have mentioned are:
841 is syntactically and semantically equivalent to the
844 (i.e., to true), and is in fact quietly replaced with this
845 expression by the lexical analyzer of \*V.
847 There are also five types of compound statements.
851 Atomic sequences (section 1.2.1),
854 Deterministic steps (section 1.2.2),
857 Selections (section 1.2.3),
860 Repetitions (section 1.2.4),
863 Escape sequences (section 1.2.5).
869 The simplest compound statement is the
873 atomic { /* swap the values of a and b */
879 In the example, the values of two variables
883 are swapped in a sequence of statement executions
884 that is defined to be uninterruptable.
885 That is, in the interleaving of process executions, no
886 other process can execute statements from the moment that
887 the first statement of this sequence begins to execute until
888 the last one has completed.
890 It is often useful to use
892 sequences to start a series of processes in such a
893 way that none of them can start executing statements
894 until all of them have been initialized:
905 sequences may be non-deterministic.
906 If any statement inside an
908 sequence is found to be unexecutable, however,
909 the atomic chain is broken, and another process can take over
911 When the blocking statement becomes executable later,
912 control can non-deterministically return to the process,
913 and the atomic execution of the sequence resumes as if
914 it had not been interrupted.
918 Another way to define an indivisible sequence of actions
922 In the above case, for instance, we could also have written:
924 d_step { /* swap the values of a and b */
930 The difference between a
939 sequence must be completely deterministic.
940 (If non-determinism is nonetheless encountered,
941 it is always resolved in a fixed and deterministic
942 way: i.e., the first true guard in selection or
943 repetition structures is always selected.)
947 jumps into or out of a
949 sequence are permitted.
953 sequence cannot be interrupted when a
954 blocking statement is encountered.
955 It is an error if any statement other than
958 sequence is found to be unexecutable.
962 sequence is executed as one single statement.
963 In a way, it is a mechanism for adding new types
964 of statements to the language.
966 None of the items listed above apply to
969 This means that the keyword
971 can always be replaced with the keyword
973 but the reverse is not true.
974 (The main, perhaps the only, reason for using
976 sequences is to improve the efficiency of
981 A more interesting construct is the selection structure.
982 Using the relative values of two variables
986 to choose between two options, for instance, we can write:
989 :: (a != b) -> option1
990 :: (a == b) -> option2
993 The selection structure above contains two execution sequences,
994 each preceded by a double colon.
995 Only one sequence from the list will be executed.
996 A sequence can be selected only if its first statement is executable.
997 The first statement is therefore called a \f2guard\f1.
999 In the above example the guards are mutually exclusive, but they
1001 If more than one guard is executable, one of the corresponding sequences
1002 is selected nondeterministically.
1003 If all guards are unexecutable the process will block until at least
1004 one of them can be selected.
1005 There is no restriction on the type of statements that can be used
1006 as a guard: it may include sends or receives, assignments,
1010 The rules of executability determine in each case what the semantics
1011 of the complete selection structure will be.
1012 The following example, for instance, uses receive statements
1013 as guards in a selection.
1017 chan ch = [1] of { byte };
1036 The example defines three processes and one channel.
1037 The first option in the selection structure of the process
1040 is executable if the channel contains
1045 is a symbolic constant defined in the
1047 declaration at the start of the program.
1048 The second option is executable if it contains a message
1052 is a symbolic constant.
1053 Which message will be available depends on the unknown
1054 relative speeds of the processes.
1056 A process of the following type will either increment
1057 or decrement the value of variable
1063 active proctype counter()
1071 Assignments are always executable, so the choice made
1072 here is truly a non-deterministic one that is independent
1073 of the initial value of the variable (zero in this case).
1075 Repetition Structures
1077 We can modify the above program as follows, to obtain
1078 a cyclic program that randomly changes the value of
1079 the variable up or down, by replacing the selection
1080 structure with a repetition.
1084 active proctype counter()
1089 :: (count == 0) -> break
1093 Only one option can be selected for execution at a time.
1094 After the option completes, the execution of the structure
1096 The normal way to terminate the repetition structure is
1100 In the example, the loop can be
1101 broken only when the count reaches zero.
1102 Note, however, that it need not terminate since the other
1103 two options remain executable.
1104 To force termination we could modify the program as follows.
1106 active proctype counter()
1114 :: (count == 0) -> break
1118 A special type of statement that is useful in selection
1119 and repetition structures is the
1124 statement becomes executable only if no other statement
1125 within the same process, at the same control-flow point,
1127 We could try to use it in two places in the above example:
1129 active proctype counter()
1144 inside the nested selection structure, can never become
1145 executable though, and is therefore redundant (both alternative
1146 guards of the selection are assignments, which are always
1148 The second usage of the
1150 however, becomes executable exactly when
1153 .CW "(count == 0)" ,
1154 and is therefore equivalent to the latter to break from the loop.
1156 There is also an alternative way to exit the do-loop, without
1159 statement: the infamous
1161 This is illustrated in the following implementation of
1162 Euclid's algorithm for finding the greatest common divisor
1163 of two non-zero, positive numbers:
1165 proctype Euclid(int x, y)
1168 :: (x > y) -> x = x - y
1169 :: (x < y) -> y = y - x
1170 :: (x == y) -> goto done
1177 init { run Euclid(36, 12) }
1181 in this example jumps to a label named
1183 Since a label can only appear before a statement,
1184 we have added the dummy statement
1190 statement is always executable and has no other
1191 effect than to change the control-flow point
1192 of the process that executes it.
1194 As a final example, consider the following implementation of
1195 a Dijkstra semaphore, which is implemented with the help of
1196 a synchronous channel.
1201 chan sema = [0] of { bit };
1204 active proctype Dijkstra()
1216 active [3] proctype user()
1219 /* critical section */
1221 /* non-critical section */
1225 The semaphore guarantees that only one of the three user processes
1226 can enter its critical section at a time.
1227 It does not necessarily prevent the monopolization of
1228 the access to the critical section by one of the processes.
1230 \*P does not have a mechanism for defining functions or
1231 procedures. Where necessary, though, these may be
1232 modeled with the help of additional processes.
1233 The return value of a function, for instance, can be passed
1234 back to the calling process via global variables or messages.
1235 The following program illustrates this by recursively
1236 calculating the factorial of a number
1239 proctype fact(int n; chan p)
1240 { chan child = [1] of { int };
1246 run fact(n-1, child);
1254 { chan child = [1] of { int };
1259 printf("result: %d\en", result)
1262 Each process creates a private channel and uses it
1263 to communicate with its direct descendant.
1264 There are no input statements in \*P.
1265 The reason is that models must always be complete to
1266 allow for logical verifications, and input statements
1267 would leave at least the source of some information unspecified.
1269 would presuppose a source of information that is not
1272 We have already discussed a few special types of statement:
1277 Another statement in this class is the
1281 is comparable to a system level
1283 statement: it becomes executable if and only if no other
1284 statement in any of the processes is executable.
1286 is a modeling feature that provides for an escape from a
1287 potential deadlock state.
1290 takes no parameters, because the types of properties we
1291 would like to prove for \*P models must be proven independent
1292 of all absolute and relative timing considerations.
1293 In particular, the relative speeds of processes can never be
1294 known with certainty in an asynchronous system.
1298 The last type of compound structure to be discussed is the
1301 It is used as follows:
1310 represent arbitrary \*P fragments.
1313 statement begins with the execution of statements from
1315 Before each statement execution in
1317 the executability of the first statement of
1319 is checked, using the normal \*P semantics of executability.
1320 Execution of statements from
1322 proceeds only while the first statement of
1324 remains unexecutable.
1325 The first time that this `guard of the escape sequence'
1326 is found to be executable, control changes to it,
1327 and execution continues as defined for
1329 Individual statement executions remain indivisible,
1330 so control can only change from inside
1334 in between individual statement executions.
1335 If the guard of the escape sequence
1336 does not become executable during the
1339 then it is skipped entirely when
1343 An example of the use of escape sequences is:
1354 As shown in the example, the curly braces around the main sequence
1355 (or the escape sequence) can be deleted if there can be no confusion
1356 about which statements belong to those sequences.
1357 In the example, condition
1359 acts as a watchdog on the repetition construct from the main sequence.
1360 Note that this is not necessarily equivalent to the construct
1376 In the first version of the example, execution of the iteration can
1377 be interrupted at \f2any\f1 point inside each option sequence.
1378 In the second version, execution can only be interrupted at the
1379 start of the option sequences.
1381 Correctness Properties
1383 There are three ways to express correctness properties in \*P,
1389 Assertions (section 1.3.1),
1392 Special labels (section 1.3.2),
1396 claims (section 1.3.3).
1402 Statements of the form
1406 are always executable.
1407 If the expression evaluates to a non-zero value (i.e., the
1408 corresponding condition holds), the statement has no effect
1410 The correctness property expressed, though, is that it is
1411 impossible for the expression to evaluate to zero (i.e., for
1412 the condition to be false).
1413 A failing assertion will cause execution to be aborted.
1417 Labels in a \*P specification ordinarily serve as
1418 targets for unconditional
1421 There are, however, also three types of labels that
1422 have a special meaning to the verifier.
1423 We discuss them in the next three subsections.
1427 When a \*P model is checked for reachable deadlock states
1428 by the verifier, it must be able to distinguish valid \f2end state\f1s
1430 By default, the only valid end states are those in which
1431 every \*P process that was instantiated has reached the end of
1433 Not all \*P processes, however, are meant to reach the
1435 Some may very well linger in a known wait
1436 state, or they may sit patiently in a loop
1437 ready to spring into action when new input arrives.
1439 To make it clear to the verifier that these alternate end states
1440 are also valid, we can define special end-state labels.
1441 We can do so, for instance, in the process type
1443 from an earlier example:
1458 defines that it is not an error if, at the end of an
1459 execution sequence, a process of this type
1460 has not reached its closing curly brace, but waits at the label.
1461 Of course, such a state could still be part of a deadlock state, but
1462 if so, it is not caused by this particular process.
1464 There may be more than one end-state label per \*P model.
1465 If so, all labels that occur within the same process body must
1467 The rule is that every label name with the prefix
1469 is taken to be an end-state label.
1471 Progress-State Labels
1473 In the same spirit, \*P also allows for the definition of
1476 Passing a progress label during an execution is interpreted
1477 as a good thing: the process is not just idling while
1478 waiting for things to happen elsewhere, but is making
1479 effective progress in its execution.
1480 The implicit correctness property expressed here is that any
1481 infinite execution cycle allowed by the model that does not
1482 pass through at least one of these progress labels is a
1483 potential starvation loop.
1486 example, for instance, we can label the
1487 successful passing of a semaphore test as progress and
1488 ask a verifier to make sure that there is no cycle elsewhere
1496 progress: sema!p; count = 0
1502 If more than one state carries a progress label,
1503 variations with a common prefix are again valid.
1507 The last type of label, the accept-state label, is used
1508 primarily in combination with
1511 Briefly, by labeling a state with any label starting
1514 we can ask the verifier to find all cycles that \f2do\f1
1515 pass through at least one of those labels.
1516 The implicit correctness claim is that this cannot happen.
1517 The primary place where accept labels are used is inside
1526 Up to this point we have talked about the specification
1527 of correctness criteria with assertions
1528 and with three special types of labels.
1529 Powerful types of correctness criteria can already
1530 be expressed with these tools, yet so far our only option is
1531 to add them to individual
1534 We can, for instance, express the claim ``every system state
1537 is true eventually leads to a system state in which property
1539 is true,'' with an extra monitor process, such as:
1541 active proctype monitor()
1549 If we require that property
1551 must \f2remain\f1 true while we are waiting
1553 to become true, we can try to change this to:
1555 active proctype monitor()
1559 :: P -> assert(P || Q)
1563 but this does not quite do the job.
1564 Note that we cannot make any assumptions about the
1565 relative execution speeds of processes in a \*P model.
1566 This means that if in the remainder of the system the
1569 becomes true, we can move to the state just before the
1571 and wait there for an unknown amount of time (anything between
1572 a zero delay and an infinite delay is possible here, since
1573 no other synchronizations apply).
1576 becomes true, we may pass the assertion, but we need not
1580 becomes false only \f2after\f1
1582 has become true, we may still fail the assertion,
1583 as long as there exists some later state where neither
1588 This is clearly unsatisfactory, and we need another mechanism
1589 to express these important types of liveness properties.
1591 The Connection with Temporal Logic
1593 A general way to express system properties of the type we
1594 have just discussed is to use linear time temporal logic (LTL)
1596 Every \*P expression is automatically also a valid LTL formula.
1597 An LTL formula can also contain the unary temporal operators â–¡
1598 (pronounced always), â—Š (pronounced eventually), and
1599 two binary temporal operators
1601 (pronounced weak until) and
1603 (pronounced strong until).
1605 Where the value of a \*P expression without temporal operators can be
1606 defined uniquely for individual system states, without further context,
1607 the truth value of an LTL formula is defined for sequences of states:
1608 specifically, it is defined for the first state of a given infinite
1609 sequence of system states (a trace).
1610 Given, for instance, the sequence of system states:
1620 standard \*P expressions, is true for
1632 holds for the remainder of the sequence after
1639 is required to hold at least until
1642 If, instead, we would write \f(CWp\f(BIU\f(CWq\f1,
1643 then we also require that there exists at least
1644 one state in the sequence where
1646 does indeed become true.
1648 The temporal operators â–¡ and â—Š
1649 can be defined in terms of the strong until operator
1653 â–¡ p = !â—Š !p = !(true \f(BIU\f(CW !p)
1659 must hold in all states of a trace, and â—Š
1663 holds in at least one state of the trace.
1665 To express our original example requirement: ``every system state
1668 is true eventually leads to a system state in which property
1671 we can write the LTL formula:
1675 where the logical implication symbol
1677 is defined in the usual way as
1679 P => Q means !P || Q
1682 Mapping LTL Formulae onto Never Claims
1684 \*P does not include syntax for specifying LTL formulae
1685 directly, but it relies on the fact that every such
1686 formula can be translated into a special type of
1687 automaton, known as a Büchi automaton.
1688 In the syntax of \*P this automaton is called a
1691 If you don't care too much about the details of
1693 claims, you can skip the remainder of this section and
1694 simple remember that \*V can convert any LTL formula
1695 automatically into the proper never claim syntax with
1698 spin -f "...formula..."
1700 Here are the details.
1701 The syntax of a never claim is:
1707 where the dots can contain any \*P fragment, including
1708 arbitrary repetition, selection, unless constructs,
1711 There is an important difference in semantics between a
1716 Every statement inside a
1718 claim is interpreted as a proposition, i.e., a condition.
1721 claim should therefore only contain expressions and never
1722 statements that can have side-effects (assignments, sends or
1723 receives, run-statements, etc.)
1726 claims are used to express behaviors that are considered
1727 undesirable or illegal.
1730 claim is `matched' if the undesirable behavior can be realized,
1731 contrary to the claim, and thus the correctness requirement violated.
1732 The claims are evaluated over system executions, that is, the
1733 propositions that are listed in the claim are evaluated over the
1734 traces from the remainder of the system.
1735 The claim, therefore, should not alter that behavior: it merely
1737 Every time that the system reaches a new state, by asynchronously
1738 executing statements from the model, the claim will evaluate the
1739 appropriate propositions to determine if a counter-example can
1740 be constructed to the implicit LTL formula that is specified.
1742 Since LTL formulae are only defined for infinite executions,
1745 claim can only be matched by an infinite system execution.
1746 This by itself would restrict us to the use of progress labels
1747 and accept labels as the only means we have discussed so far
1748 for expressing properties of infinite behaviors.
1749 To conform to standard omega automata theory, the behaviors of
1751 claims are expressed exclusively with
1756 To match a claim, therefore, an infinite sequence of true propositions
1757 must exist, at least one of which is labeled with an
1759 label (inside the never claim).
1761 Since \*P models can also express terminating system behaviors,
1762 we have to define the semantics of the
1764 claims also for those behaviors.
1765 To facilitate this, it is defined that a
1767 claim can also be matched when it reaches its closing curly brace
1768 (i.e., when it appears to terminate).
1769 This semantics is based on what is usually referred to as a `stuttering
1771 With stuttering semantics, any terminating execution can be extended
1772 into an equivalent infinite execution (for the purposes of evaluating
1773 LTL properties) by repeating (stuttering) the final state infinitely often.
1774 As a syntactical convenience, the final state of a
1776 claim is defined to be accepting, i.e., it could be replaced with
1777 the explicit repetition construct:
1779 accept: do :: skip od
1781 Every process behavior, similarly, is (for the purposes of evaluating the
1783 claims) thought to be extended with a dummy self-loop on all final states:
1789 labels only occur in the
1791 claim, not in the system.)
1793 The Semantics of a Never Claim
1796 claims are probably the hardest part of the language to understand,
1797 so it is worth spending a few extra words on them.
1798 On an initial reading, feel free to skip the remainder of this
1801 The difference between a
1803 claim and the remainder of a \*P system can be explained
1805 A \*P model defines an asynchronous interleaving product of the
1806 behaviors of individual processes.
1807 Given an arbitrary system state, its successor states are
1808 conceptually obtained in two steps.
1809 In a first step, all the executable statements in the
1810 individual processes are identified.
1811 In a second step, each one of these statements is executed,
1812 each one producing one potential successor for the current state.
1813 The complete system behavior is thus defined recursively and
1814 represents all possible interleavings of the individual process behaviors.
1815 It is this asynchronous product machine that we call the `global
1820 claim defines a \f2synchronous\f1 product of the global system behavior
1821 with the behavior expressed in the claim.
1822 This synchronous product can be thought of as the construction of a
1823 new global state machine, in which every state is defined as a pair
1827 a state from the global system (the asynchronous product of processes), and
1829 a state from the claim.
1830 Every transition in the new global machine is similarly defined by a pair
1831 of transitions, with the first element a statement from the system, and the
1832 second a proposition from the claim.
1833 In other words, every transition in this final synchronous product is
1834 defined as a joint transition of the system and the claim.
1835 Of course, that transition can only occur if the proposition from the
1836 second half of the transition pair evaluates to true in the current state
1837 of the system (the first half of the state pair).
1841 To manually translate an LTL formula into a
1843 claim (e.g. foregoing the builtin translation that \*V
1844 offers), we must carefully consider whether the
1845 formula expresses a positive or a negative property.
1846 A positive property expresses a good behavior that we
1847 would like our system to have.
1848 A negative property expresses a bad behavior that we
1849 claim the system does not have.
1852 claim can express only negative claims, not positive ones.
1853 Fortunately, the two are exchangeable: if we want to express
1854 that a good behavior is unavoidable, we can formalize all
1855 ways in which the good behavior could be violated, and express
1860 Suppose that the LTL formula â—Šâ–¡
1864 a \*P expression, expresses a negative claim
1865 (i.e., it is considered a correctness violation if
1866 there exists any execution sequence in which
1868 can eventually remain true infinitely long).
1869 This can be written in a
1875 :: skip /* after an arbitrarily long prefix */
1876 :: p -> break /* p becomes true */
1879 :: p /* and remains true forever after */
1883 Note that in this case the claim does not terminate, and
1884 also does not necessarily match all system behaviors.
1885 It is sufficient if it precisely captures all violations
1886 of our correctness requirement, and no more.
1888 If the LTL formula expressed a positive property, we first
1889 have to invert it to the corresponding negative property
1891 and translate that into a
1894 The requirement now says that it is a violation if
1896 does not hold infinitely long.
1905 We have used the implicit match of a claim upon reaching the
1906 closing terminating brace.
1907 Since the first violation of the property suffices to disprove
1908 it, we could also have written:
1917 or, if we abandon the connection with LTL for a moment,
1918 even more tersely as:
1920 never { do :: assert(p) od }
1922 Suppose we wish to express that it is a violation of our
1923 correctness requirements if there exists any execution in
1925 .CW "â–¡ (p -> â—Š q)"
1926 is violated (i.e., the negation of this formula is satisfied).
1929 claim expresses that property:
1946 in the first repetition construct would imply a check for just
1947 the first occurrence of proposition
1949 becoming true in the execution sequence, while
1952 The above formalization checks for all occurrences, anywhere in a trace.
1954 Finally, consider a formalization of the LTL property
1955 .CW "â–¡ (p -> (q U r))" .
1956 The corresponding claim is:
1960 :: skip /* to match any occurrence */
1961 :: p && q && !r -> break
1962 :: p && !q && !r -> goto error
1966 :: !q && !r -> break
1971 Note again the use of
1975 to avoid matching just the first occurrence of
1979 Predefined Variables and Functions
1981 The following predefined variables and functions
1982 can be especially useful in
1986 The predefined variables are:
1992 is a predefined local variable in each process
1993 that holds the unique instantiation number for
1995 It is always a non-negative number.
1998 is a predefined global variable that always holds the
1999 instantiation number of the process that performed the last
2000 step in the current execution sequence.
2001 Its value is not part of the system state unless it is
2002 explicitly used in a specification.
2005 /* it is not possible for the process with pid=1
2006 * to execute precisely every other step forever
2010 :: _last != 1 -> _last == 1
2014 The initial value of
2018 Three predefined functions are specifically intended to be used in
2020 claims, and may not be used elsewhere in a model:
2023 .CW procname[pid]@label .
2027 returns the current control state
2028 of the process with instantiation number
2030 or zero if no such process exists.
2035 /* Whimsical use: claim that it is impossible
2036 * for process 1 to remain in the same control
2037 * state as process 2, or one with smaller value.
2040 :: pc_value(1) <= pc_value(2)
2046 tells whether the process with instantiation number
2048 has an executable statement that it can execute next.
2053 /* it is not possible for the process with pid=1
2054 * to remain enabled without ever executing
2058 :: _last != 1 && enabled(1)
2063 .CW procname[pid]@label
2064 tells whether the process with instantiation number
2066 is currently in the state labeled with
2069 .CW "proctype procname" .
2070 It is an error if the process referred to is not an instantiation
2073 Verifications with \*V
2075 The easiest way to use \*V is probably on a Windows terminal
2076 with the Tcl/Tk implementation of \s-1XSPIN\s0.
2077 All functionality of \*V, however, is accessible from
2078 any plain ASCII terminal, and there is something to be
2079 said for directly interacting with the tool itself.
2081 The description in this paper gives a short walk-through of
2082 a common mode of operation in using the verifier.
2083 A more tutorial style description of the verification
2084 process can be found in [Ho93].
2085 More detail on the verification of large systems with the
2086 help of \*V's supertrace (bitstate) verification algorithm
2087 can be found in [Ho95].
2092 Random and interactive simulations (section 2.1),
2095 Generating a verifier (section 2.2),
2098 Compilation for different types of searches (section 2.3),
2101 Performing the verification (section 2.4),
2104 Inspecting error traces produced by the verifier (section 2.5),
2107 Exploiting partial order reductions (section 2.6).
2111 Random and Interactive Simulations
2113 Given a model in \*P, say stored in a file called
2115 the easiest mode of operation is to perform a random simulation.
2120 tells \*V to perform a random simulation, while printing the
2121 process moves selected for execution at each step (by default
2122 nothing is printed, other than explicit
2124 statements that appear in the model itself).
2125 A range of options exists to make the traces more verbose,
2126 e.g., by adding printouts of local variables (add option
2128 global variables (add option
2130 send statements (add option
2132 or receive statements (add option
2136 (with N any number) to fix the seed on \*V's internal
2137 random number generator, and thus make the simulation runs
2139 By default the current time is used to seed the random number
2143 spin -p -l -g -r -s -n1 spec
2146 If you don't like the system randomly resolving non-deterministic
2147 choices for you, you can select an interactive simulation:
2151 In this case you will be offered a menu with choices each time
2152 the execution could proceed in more than one way.
2154 Simulations, of course, are intended primarily for the
2155 debugging of a model. They cannot prove anything about it.
2156 Assertions will be evaluated during simulation runs, and
2157 any violations that result will be reported, but none of
2158 the other correctness requirements can be checked in this way.
2160 Generating the Verifier
2162 A model-specific verifier is generated as follows:
2166 This generates a C program in a number of files (with names
2170 Compiling the Verifier
2172 At this point it is good to know the physical limitations of
2173 the computer system that you will run the verification on.
2174 If you know how much physical (not virtual) memory your system
2175 has, you can take advantage of that.
2176 Initially, you can simply compile the verifier for a straight
2177 exhaustive verification run (constituting the strongest type
2178 of proof if it can be completed).
2181 \*C -o pan pan.c # standard exhaustive search
2183 If you know a memory bound that you want to restrict the run to
2184 (e.g., to avoid paging), find the nearest power of 2 (e.g., 23
2185 for the bound $2 sup 23# bytes) and compile as follows.
2187 \*C '-DMEMCNT=23' -o pan pan.c
2189 or equivalently in terms of MegaBytes:
2191 \*C '-DMEMLIM=8' -o pan pan.c
2193 If the verifier runs out of memory before completing its task,
2194 you can decide to increase the bound or to switch to a frugal
2195 supertrace verification. In the latter case, compile as follows.
2197 \*C -DBITSTATE -o pan pan.c
2200 Performing the Verification
2202 There are three specific decisions to make to
2203 perform verifications optimally: estimating the
2204 size of the reachable state space (section 2.4.1),
2205 estimating the maximum length of a unique execution
2206 sequence (2.4.2), and selecting the type of correctness
2208 No great harm is done if the estimates from the first two
2209 steps are off. The feedback from the verifier usually provides
2210 enough clues to determine quickly what the optimal settings
2211 for peak performance should be.
2215 For a standard exhaustive run, you can override the default choice
2216 for the size for the hash table ($2 sup 18# slots) with option
2222 selects $2 sup 23# slots.
2223 The hash table size should optimally be roughly equal to the number of
2224 reachable states you expect (within say a factor of two or three).
2225 Too large a number merely wastes memory, too low a number wastes
2226 CPU time, but neither can affect the correctness of the result.
2228 For a supertrace run, the hash table \f2is\f1 the memory arena, and
2229 you can override the default of $2 sup 22# bits with any other number.
2230 Set it to the maximum size of physical memory you can grab without
2231 making the system page, again within a factor of say two or three.
2234 if you expect 8 million reachable states and have access to at least
2235 8 million ($2 sup 23#) bits of memory (i.e., $2 sup 20# or 1 Megabyte of RAM).
2239 By default the analyzers have a search depth restriction of 10,000 steps.
2240 If this isn't enough, the search will truncate at 9,999 steps (watch for
2241 it in the printout).
2242 Define a different search depth with the -m flag.
2246 If you exceed also this limit, it is probably good to take some
2247 time to consider if the model you have specified is indeed finite.
2248 Check, for instance, if no unbounded number of processes is created.
2249 If satisfied that the model is finite, increase the search depth at
2250 least as far as is required to avoid truncation completely.
2252 If you find a particularly nasty error that takes a large number of steps
2253 to hit, you may also set lower search depths to find the shortest variant
2254 of an error sequence.
2258 Go up or down by powers of two until you find the place where the
2259 error first appears or disappears and then home in on the first
2260 depth where the error becomes apparent, and use the error trail of
2261 that verification run for guided simulation.
2263 Note that if a run with a given search depth fails to find
2264 an error, this does not necessarily mean that no violation of a
2265 correctness requirement is possible within that number of steps.
2266 The verifier performs its search for errors by using a standard
2267 depth-first graph search. If the search is truncated at N steps,
2268 and a state at level N-1 happens to be reachable also within fewer
2269 steps from the initial state, the second time it is reached it
2270 will not be explored again, and thus neither will its successors.
2271 Those successors may contain errors states that are reachable within
2272 N steps from the initial state.
2273 Normally, the verification should be run in such a way that no
2274 execution paths can be truncated, but to force the complete exploration
2275 of also truncated searches one can override the defaults with a compile-time
2278 When the verifier is compiled with that additional directive, the depth at
2279 which each state is visited is remembered, and a state is now considered
2280 unvisited if it is revisited via a shorter path later in the search.
2281 (This option cannot be used with a supertrace search.)
2283 Liveness or Safety Verification
2285 For the last, and perhaps the most critical, runtime decision:
2286 it must be decided if the system is to be checked for safety
2287 violations or for liveness violations.
2289 pan -l # search for non-progress cycles
2290 pan -a # search for acceptance cycles
2292 (In the first case, though, you must compile pan.c with -DNP as an
2293 additional directive. If you forget, the executable will remind you.)
2294 If you don't use either of the above two options, the default types of
2295 correctness properties are checked (assertion violations,
2296 completeness, race conditions, etc.).
2297 Note that the use of a
2301 labels requires the use of the
2303 flag for complete verification.
2307 restricts the search for liveness properties further under
2308 a standard \f2weak fairness\f1 constraint:
2310 pan -f -l # search for weakly fair non-progress cycles
2311 pan -f -a # search for weakly fair acceptance cycles
2313 With this constraint, each process is required to appear
2314 infinitely often in the infinite trace that constitutes
2315 the violation of a liveness property (e.g., a non-progress cycle
2316 or an acceptance cycle), unless it is permanently blocked
2317 (i.e., has no executable statements after a certain point in
2318 the trace is reached).
2319 Adding the fairness constraint increases the time complexity
2320 of the verification by a factor that is linear in the number
2321 of active processes.
2323 By default, the verifier will report on unreachable code in
2324 the model only when a verification run is successfully
2326 This default behavior can be turned off with the runtime option
2332 (The order in which the options such as these are listed is
2334 A brief explanation of these and other runtime options can
2335 be determined by typing:
2340 Inspecting Error Traces
2342 If the verification run reports an error,
2343 any error, \*V dumps an error trail into a file named
2347 is the name of your original \*P file.
2348 To inspect the trail, and determine the cause of the error,
2349 you must use the guided simulation option.
2354 gives you a summary of message exchanges in the trail, or
2358 gives a printout of every single step executed.
2359 Add as many extra or different options as you need to pin down the error:
2361 spin -t -r -s -l -g spec
2365 didn't change since you generated the analyzer from it.
2367 If you find non-progress cycles, add or delete progress labels
2368 and repeat the verification until you are content that you have found what
2369 you were looking for.
2371 If you are not interested in the first error reported,
2374 to report on specific others:
2378 ignores the first two errors and reports on the third one that
2380 If you just want to count all errors and not see them, use
2387 Internally, the verifiers produced by \*V deal with a formalization of
2388 a \*P model in terms of extended finite state machines.
2389 \*V therefore assigns state numbers to all statements in the model.
2390 The state numbers are listed in all the relevant output to make it
2391 completely unambiguous (source line references unfortunately do not
2392 have that property).
2393 To confirm the precise state assignments, there is a runtime option
2394 to the analyzer generated:
2396 pan -d # print state machines
2398 which will print out a table with all state assignments for each
2402 Exploiting Partial Order Reductions
2404 The search algorithm used by \*V is optimized
2405 according to the rules of a partial order theory explained in [HoPe94].
2406 The effect of the reduction, however, can be increased considerably if the verifier
2407 has extra information about the access of processes to global
2409 For this purpose, there are two keywords in the language that
2410 allow one to assert that specific channels are used exclusively
2411 by specific processes.
2412 For example, the assertions
2417 claim that the process that executes them is the \f2only\f1 process
2418 that will receive messages from channel
2420 and the \f2only\f1 process that will send messages to channel
2423 If an exclusive usage assertion turns out to be invalid, the
2424 verifier will be able to detect this, and report it as a violation
2425 of an implicit correctness requirement.
2427 Every read or write access to a message channel can introduce
2428 new dependencies that may diminish the maximum effect of the
2429 partial order reduction strategies.
2430 If, for instance, a process uses the
2432 function to check the number of messages stored in a channel,
2433 this counts as a read access, which can in some cases invalidate
2434 an exclusive access pattern that might otherwise exist.
2435 There are two special functions that can be used to poll the
2436 size of a channel in a safe way that is compatible with the
2441 returns true if channel
2445 returns true if channel
2447 contains at least one message.
2448 Note that the parser will not recognize the free form expressions
2452 as equally safe, and it will forbid constructions such as
2455 .CW !nempty(qname) .
2456 More detail on this aspect of the reduction algorithms can be
2461 For reference, the following table contains all the keywords,
2462 predefined functions, predefined variables, and
2463 special label-prefixes of the language \*P,
2464 and refers to the section of this paper in
2465 which they were discussed.
2470 _last (1.4) _pid (1.1.1) accept (1.3.2) active (1.1.1)
2471 assert (1.3.1) atomic (1.2.1) bit (1.1.2) bool (1.1.2)
2472 break (1.2.4) byte (1.1.2) chan (1.1.3) d_step (1.2.2)
2473 do (1.2.4) else (1.2.4) empty (1.1.3) enabled (1.4)
2474 end (1.3.2) fi (1.2.3) full (1.1.3) goto (1.2.2)
2475 hidden (not discussed) if (1.2.3) init (1.1.1) int (1.1.2)
2476 len (1.1.3) mtype (1.1.3) nempty (2.6) never (1.3.3)
2477 nfull (2.6) od (1.2.4) of (1.1.3) pc_value (1.4)
2478 printf (1.1.1) proctype (1.1.1) progress (1.3.2) run (1.1.1)
2479 short (1.1.2) skip (1.2) timeout (1.2.4) typedef (1.1.2)
2480 unless (1.2.5) xr (2.6) xs (2.6)
2489 Design and Validation of Computer Protocols,
2491 Prentice Hall, 1991.
2494 G.J. Holzmann, ``Tutorial: Design and Validation of Protocols,''
2496 Computer Networks and ISDN Systems,
2498 1993, Vol. 25, No. 9, pp. 981-1017.
2501 G.J. Holzmann and D.A. Peled, ``An improvement in
2502 formal verification,''
2504 Proc. 7th Int. Conf. on Formal Description Techniques,
2506 FORTE94, Berne, Switzerland. October 1994.
2509 G.J. Holzmann, ``An Analysis of Bitstate Hashing,''
2510 technical report 2/95, available from author.
2513 G.J. Holzmann, ``Software model checking: extracting
2514 verification models from source code,''
2516 Proc. Formal Methods in Software Engineering and Distributed
2519 PSTV/FORTE99, Beijng, China, Oct. 1999, Kluwer,pp. 481-497.