📄 whatispin.html
字号:
<html>
<body bgcolor="#ffffff">
<head>
<TITLE>Spin - Formal Verification</TITLE>
<img src=spinlogo.gif align=right>
<p>
<meta name="category" content="Verification,Software,Model Checking">
<meta name="description" content="Spin is a general tool for
verifying the correctness of distributed software (designs)
in a rigorous and mostly automated fashion.">
<meta name="keywords" content="software verification, model checking,
distributed systems, linear temporal logic, ltl, concurrency,
coordination, reactive systems, proof, on-the-fly, supertrace">
</head>
<h1><tt><font color="#FF0000">ON-THE-FLY, LTL MODEL CHECKING with SPIN
</font></tt></h1>
<h2><tt>Contents</tt></h2>
<ul><tt>
<li><a NAME=1 href="#A">General Description</a>
<li><a NAME=1 href="#B">Tool Documentation</a>
<li><a NAME=1 href="#S6">Theoretical Background</a>
<li><a NAME=1 href="#C">Spin NewsLetters</a>
<li><a NAME=1 href="#D">Spin Workshops</a>
</tt></ul>
<p>
For downloading and installation instructions, see Spin's
<A href="http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html">
Readme</a> file.
<p>
<a NAME="A">
<h2><tt>General Description</tt></h2></a>
Spin is a widely distributed software package that
supports the formal verification of distributed
systems. The software was developed at Bell Labs
in the formal methods and verification group starting
in 1980.
Some of the features that set this tool apart from
related verification systems are:
<ul>
<li>
Spin targets efficient <b>software</b> verification, not
hardware verification. Spin uses a high level language
to specify systems descriptions, called PROMELA (PROcess
MEta LAnguage).
Spin has been used to trace logical design errors in
distributed systems design, such as operating systems,
data communications protocols, switching systems,
concurrent algorithms, railway signaling protocols, etc.
The tool checks the logical consistency of a specification.
It reports on deadlocks, unspecified receptions, flags
incompleteness, race conditions, and unwarranted
assumptions about the relative speeds of processes.
<li>
Spin works <b>on-the-fly</b>, which means that it
avoids the need to construct of a global state graph, or a
Kripke structure, as a prerequisite for the verification of
any system properties.
<li>
Spin can be used as a full <b>LTL model checking</b> system, supporting all
correctness requirements expressible in linear time temporal logic,
but it can also be used as an efficient on-the-fly verifier for more
basic safety and liveness properties. Many of the latter properties
can be expressed, and verified, without the use of LTL.
<br>
Correctness properties can be specified as system
or process invariants (using assertions), or as general
linear temporal logic requirements (LTL), either directly
in the syntax of LTL, or indirectly as
<b>Büchi Automata</b> (called <b>never</b> claims).
<li>
Spin supports dynamically <b>growing and shrinking numbers of
processes</b>, using a rubber state vector technique.
<li>
Spin supports both <b>rendezvous</b> and <b>buffered
message passing</b>, and communication through <b>shared memory</b>.
Mixed systems, using both synchronous and asynchronous communications,
are also supported. Message channel identifiers for both rendezvous
and buffered channels, can be passed from
one process to another in messages.
<li>
Spin supports random, interactive and guided
simulation, and both exhaustive and partial proof techniques.
The tool is meant to scale smoothly with problem size, and is
specifically designed to handle even very large problem sizes.
<li>
To optimize the verification runs, the tool exploits efficient
partial order reduction techniques, and (optionally) BDD-like
storage techniques.
</ul>
To verify a design, a formal model is built using
PROMELA, Spin's input language.
PROMELA is a non-deterministic
language, loosely based on Dijkstra's guarded command
language notation and borrowing the notation
for i/o operations from Hoare's CSP language.
<p>
Spin can be used in three basic modes:
<ol>
<li>
as a simulator, allowing for rapid prototyping
with a random, guided, or interactive simulations
</li>
<li>
as an exhaustive state space analyzer,
capable of rigorously proving the validity of
user specified correctness requirements
(using partial order reduction theory
to optimize the search)
</li>
<li>
as a bit-state space analyzer that can
validate even very large protocol systems
with maximal coverage of the state space
(a proof approximation technique).
</li>
</ol>
<p>
The Spin software is written in ANSI standard C,
and is portable across all versions of the UNIX operating system.
It can also be compiled to run on any standard PC running
Linux, Windows95/98, or WindowsNT.
<p>
Downloading and installation instructions can be found in Spin's
<A href="http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html">
Readme</a> file.
<p>
<a NAME="B">
<h2><tt>Tool Documentation</tt></h2></a>
Documentation for Spin consists of
published papers and books, documentation distributed with
the Spin sources, online manual pages, the Spin Newsletters,
and the Spin Workshop proceedings.
The following list points to the online documentation; some
relevant papers and books can be found in the next section.
<ul>
<li><A href="http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html">
README.html</a> with the downloading and installation notes for Spin.
<p>
<li>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/index.html">
ONLINE REFERENCES</a>, including a semantics definition for the
specification language Promela, and manual pages
explaining the run-time options for Spin and for the
verifiers generated by Spin. Direct links to some of these manuals are:
<pre>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html">Manual.html</a> (language and tool)
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Quick.html">Quick.html</a> (by Rob Gerth, Eindhoven Univ./Intel)
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/GettingStarted.html">GettingStarted.html</a> (mostly on xspin)
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Roadmap.html">Roadmap.html</a> (mostly on spin)
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/WhatsNew.html">WhatsNew.html</a> (mostly on promela)
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Exercises.html">Exercises.html</a> (routine use)
</pre>
If you have Xspin working, start with
<tt>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/GettingStarted.html">GettingStarted</a>
</t>
If you have only plain spin working, start with
<tt>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Roadmap.html">Roadmap</a> and <a href="Exercises.html">Exercises</a>
</t>
In both cases proceed with
<tt>
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/Manual.html">Manual</a> and then <a href="http://cm.bell-labs.com/cm/cs/what/spin/Man/WhatsNew.html">WhatsNew.html</a>
</tt>
<p>
<li>
Short description of the
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Doc/roots.html">
origin of the tool.</a>
<p>
<li>
Modifications, updates, extensions, fixes of the Spin sources
are documented in the file Doc/V[123].Updates, which is part of
the main Spin distribution. The file Doc/V3.Updates for instance,
gives the update history for Spin version 3.
<p>
Included in the Spin distribution are also these files:
<pre>
Errata on the printed book: Doc/Book.Errata
Answers to selected exercises: Doc/Book.answers
More explanation on chapter 6: Doc/Book.Ch6.add
Spin examples used in the book: Doc/Book.samples
</pre>
More Promela examples can also be found in the Test
directory from the distribution, and in some of the papers below.
</ul>
<h2><tt><a name="S6">Theoretical Background</a></tt></h2>
<p>
<ul>
<li>
The on-the-fly verification algorithm used in Spin is described in
<pre>
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/popd.html">Design and Validation of Computer Protocols,</A>
Prentice Hall, New Jersey, 1991, ISBN 0-13-539925-4.
A paperback edition of the book is available from <a href="http://www.amazon.com">www.amazon.com.</a>
The text of the book is also available online in PDF format,
and in Postscript: <a href="http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91.html">Book91.html</a>
There is also a Japanese translation of the book.
</pre>
<li>
A more recent overview paper, with verification examples, is:
<pre>
<i>The Spin Model Checker</i>,
IEEE Trans. on Software Engineering,
Vol. 23, No. 5, May 1997, pp. 279-295.
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/gz/ieee97.ps.gz">(gzipped postscript)</a>
</pre>
<li>
The automata-theoretic foundation for Spin:
<pre>
<i>An automata-theoretic approach to automatic
program verification</i>,
by Moshe Y. Vardi, and Pierre Wolper,
Proc. First IEEE Symp. on Logic in Computer Science,
1986, pp. 322-331.
</pre>
<li>
The algorithm for bitstate hashing (optional in Spin for verifying
large problem sizes) is discussed in detail in:
<pre>
<i>An analysis of bitstate hashing</i>,
by G.J. Holzmann, Formal Methods in Systems Design, Nov. 1998
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/gz/fmsd98.ps.gz">(gzipped postscript)</a>
</pre>
<li>
The algorithm for partial order reduction is described in:
<pre>
<i>An Improvement in Formal Verification</i>,
by G.J. Holzmann and D. Peled,
Proc. FORTE 1994 Conference, Bern, Switzerland.
<a href="http://cm.bell-labs.com/cm/cs/what/spin/Doc/forte94a.ps.gz">(gzipped postscript)</a>
</pre>
<li>
The nested depth first search algorithm used in Spin:
<pre>
<i>On nested depth-first search</i>,
by G.J. Holzmann, D. Peled, and M. Yannakakis,
in <i>The Spin Verification System</i>, pp. 23-32,
American Mathematical Society, 1996. (Proc. of the 2nd Spin Workshop.)
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/gz/spin96a.ps.gz">(gzipped postscript)</a>
</pre>
<li>
Wolper's hash-compact method (optional in Spin version 3.2.1 and later)
was first presented and analyzed in:
<pre>
<i>Reliable hashing without collision detection</i>,
by Pierre Wolper and Dennis Leroy,
Proc. 5th Int. Conference on Computer Aided Verification, 1993,
Elounda, Greece, pp. 59-70.
</pre>
<li>
The algorithm for conversion of LTL to Buchi Automata
(in Spin terminology: never claims) is described in:
<pre>
<i>Simple on-the-fly automatic verification of
linear temporal logic</i>,
by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper,
Proc. PSTV 1995 Conference, Warsaw, Poland.
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/gz/ltl.ps.gz">(gzipped postscript)</a>
</pre>
<li>
The algorithm for storing reachable states with a minimized automaton
(new in Spin Version 3)
<pre>
<i>A Minimized automaton representation of reachable states</i>,
by A. Puri and G.J. Holzmann,
Software Tools for Technology Transfer, Vol. 3, No. 1, Springer Verlag.
<a href="http://cm.bell-labs.com/cm/cs/who/gerard/gz/sttt98.ps.gz">(gzipped postscript)</a>
</pre>
</ul>
<a NAME="C">
<h2><tt>NewsLetters</tt></h2></a>
<ul>
<li>The <A href="http://netlib.bell-labs.com/netlib/spin/news/news.html">Spin News Letters</A>
give updates on all changes, extensions, and revisions of the sources
since the book was published. You can subscribe to the email
distribution of these newsletters by sending a one-line message
<i>Subscribe</i> to
<pre>
<font color=red>spin_list@research.bell-labs.com</font>
</pre>
New releases of the Spin software are announced through these newsletters.
Occassionally the newsletters also include
answers to frequently asked questions, describe main new
applications or projects with Spin.
The newsletter serves mainly to establish
contacts between people using the Spin software in different
countries (there are users in over 40 different countries).
<p>
Anyone who wants to announce an extension of the basic Spin
software, to seek advice from or contacts with other Spin users,
to make available postscript versions of papers on Spin usage
(e.g. by anonymous ftp or as a URL on the internet) for feedback
or communication, can also submit such items for inclusion in
announcements to the mailing list.
</ul>
<a NAME="D">
<h2><tt>Annual Workshops</tt></h2></a>
<IMG SRC="spinner.gif" HEIGHT=51 WIDTH=48 ALIGN=right>
The next, 7th, Spin workshop
<ul>
<li> <a href="http://ase.arc.nasa.gov/spin2000">SPIN2000</a>
</ul>
will be held August 30-September 1, 2000 at Stanford University
near San Fransisco, CA, USA, organized by Klaus Havelund,
John Penix, and Willem Visser from NASA Ames Research Center
in California.
<br>
Online proceedings for previous workshops can be found in:
<ul>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws95/papers.html">Spin95-1, Oct. 1995, Montreal, Canada</a>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws96/papers.html">Spin96-2, Aug. 1996, Rutgers University, USA</a>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws97/papers.html">Spin97-3, Apr. 1997, Twente University, The Netherlands</a>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws98/program.html">Spin98-4, Nov. 1998, ENST, Paris, France</a>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws99a/program99.html">Spin99-5, July 1999, Trento, Italy</a>
<li> <a href="http://netlib.bell-labs.com/netlib/spin/ws99b/program99.html">Spin99-6, Sept. 1999, Toulouse, France</a>
</ul>
<p>
<hr>
<table cols=3>
<tr>
<tr>
<td valign=top width=200><tt>spin_list@research.bell-labs.com</tt></td>
<td valign=top width=200 align=center></td>
<td valign=top width=400 align=right>
<font size="3"><b><tt>(Page Updated: 21 June 1999)</tt></font></b></td></tr>
</table>
</body> </html>
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -