Customer Reviews

The SPIN Model Checker: Primer and Reference Manual

5 star:		(3)
4 star:		(0)
3 star:		(0)
2 star:		(0)
1 star:		(0)

 

 

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.

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.

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.