In pervious versions of Spin, in a check for non-progress cycles (runtime option -l) also terminating sequences that did not pass through at least one progress label would be reported as errors. This aberration has been removed from version 2.

1.6.4 New Semantics of Timeout

In previous versions of Spin, if the system reached a valid end-state (e.g., a state in which all processes have stopped at a state that is marked with an end-label), no timeout options would be considered. This lead to unexpected behavior, for instance in cases where the initial system state was defined to be a valid end-state and all system behavior was meant to be triggered by an initial timeout. In Spin version 2 this will work correctly. The possibility of a timeout is now independent of the validity of the current system state as an end-state, as also required by Promela semantics.

1.6.5 New Randomizer for Simulations

The behavior of the default random number generators on some systems left much to be desired. The new version of Spin contains it's own random number generator, based on [PM88]. The specific way in which process actions are randomized within non-deterministic selections and in the process scheduling algorithm for the random simulations has also been improved.

1.6.6 More Robust Guided Simulation

The format of an error trail generated by the verifiers produced by earlier versions of Spin was defined in terms of states. The guided simulator, when trying to follow such a trail, could get confused, and declare to have `lost the trail' in cases where there would be more than one possible path from one state of the trail to the next. In the new version of Spin this is avoided by defining the trails in terms of the precise transitions to be executed along the trail. Spin version 2 also creates a separate trail file for each specification it analyzes, rather than using a single fixed name pan.trail.

In cases where more than one, numbered, trail file exists, (these can be generated with the runtime option -e), the user can select the trail file to be used in a guided simulation by adding the trail-file sequence number to the -t flag, e.g. as in

	$ spin -t4 spec

1.6.7 Improved Error Reporting

The syntax requirements of Promela have been relaxed a little, to avoid pedantic error reports about (especially) missing, or misplaced semi-colons. Some extra type checking is performed, and the error reports issued should be easier to interpret.

Starting with Version 3.0 also, Spin will mildly complain when data-types are used that needleslly increase the memory requirements of a verification run, e.g., when integer variables are used for booleans.

2. Changes in Promela

2.1 New Language Constructs

Nine new language constructs were added to Promela. In no particular order, the extensions are summarized below.

2.1.1 Else

The most frequently asked for language construct is now supported.

Syntax:

	else

The else statement can be used as the guard (i.e., the first statement) of an option sequence inside selection or iteration constructs. It is a syntax error to specify more than one else statement within a single selection or iteration construct.

Example:

	if

	:: a > b -> ...

	:: a == b -> ...

	:: else -> ...

	fi

2.1.2 Unless

A concept based on the comparable construct watching from Esterel [BCG86], [Hal93], and analogous concepts in languages such as Statecharts [Har87].

Syntax:

	B unless C

	{ B1; B2; B3 } unless { C1; C2 }

Example:

	A;

	do

	:: b1 -> B1

	:: b2 -> B2

	 ...

	od

	unless { c -> C };

	D

	A;

	do

	:: b1 -> B1

	:: b2 -> B2

	 ...

	:: c -> break

	od;

	C; D

The unless operator can be used in hierarchical proofs, in refinement proofs, and as a general escape mechanism.

2.1.3 d_step

d_step is a deterministic alternative to atomic, that can be supported more efficiently in the verifiers. For long code segments with deterministic local computations, the use of d_step instead of atomic can reduce the time requirements of a verification.

Syntax:

	d_step { ... }

Example:

	d_step {	/* initialize an array */

		i = 0;

		do

		:: i <  N -> buf[i] = i; i++

		:: i >= N -> break

		od; skip	/* skip is needed here */

	}

2.1.4 Sorted Send

In addition to the standard synchronous and asynchronous message passing primitives there are now two new types of operations on message channels: sorted send and random receive. We first discuss the sorted send operation.

Syntax:

	qname!!msg,...

The sorted send operation can be exploited by, for instance, listing an appropriate message field (e.g., a sequence number) as the first field of each message. Much administrative work with reshuffling messages to place them in some other order than the default order of arrival can thus be avoided.

2.1.5 Random Receive

The random receive operation is the logical counterpart of the sorted send operation.

Syntax:

	qname??msg,...

Applying sorted send and random receives together can be used to implement channels that buffer messages as sets. By storing the sets in numerical order, a significant reduction in the number of reachable states of a verification model can be obtained.

2.1.6 Hidden Data

Spin version 2 supports a new qualifier for data objects: hidden.

Syntax:

	hidden type_name variable_name, ...

Example:

	chan q = [8] of { byte };



	hidden byte a;

	 ...

	do

	:: q?a	/* flush the channel */

	:: empty(q) -> break

	od

A related new keyword from Version 3.0 is show. This keyword can also be prefixed to variable declarations, just like hidden, but it does not affect the semantics of of the model. It affects only the way in which data can be displayed in message sequence charts through Xspin or through Spin option -M (see Section 4).

2.1.7 Structures

Spin versions 2 and later support user-defined data types in the form of named structures. A Promela typedef definition can be used to introduce a new name for a list of data objects of predefined, or earlier defined, types. The new typename can then be used to declare and instantiate new data objects, which can be used in any context in the obvious ways.

Example:

	typedef Field {

	        short f;

	        byte  g

	};

	

	typedef Msg {

	        byte a[3];

	        int fld1;

	        Field   fld2;

	        chan p[3];

	        bit b

	};

	

	byte p;

	Msg foo;

	

	chan q = [2] of { byte, Msg };

	

	init {

		q!p,foo;

		q?p,foo

	}

2.1.8 Conditional Expressions

Conditional expressions, analogous to the C-syntax expr?expr:expr, are now supported. To avoid parsing conflicts, though, the syntax is different from C.

Syntax:

	(expr1 -> expr2 : expr3)

Semantics:
The expression has the value of expr2 when expr1 evaluates to a non-zero value, and the value of expr3 otherwise.

Example:

	chan q[3] = [0] of { mtype };



	sender:  	q[cond2 -> 1 : 2]!msg -> ...



	receiver:	q[cond1 -> 1 : 0]?msg -> ...

2.1.9 Active Proctypes

In earlier versions of Spin there was one predefined initial process, named init. The init process was the only process that could be active in the initial system state of a verification. In Spin version 2 there is a new keyword active that can be prefixed to any proctype definition. If the keyword is present, an instance of that proctype will be active in the initial system state. Multiple instantiations of the same proctype can be specified with an optional array suffix of the new keyword (separated from it by white space).

Example:

	active proctype A() {  ... }

	active [4] proctype B() {  ... }

A process can find out what its instantiation number is through the new predefined local variable _pid (see also Section 2.2.2). As before, process instantiation numbers begin at 1 for the first process run, and count up. At any point in time, only the process with the highest instantiation number can die (i.e., the most recently created child). Processes instantiation numbers can be recycled by the verifier. A never claim, if defined, always carries a zero or negative instantiation number.

2.2 New Predefined Variables and Functions

2.2.1 Support for Partial Order Reductions

Partial order reductions can only be applied to asynchronous send and receive operations if the processes that use these operations follow specific rules of usage, that must be asserted with the new keywords xr and xs. For example, the assertions

	xr q1;

	xs q2;

If an exclusive usage assertion turns out to be invalid, Spin will report this during verifications as the violation of a formal correctness requirement.

The partial order reduction algorithm can take advantage of the presence of the assertions by optimizing the reduction algorithm (nonetheless without losing its ability to detect and report all cases in which an assertion of this type could be violated). See [HP94] for more details.

Four additional functions on channels are predefined. They are given with their equivalents in terms of the existing function len, assuming that the size of the channel inspected here is QSZ (as defined by the user).

	nfull(q) 	len(q) < QSZ

	nempty(q)	len(q) > 0

	full(q)  	len(q) == QSZ

	empty(q) 	len(q) == 0

For the partial order reductions, any other test on the contents of a channel, such as q?[msg] or len(q), counts as both a read and a write access of the channel q, which may violate an earlier xr or xs assertion.

Restrictions:
The partial order reduction rules are not (yet) applied to synchronous send and receive operations.

2.2.2 Variables and Functions

There are two additional predefined variables (_pid and _last), and two more predefined functions (enabled() and pc_value()).

_pid is a predefined local variable that holds the instantiation number of a process.

Example:

	active [3] proctype A()

	{

		printf("hi, i am process number: %d\n", _pid)

	}

Example:

	never {

		/* claim that it is not possible for process 1

		 * to execute precisely every other step forever

		 */

	accept:

		do

		:: _last != 1 -> _last == 1

		od

	}

Example:

	never {

		/* claim that it is not possible for process 1

		 * to remain enabled without ever executing

		 */

	accept:

		do

		:: _last != 1 && enabled(1)

		od

	}

Example:

	never {

	        do

	        :: pc_value(1) <= pc_value(2)

	        && pc_value(2) <= pc_value(3)

	        && pc_value(3) <= pc_value(4)

	        && pc_value(4) <= pc_value(5)

	        od

	}

2.3 Changes in Semantics

In Spin Version 2.0, two small changes were made in the semantics of Promela programs. (Version 3.0 contains no further changes.)

2.3.1 Blocking Atomic Sequences

Until now it was considered an error if an atomic sequence contained any statement that could block the execution of the sequence. This caused much confusion and complicates modeling needlessly. Starting with Spin version 2, it is legal for an atomic sequence to block. If a process inside an atomic sequence blocks, control shifts non-deterministically to another process. If the statement later becomes executable, control can return to the process and the atomic execution of the remainder of the sequence resumed.

This change in semantics makes it relatively easy to model, for instance, co-routines where control does not pass from one process to another until and unless the running process blocks.

2.3.2 Rendez-Vous Operations

It is no longer allowed for a process to perform a rendez-vous handshake with itself, by placing the send and receive half of the rendez-vous in subsequent statements. Of course, it should never have been legal, but the verifiers produced by previous versions of Spin silently allowed it.

2.4 Changes in Syntax

2.4.1 Use of Mtypes

Starting with Spin version 1.6.0 (August 1994) it is legal, and recommended, to use mtype as a data type definition inside channel declarations. It allows the simulator to interpret message fields more predictably either symbolically (if defined as an mtype) or numerically (if defined otherwise).

Starting with version 2.7.8 mtype can also be used as a full first class data-type, just like bit, byte, short, and int. Variables of type mtype can be assigned symbolic values from the range declared in a standard mtype range definition (i.e.: mtype = { ... }; ). The value range of an mtype variable (global or local) equals to that of a byte variable (i.e., 0..255). Example:

	mtype = { full, empty, half_full };

	mtype glass = empty;

2.4.2 Remote Referencing

The adoption of the partial order reduction technique has inspired a revision of the use of remote referencing. It is no longer legal to reference the local variables of a process from within another process, or from within a never claim. No expressiveness is lost, since a local variable can always be made visible to all processes, and to the claim, by promoting it to a global variable.

The only valid type of remote referencing that remains is to poll the control state of a process. The syntax for this has changed. The expression:

	procname[pid]@label

2.4.3 A Few More C-isms

The use of var++ and var--, as abbreviations of respectively var = var + 1 and var = var - 1, is now supported.

3. Changes in Xspin

Xspin requires a standard X-11 windows environment, and a local installation of the Tcl/Tk toolset. On a Unix system, Xspin is started with the name of a file containing a Promela specification as an argument (or optionally without arguments). For instance as follows:

	$ xspin H4

	Spin Version 2.0 -- 1 January 1995

	xspin:  

Throughout the use of Xspin, a log of all actions performed is maintained on the standard output. It is handy to have this log visible during a session with Xspin. Syntax errors, unexpected events, time-consuming actions such as background compilations and verification runs, can be tracked only in the log. All entries in the log are prefixed by xspin: , to avoid confusion. In the example above, Xspin logged as the first action performed the successful opening of the file H4.

In Version 3, the log has become a standard part of the main xspin interface, so it is guaranteed to be always visible.

The main display of Xspin is text window that displays the file just opened. The file name itself is shown in the title bar. The view in the text window can be changed in three different ways: with the scroll bar, by typing a line number (followed by a ) in the box in the title bar marked Show line:, or by moving the mouse with the middle button down (on a three button mouse). This use of the middle mouse button works in almost all text displays maintained by Xspin.

There are several buttons in the title bar of the Xspin display. We will discuss these separately in the following subsections.

3.1 The File Menu

The file menu gives a choice of five actions: Clear, Load/Open, ReOpen, Save, and Quit.

Clear will remove the contents of the text window.
ReOpen will read in a fresh copy of the most recently opened file, discarding any textual changes that were made within the Xspin window since the last explicit Save action (see below).
Load/Open prompts the user with a browse list of all files in the current directory. Double-clicking any of the files will cause Xspin to open it, and place it in its text window. Of course, this only makes sense for Promela specifications. Scrolling in this browse list can again be done either with the scroll bar or with the middle mouse button. Double-clicking a directory name will cause the browse window to descend into that directory and display the files listed there. Double-clicking the first entry ( .. ) will cause the browse window to move up to the parent directory, and display the files listed there.
Save brings up a panel with an editable filename, and after clicking an OK button writes the current version of the file back into the file system. Xspin maintains it's own copy of the file in a special file called pan.in to avoid unintentionally overwriting the original source of the Promela specification. The source file itself is only (over)written with an explicit Save request through the File Menu.
Quit terminates the session of Xspin, without any further actions.

3.2 The Help Menu

The help menu gives a quick online review of the main usage of Spin and Xspin, and contains some hints on the setting of the parameters and options during verifications and simulations. The current entries in this menu are: Promela Usage, Xspin Usage, Simulation, Verification, FSM Views, LTL Formulae, and Reducing Complexity.

3.3 The Syntax-Check Button

Starting with Xspin version 3.0, there is a syntax check option. Pressing it will cause Xspin to invoke Spin (version 3.0 or later) to perform only a syntax check on the model. It does so by generating the pan.c file, but it will not continue with a compilation of this file when no syntax errors are found. The result of the check is displayed in a separate window, and lines in the source that contain syntax errors are highlighted.

3.4 The Simulate Panel

Clicking the Simulate button in Xspin brings up the simulate options panel. The main choice provided here is to perform either a random simulation or a guided simulation. A guided simulation can only be performed if a verification run was done first, and that verification run revealed an error in the protocol. The error trail can then be followed with a guided simulation. Xspin will know where to find the files, and will complain appropriately if they do not exist.

The tersest display mode would be to select a Time Sequence. The time sequence shows one column per process, with the actions of each process printed in the corresponding column. Each row is prefixed by the process instantiation number and the line number within the specification that contains the source line executed.

Selecting the option One Window per Process will cause the creation of a separate display window for each running process (the windows are created in a lazy fashion: not until a process executes its first statement in the trace).

The last option One Trace per Process similarly creates one window per process, and shows slightly more information, mostly for debugging purposes. If the Variable Values Panel is selected, a separate window is maintained with all local and global variable values. If the Selected Variables suboption is chosen, all variables of which the declaration is prefixed with the keyword show in the specification itself will be included in the MSC displays.

3.5 The Verify Panel

Clicking the Verify button brings up the verify panel. The panel gives visual control over most of the options that Spin provides for performing automated verifications. The initial settings are chosen in such a way that they will provide a reasonable starting point for most applications. A first verification run, therefore, can in most cases safely be performed by hitting the Run button in the lower right of the panel, without changing any of the default settings.

When a verification run completes, Xspin will attempt to provide hints about ways to proceed, based on the results obtained. No hints are provided when a clean run is performed, i.e., a complete exhaustive search, that did not reveal any errors. The default hint in cases like these is to consider whether or not the properties that were proven are the correct ones, and whether or not other properties still remain to be proven. In particular, proving liveness properties (properties of infinite behaviors as manifested by execution cycles) requires a separate verification run with the appropriate options selected in the Correctness Properties section of the validator panel. In the default verification run only safety properties (State Properties) are proven.

3.6 The LTL Panel

Brings up a panel with an entry box where an LTL formula can be entered in standard LTL syntax. The formula is translated into a never claim when a the return key is pressed, or the Translate/Convert button is selected, and can be saved into a file. See the Help menu for this option for more details.

3.7 The Fsm View Option

After selecting one of the proctypes that are part of the Promela specification, Xspin will produce and compile an executable verifier, and use the state machine output from the -d option to display a bubble-chart of its local states and transitions.

Moving the cursor over a state (i.e., a circle) will display the corresponding source line number and, simultaneously, highlight that line in the main text display window. Clicking at an edge will display the source text that corresponds to that edge. A state can be moved to a new location on the display with the left or middle mouse button down. The graph can be saved and printed with standard X utilities for (partial) screen dumps (e.g., with the grab option of the program xv), or converted into Postscript and then printed.

If Xspin detects that the graph layout program DOT is installed, an additional button is enabled that allows the state graph to be redrawn with that program (recommended). See the README.html file for details on the distribution of DOT.

4. Changes in Spin Version 3.0

The most important changes that were made in Version 3.0 are summarized below. Other, more minor, extensions, such as the addition of the Syntax Check option in Xspin, the extension of the -t option, or the new hints for frugal data-typing, have been mentioned in the main text.

4.1 Three New Options in Spin

4.1.1 Postscript output, option -M

A new option to basic Spin allows one to generate a standard Postscript file that contains the message sequence chart for a simulation. So far, this output could only be created with help from Xspin. Especially for long simulation trails (e.g., error trails produced with the verifier) Xspin can become quite slow when it attempts to build the message sequence charts. This has been improved a little in Xspin itself, but it is always much faster to use basic Spin to generate the Postscript files. For example,

	$ spin -t -M spec

	spin: trail ends after 2888 steps

	spin: wrote 3 pages into 'spec.ps'

	$ spin -n123 -M spec

	spin: wrote 7 pages into 'spec.ps'

4.1.2 Columnated output, option -c

A plain ASCII approximation of a message sequence chart can be generated with Spin option -c. It can be used just like option -M as shown above, except that the output appears on the standard output. For example:

	$ spin -c leader

	proc 1 = node

	proc 2 = node

	proc 3 = node

	proc 4 = node

	proc 5 = node

	q\p   0   1   2   3   4   5

	  1   .   .   .   .   .   out!one,4

	  2   .   out!one,one

	  3   .   .   out!one,two

	  2   .   .   in?one,one

	  4   .   .   .   out!one,winner

	  1   .   in?one,4

	  3   .   .   .   in?one,two

	  2   .   out!two,4

	  3   .   .   out!two,one

	  4   .   .   .   out!two,two

4.1.3 Reading LTL formula from a file

Some users have reported problems with non-standard quoting conventions on some systems that complicate the use of Spin's option -f. In version 3.0 there is a new option -F that takes a file-name argument, from which the formula will be read. For example:

	$ spin -f "[] (p U q)"

	 ...

	$ cat file

	[] (p U q)

	# an example LTL formula

	$ spin -F file

	 ...

4.2 Three Additions to Promela, and One Change

The inspiration for adding event trace definitions to Spin can be found in one of Spin's predecessors, from 1984, which was called trace. In trace, event trace defintions were specified with the keyword assert [H85,H87] (no longer free for this purpose in Spin). The current implementation of event traces matches the one from [H85,H87]. Their semantics, purpose, intended use are described below.

4.2.1 Event Traces

A simple example of an event trace definition that specifies the correctness requirement that send operations on the channel q1 alternate with receive operations on the channel q2, and furthermore that all send operations on q1 are (claimed to be) exclusively messages with value a, and all receive operations on channel q2 are exclusively messages with value b.

	trace {

		do

		:: q1!a; q2?b

		od

	}

• Each channel name that is used in an event trace definition is monitored for compliance with the structure and context of the complete trace.
• If only send operations on channel q appear in the trace, then only send operations on channel q are subject to the check. Similarly for receive operations. If both types appear, both are subject to the check, and they must occur in the relative order that the trace definition gives.
• An event trace definition may contain only send and receive operations (i.e., events), but it may contain any control flow construct. This means that no global or local variables can be used, no assignments, and no boolean tests can appear. The send and receive operations are restricted to simple sends or receives; they cannot be variations of sends and receives such as random receive, sorted send, receive test, etc.
• Message fields that must be matched in sends or receives must be specified with the help of mtype variables, or with constants. Message fields that have don't care values must be specified with the predefined write-only variable _ (see section 2.1.6).
• The sends and receives that appear in an event trace are called monitored events. These events do not generate new behavior, but they are required to match send or receive events on the same channels in the model, with matching constant and/or mtype parameters. The event occurs if the matching statement in the model is executed, i.e., it matches on a state transition, not a on state as such.
• There are two significant differences between an event trace and a never-claim definition:
  • An event trace matches event occurrences that can occur in the transitions between system states, where a never claim matches propositional values on the system states that exist between state transitions.

    Recall that a system state, for the purposes of verification with Spin, is a stable value assignment to variables, process-states, and message channels, that can be tested in boolean propositions. The transitions of a never claim are labeled with boolean propositions (expressions) that must evaluate to true in system states. The transitions of an event trace are labeled directly with monitored events that must occur in system transitions in the partial order that is stipulated in the trace definition.

  • An event trace monitors only a subset of the events in a system: only those of the types that are mentioned in the trace (i.e., the monitored events). A never claim, on the other hand, looks at all global systems states that are reached, and must be able to match the state assignments in the system at every state that is reached.

    An event trace automaton, just like a never claim automaton, has a current state, but it only executes transitions if a monitored event occurs in the system. (I.e., it does not execute synchronously with the system, as a never claim is required to do.)

• An event trace can be used to specify a type of correctness requirement that is hard to express elegantly with only state based reasoning. An event trace can, for instance, directly capture the occurence of receive events on rendez-vous channels. Such event occurrences are much harder to match with state propositions in never claims. Note also that LTL formulae cannot express all the properties that event traces can express (e.g. the alternation property shown as the small example above).
• An event trace causes a correctness violation if a send or receive action is executed in the system that is within the scope of the event trace, but that cannot be matched by a monitored event within that definition.
• The event trace can be negated by replacing the keyword trace with the keyword notrace. In this case a correctness violation is reported if the trace definition can be completed by reaching the endstate of the definition (the closing curly brace).
• One can use accept, progress, and end-state labels in event trace definitions, with the usual interpretation.

4.2.2 The keyword show

This keyword has no semantic content, but only serves to allow Xspin (and Spin's Postscript output option -M) to determine which variables should be tracked and included in message sequence chart displays. The value of any variable of which the declaration is prefixed with the keyword show is updated in these displays. The method of use is identical to that for the keyword hidden (section 2.1.6).

4.2.3 True and False

The symbolic names true and false are now recognized by the Spin parser as predefined constants with values 1 and 0 respectively.

4.2.4 Atomics inside Atomics

The Spin parser no longer rejects the use of an atomic sequence that is contained within another atomic or d_step sequence. They are accepted as redundant, but harmless.

4.3 A New State Compression Option

One of the main new additions to Spin version 3.0 is a new state compression algorithm that is based on the representation of the state space by a minimized automaton, much like a BDD. Instead of storing states explicitly, Spin constructs and updates a recognizer for states, and keeps it in minimal form. To enable the option, compile the verifier in pan.c with the directive -DMA=N, where N is the maximum length of the state vector you expect. The run will abort if the guess for the state vector size is too small (and will run somewhat inefficiently if it is too large). The new algorithm, and its performance, is described in detail in [HP97].

The automaton based representation can be considerably smaller than an exhaustive state space representation, but it can also be considerably more time consuming. Both these features imply that a checkpoint update and recovery option is both possible and desirable. To enable checkpointing, compile pan.c with the directive -DW_XPT. (By default this writes out a checkpoint file after every multiple of one million states stored. To restart an aborted run from a checkpoint file, recompile pan.c with directive -DR_XPT.) As may be expected, the creation and updating of the checkpoint files slows down the verification process.

4.4 New Treatment of Process Recycling

Process death is a conditionally safe action for the enforcement of the partial order reduction rules from [HP94]. The safety condition has two parts:

• The dying process is the youngest process in the system (i.e., it is the most recently created process that is still running), and
• There are fewer than the maximum number of processes (256) currently running.

The two conditions imply that the process death action can not enable the execution of run statements, but it can enable other process deaths (i.e., of another process that now become youngest). The sequence of process death operations remains fixed to the reverse order of creation. i.e., process death operations cannot be reordered. The change has the desirable effect that a process death is forceed as quickly as possible. Allowing process death to be postponed arbitrarily long tends to create articifial execution scenarios where the number of active processes can grow without bound.

This change partly reverses a decision made earlier in Spin version 2.8.5. Compatibility with Spin versions from 2.8.5-2.9.7 on this issue can be restored by compiling pan.c with -DGLOB_ALPHA .

5. In Conclusion

Spin is intended to be both a testbed for the development and evaluation of new verification techniques, and it is meant to present a robust and reliable environment for performing verifications of concurrent systems. If the system is to live up to its promise, therefore, it will continue to evolve. Users can subscribe to a mailing list that will announce all new releases of the software. (See the README.html file from the distribution.)

Apart from further algorithmic improvements, it is also anticipated that the language Promela will mature further towards a more complete systems specification language. The existing version of Spin is meant to provide a stable foundation for all future work. None of the existing functionality is likely to be affected by future revisions, and will continue to be supported.

Acknowledgements

The design and implementation of the Spin model checker is based on contributions, ideas, and inspiration from many friends and colleagues over a long period of time, most notably Costas Courcoubetis, Peter Van Eijk, Michael Ferguson, Rob Gerth, Patrice Godefroid, Doug McIlroy, Doron Peled, Rob Pike, Anuj Puri, Jim Reeds, Moshe Vardi, Pierre Wolper, and Mihalis Yannakakis.

References

[AD94] R. Alur and D. L. Dill, ``A theory of timed automata,'' Theoretical Computer Science, 126, pp. 183-235, 1994.

[BCG86] G. Berry, P. Couronne and G. Gonthier, ``Synchronous Programming of Reactive Systems: An Introduction to ESTEREL,'' Proc. 1st Franco-Japanese Symp. on Programming of Future Generation Computers, 1986, Tokyo. pp. 35-56. Ed. K. Fuchi, M. Nivat. North Holland Publ.

[PC95] C-T. Chou, and D. Peled, ``Verifying a Model-Checking Algorithm,'' Proc. TACAS'96, Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, March 1996. LNCS 1055, Springer Verlag, 1995.

[C74] Y. Choueka, ``Theories of automata on @omega@-tapes: a simplified approach,'' Journal of Computer and System Science 8 (1974), 117-141.

[ClEm81] E. M. Clarke and E. A. Emerson, ``Characterizing properties of parallel programs as fixpoints,'' 7th Int. Coll. on Automata, Languages and Programming. LNCS 85, 1981.

[CVWY92] C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, ``Memory efficient algorithms for the verification of temporal properties,'' Formal Methods in Systems Design I, 1992, pp. 275-288.

[GH93] P. Godefroid and G. J. Holzmann, ``On the verification of temporal properties,'' Proc. IFIP/WG6.1 Symp. on Protocols Specification, Testing, and Verification, PSTV93, Liege, Belgium, June 1993.

[Haj78] J. Hajek, ``Automatically verified data transfer protocols,'' Proc. 4th ICCC, 1978, Kyoto, pp. 749-756.

[Hal93] N. Halbwachs, ``Synchronous programming of reactive systems,'' Kluwer Academic Publishers, 1993.

[Har87] D. Harel, ``Statecharts: A visual formalism for complex systems,'' Science of Computer Programming vol 8, 1987, pp 231-274.

[H81] G. J. Holzmann, ``PAN - a protocol specification analyzer,'' Bell Laboratories Technical Memorandum, TM81-11271-5, May 1981.

[H83] G. J. Holzmann, R. A. Beukers, ``The PANDORA Protocol Development System,'' Proc. 3rd Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Eds. H. Rudin and C. West, pp. 357--369, North Holland Publ. Co., June, 1983.

[H85] G. J. Holzmann, ``Tracing protocols,'' AT&T Techn. Journal, Vol 64, No. 10, Dec. 1985.

[H87] G. J. Holzmann, ``Automated protocol validation in Argos, assertion proving, scatter searching,'' IEEE Trans. on Software Eng., Vol SE-13, No 6, June 1987, pp. 683-696.

[H88] G. J. Holzmann, ``An improved reachability analysis technique,'' Software Practice and Experience, Vol. 18, No. 2, pp. 137-161, Feb. 1988.

[H89] G. J. Holzmann, J. Patti, ``Validating SDL Specifications: An Experiment,'' Proc. 9th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Ed. C. Vissers and E. Brinksma, Twente, Neth., June, 1989.

[H91] G. J. Holzmann, ``Design and Validation of Computer Protocols,'' Prentice Hall, 1991.

[HP94] G. J. Holzmann and D. Peled, ``An improvement in formal verification,'' Proc. 7th Int. Conf. on Formal Description Techniques, FORTE94, Berne, Switzerland. October 1994.

[GPVW95] R. Gerth, D. Peled, M. Vardi, P. Wolper, ``Simple on-the-fly automatic verification of linear temporal logic,'' Proc. PSTV95 Conference, Warsaw Poland, 1995.

[H95] G. J. Holzmann, ``An analysis of bitstate searching,'' Proc. IFIP/WG6.1 Symp. on Protocols Specification, Testing, and Verification, PSTV95, Warsaw, Poland, June 1995.

[HPY96] G. J. Holzmann, D. Peled, and M. Yannakakis, ``On nested depth-first search,'' Proc. 2nd Spin Workshop, American Mathematical Society, DIMACS/32. October 1996.

[H97a] G. J. Holzmann, ``State compression in Spin,'' Proc. 3rd Spin Workshop, Twente University, April 1997.

[H97b] G. J. Holzmann, ``The model checker Spin,'' IEEE Trans. on Software Engineering, Vol. 23, No. 5.

[HP97] G. J. Holzmann and A. Puri, ``A minimized automaton representation of reachable states,'' Technical report, submitted for publication.

[H98] G. J. Holzmann, ``The Verification of Concurrent Systems,'' Course Notes 1994-1996. (To be published).

[KR88] B. W. Kernighan and D. M. Ritchie, ``The C Programming Language,'' 2nd Edition, Prentice Hall, 1988.

[PM88] S. K. Park and K. W. Miller, ``Random number generators: good ones are hard to find,'' Comm. of the ACM, Vol 31, No. 10, Oct. 1988, pp. 1192-1201.

[P94] D. A. Peled, ``Combining partial order reductions with on-the-fly model checking,'' Proc. 6th Int. Conf. on Computer Aided Verification, CAV94, Stanford, Ca., June 1994.

[Qu82] J. P. Queille, ``Le systeme C\ësar: description, sp\ëcification et analyse des applications r\ëparties,'' Ph.D. Thesis, June 1982, Computer Science Dept., Univ. Grenoble, France.

[W78] C. H. West, ``General Technique for Communications Protocol Validation,'' IBM Journal of Research and Development, Vol 22, No. 4, p. 393, 1978.

Summary of Compiler Directives

There are four directives that can be used for compiling the Spin sources itself. These should never be needed by Spin users, only (once) by someone recompiling and installing Spin from its sources.

Directives for Compiling Spin itself

NXT	if defined, the NEXT operator X  can be used

	in LTL formulae; risky, not compatible with partial

	order reductions

PC	required when compiling Spin on a PC

PRINTF	if defined, printf statements in the model are enabled

	during the verification process (not recommended)

SOLARIS	when compiling Spin on a Sun Solaris system

The remaining tables give optional directives for compiling the verifiers that are generated by Spin. Traditionally these are stored in a file named pan.c (with a number of dependent files). Usage of the directives below is always optional, and typically of the form:

	$ spin -a spec

	$ cc -o pan -DNOBOUNDCHECK pan.c

Directives Supported by Xspin

BITSTATE	use supertrace/bitstate instead of exhaustive exploration

MEMCNT=N	set upperbound to the amount of memory that can be allocated

	usage, e.g.: -DMEMCNT=20  for a maximum of $2 sup 20# bytes

NOCLAIM	exclude the never claim from the verification, if present

NOFAIR	disable the code for weak-fairness (is faster)

NOREDUCE	disables the partial order reduction algorithm

NP	enable non-progress cycle detection (option -l),

	replacing option -a for acceptance cycle detection

PEG	add complexity profiling (transition counts)

SAFETY	optimize for the case where no cycle detection is needed

	(faster, uses less memory, disables both -l and -a)

VAR_RANGES	compute the effective value range of variables

	(restricted to the interval 0..255)

CHECK	generate debugging information (see also below)

Directives Related to Partial Order Reduction

CTL	allow only those reductions that are consistent with

	branching time logics like CTL (i.e., the persistent

	set contains either one or all transitions)

GLOB_ALPHA	consider process death a global action (for compatibility

	with versions of Spin between 2.8.5 and 2.9.7)

NIBIS	apply a small optimization of partial order reduction

	(sometimes faster, sometimes not...)

XUSAFE	disable validity checks of x[rs] assertions (faster,

	and sometimes useful if the check is too strict, e.g.

	when channels are passed around as process parameters)

Directives to Increase Speed

NOBOUNDCHECK	don't check array bound violations (faster)

NOCOMP	don't compress states with fullstate storage

	(faster, but not compatible with liveness unless -DBITSTATE)

NOSTUTTER	disable stuttering rules (warning: changes semantics)

	stuttering rules are the standard way to extend a finite

	execution sequence into and infinite one, to allow for

	a consistent interpretation of B\(u"chi acceptance rules

Directives to Reduce Memory Use

COLLAPSE	a state vector compression mode; collapses state vector sizes

	by up to 80% to 90% (see Spin97 workshop paper)

	variations: add -DSEPQS or -DJOINPROCS (off by default)

MA=N	use a minimized DFA encoding for the state space, similar

	to a BDD, assuming a maximum of N bytes in the state-vector

	(this can be combined with -DCOLLAPSE for greater effect in

	cases when the original state vector is long)

Directives Reserved for Use When Prompted by Spin

NFAIR=N	allocates memory for enforcing weak fairness

	usage, e.g.: -DNFAIR=3	(default is 2)

VECTORSZ=N	allocates memory (in bytes) for state vector

	usage, e.g.: -DVECTORSZ=2048	(default is 1024)






Directives For Debugging Spin Verifiers




VERBOSE	adds elaborate debugging printouts

CHECK	more frugal debugging printouts

SVDUMP	if defined, adds an option -pN to the runtime verifiers to

	produce a file sv_dump at the end of the run, with a

	binary representation of all states, using a fixed size of

	N bytes per state.  (see also SDUMP below)

SDUMP	if used in addition to CHECK: adds ascii dumps of state vectors

	to verbose output (i.e., an ascii version of SVDUMP)







Directives for Experimental Use




BCOMP	when in BITSTATE mode, this computes hash functions over

	the compressed state-vector (compressed with byte-masking)

	in some cases, this can improve the coverage

COVEST	compiles in extra code for giving a coverage estimate

	at the end of BITSTATE runs, defined by Uli Stern.

	must compile pan.c with -lm in this case.

HYBRID_HASH	can shave a word (4 bytes) from every state vector,

	in 25% of the cases...

	when the state vector is 1 byte longer than a multiple of 4

	the memory allocator ends up adding 3 dummy bytes to secure

	memory alignment.  to avoid this, the HYBRID_HASH mode will

	take away 1 byte from the state vector, and use it as part

	of the hash -- this causes more collisions, but preserves

	correct exhaustive exploration - and saves 4 bytes per stored

	state in memory...

NOVSZ	risky - removes 4 bytes from state vector - its length field.

	in most cases this is redundant - so when memory is

	tight in fullstate storage, try this mode.

	if the number of states stored changes when -DNOVSZ is

	used, the information wasn't redundant...  (safety checks

	will still be valid, but liveness checks may then fail)

	NOVSZ cannot be combined with COLLAPSE

PRINTF	enables printfs during verification runs (Version 2.8

	and later -- earlier versions always left these enabled)

RANDSTORE	when in BITSTATE mode, use for instance -DRANDSTORE=33 to

	reduce the probability of storing the bits in the hasharray

	to 33%. the value assigned must be between 0 and 99

	low values increase the amount of work done (time complexity)

	and increase the effective coverage for large state spaces.

	most useful in sequential bitstate hashing runs to improve

	the accumulative coverage of all runs significantly.

REACH	guarantee absence of errors within the -m depth-limit

	(described in more detail in Newsletter 4 and in

	the V2.Updates notes for Version 2.2.)

W_XPT=N	in combination with MA, write checkpoint files every multiple

	of N states stored

R_XPT	in combination with MA, restart a verification run from the

	last checkpoint file written, can be combined with W_XPT















Spin Online References


Promela Manual Index


Promela Grammar


Spin HomePage







(Page Updated: 27 August 1997)