The SPIN Model Checker: Primer and Reference Manual (paperback) (Anglais) Broché – 4 septembre 2003
- Choisissez parmi 17 000 points de collecte en France
- Les membres du programme Amazon Prime bénéficient de livraison gratuites illimitées
- Trouvez votre point de collecte et ajoutez-le à votre carnet d’adresses
- Sélectionnez cette adresse lors de votre commande
Description du produit
Présentation de l'éditeur
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
Quatrième de couverture
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.
Aucun appareil Kindle n'est requis. Téléchargez l'une des applis Kindle gratuites et commencez à lire les livres Kindle sur votre smartphone, tablette ou ordinateur.
Pour obtenir l'appli gratuite, saisissez votre numéro de téléphone mobile.
Détails sur le produit
Si vous vendez ce produit, souhaitez-vous suggérer des mises à jour par l'intermédiaire du support vendeur ?
|5 étoiles (0%)|
|4 étoiles (0%)|
|3 étoiles (0%)|
|2 étoiles (0%)|
|1 étoile (0%)|
Commentaires client les plus utiles sur Amazon.com
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.