The SPIN Model Checker: Primer and Reference Manual [Hardcover]

Gerard J. Holzmann (Author)

Book Description

ISBN-10: 0321228626 | ISBN-13: 978-0321228628 | Publication Date: September 14, 2003 | Edition: 1

The SPIN Model Checker is used for both teaching software verification techniques, and for validating large scale applications. The growing number of users has created a need for a more comprehensive user guide and a standard reference manual that describes the most recent version of the tool. This book fills that need. SPIN is used in over 40 countries. The offical SPIN web site, spinroot.com receives between 2500 and 3000 hits per day. It has been estimated that up to three-quarters of the $400 billion spent annually to hire programmers in the United States is ultimately spent on debugging.

Editorial Reviews

From the Back Cover

Master SPIN, the breakthrough tool for improving software reliability

SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen years ago. The tool has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.

This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most complex software verification problems.

• Sum Design and verify both abstract and detailed verification models of complex systems software
• Sum Develop a solid understanding of the theory behind logic model checking
• Sum Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the TimeLine editing tool
• Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source code

The SPIN software was awarded the prestigious Software System Award by the Association for Computing Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World Wide Web.

About the Author

DR. GERARD J. HOLZMANN is the principal designer of the SPIN system. Formerly Directory of Computing Principles Research at Bell Laboratories in Murray Hill, N.J., he recently joined NASA's Jet Propulsion Laboratory in Pasadena, CA, to help set up a new Laboratory for Reliable Software. Holzmann's earlier books include Design and Validation of Computer Protocols (Prentice Hall), and The Early History of Data Networks (IEEE CS Press).

See all Editorial Reviews

Product Details

• Hardcover: 608 pages
• Publisher: Addison-Wesley Professional; 1 edition (September 14, 2003)
• Language: English
• ISBN-10: 0321228626
• ISBN-13: 978-0321228628
• Product Dimensions: 9.6 x 7.3 x 1.1 inches
• Shipping Weight: 1.8 pounds
• Average Customer Review: 5.0 out of 5 stars  See all reviews (3 customer reviews)
• Amazon Best Sellers Rank: #1,474,921 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

24 of 25 people found the following review helpful:

5.0 out of 5 stars Essential reference for SPIN users, November 26, 2003

By 

Theo Ruys (Deventer, The Netherlands) - See all my reviews

This review is from: The SPIN Model Checker: Primer and Reference Manual (Hardcover)

If you are serious about using SPIN, this is the book that should be
on your desk. Highly recommended.

Model checking is all about finding bugs in software.
Whether you need to find bugs in the initial design of your software,
or want to find errors in your code automatically, model checking tools
can help you out. And among the many model checking tools available,
SPIN is arguably one the most powerful ones. And the good thing is:
SPIN is freely available and open source.

Powerful tools should be handled with care. And SPIN is not any
different. This book, by the principal designer of SPIN, however,
explains everything you need to know to use SPIN in the most
efficient way.

The book of course explains SPIN's modelling language Promela and the
many ways to specify properties to be checked with SPIN. The usage of
SPIN and its graphical interface Xspin are discussed in depth as well.
The book also shows you what's under the hood of SPIN. The basic

verification algorithms are explained and all optimization algorithms
which make SPIN such a cutting-edge tool. For advanced use of SPIN
(to squeeze out those last megabytes), it is important to have an
idea how the tool works.
Abstraction is the key activity in composing efficient models that
can be checked with SPIN. The book offers guidelines in how to make
abstractions of system designs, but also shows how to generate
Promela models from ANSI-C code.

The book is nicely structured into four parts: Intro, Foundation,
Practice, and Reference Material. This makes it easy to find the
information you are looking for.
Another nice thing about the book is that each chapter is concluded
with bibliographic notes which list the pointers to literature that
go even deeper into the subject of the particular chapter. The
chapters themselves are illustrated with many (real world) examples
and the book is very well written. And be sure to check out
Appendix B "The Great Debates" which discusses several "religious"
topics concerning concurrency theory.

A substantial part of the book (Reference Material, nearly 200 pages)
is devoted to a reference to all Promela statements and the various
SPIN options. Using the UNIX man-page style, the details of all features
are carefully explained. Especially for this part, I keep the book
within reach on my desk. Even after more than five years of experience
with SPIN, I occasionally need to know the exact semantics of some
Promela construct. And the book explains it well.

Although the book includes some introductionary chapters to SPIN, the
book shines as a reference to SPIN. People completely new to SPIN might
better start their journey at the SPIN's website: http://spinroot.com,
which - among other goodies - hosts some more gentle introductions
on SPIN. But for intermediate and advanced users of SPIN the book
is a must.

4 of 4 people found the following review helpful:

5.0 out of 5 stars enables programmatic verification of a design, February 4, 2006

By 

W Boudville (Terra, Sol 3) - See all my reviews
(VINE VOICE)    (TOP 1000 REVIEWER)    (HALL OF FAME REVIEWER)    (REAL NAME)   

This review is from: The SPIN Model Checker: Primer and Reference Manual (Hardcover)

If you are a programmer [and why else would you be reading this?], then you have experience in debugging conventional code, running on single CPU machines. But what about software running concurrently on several machines? There is an inherent non-determinacy that can cause debugging to be very awful.

In answer, Holzmann and others came up with the SPIN model. He is the main proponent and, fittingly, authored this standard text on it. The basic idea is to represent code by a logic model. Where the code might be already written, or, more usefully, not yet. That is to say, you are doing a top-down approach and working on a design.

The model is written in a special language. Then, the SPIN model checker can programmatically test this model for bugs. Especially in concurrent mode. En route, the book teaches you of the usefulness of finite state machines in modelling.

This programmatic testing is far more robust than manual inspection of the code. The book shows in detail how to use SPIN. The end result is an automated testing of your model. To be sure, you still have to map from your model to the actual code. But this can now be done in confidence that your design was correct.

1 of 5 people found the following review helpful:

5.0 out of 5 stars Executable example or killer application are needed., March 11, 2008

By 

kaizen (Japan) - See all my reviews

This review is from: The SPIN Model Checker: Primer and Reference Manual (Hardcover)

SPIN is an acronym for Simple Promela Interpreter.
Promela is a specification language in verification system, SPIN.
I am not a promela programer. I want to know executable example or killer application using Promela/SPIN.
For example, operating system, network protocols or real application should be written using Promela.
Then this book is the best book, who test the system.
There are many references of the promela syntax, grammer, notes and examples.