- Hardcover: 608 pages
- Publisher: Addison-Wesley Professional; 1 edition (September 14, 2003)
- Language: English
- ISBN-10: 0321228626
- ISBN-13: 978-0321228628
- Product Dimensions: 7.1 x 1.3 x 9.6 inches
- Shipping Weight: 1.8 pounds
- Average Customer Review: 5 customer reviews
Amazon Best Sellers Rank:
#2,733,924 in Books (See Top 100 in Books)
- #560 in Books > Engineering & Transportation > Engineering > Industrial, Manufacturing & Operational Systems > Industrial Technology
- #791 in Books > Computers & Technology > Programming > Software Design, Testing & Engineering > Testing
- #939 in Books > Computers & Technology > Networking & Cloud Computing > Data in the Enterprise > Client-Server Systems
Enter your mobile number or email address below and we'll send you a link to download the free Kindle App. Then you can start reading Kindle books on your smartphone, tablet, or computer - no Kindle device required.
To get the free app, enter your mobile phone number.
The SPIN Model Checker: Primer and Reference Manual 1st Edition
Use the Amazon App to scan ISBNs and compare prices.
Customers who bought this item also bought
What other items do customers buy after viewing this item?
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).
Browse award-winning titles. See more
Top customer reviews
There was a problem filtering reviews right now. Please try again later.
I found the Promela language funky, and the publicly available tools were reminscent of compiler technology 30 years ago. The book makes up for all this, though, because as a reference I could go between the examples and my code and figure out what was syntactically or semantically wrong.
The reference book was also helpful in suggesting debugging techniques to figure out what issues that the model was uncovering. But the most important part of this process was moving from interpreter to compiled model, and understanding how to use the trails and then later the compile-time options to track down issues and to get the verification to complete in a reasonable memory footprint. Compared to a few other formal verification tools I have looked at, the debugging and compilation options are better here. And the reference book explains these at the level of detail you need to know to use them effectively.
My only complaint with the book is that I bought a paperback version, and I used it so much over 3 weeks that the binding is already breaking down. My recommendation is that you spend more and buy the hardcover book, because you may spend a lot of time with it open!
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
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: [...]
which - among other goodies - hosts some more gentle introductions
on SPIN. But for intermediate and advanced users of SPIN the book
is a must.
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.
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.