O'Reilly logo

Spin Model Checker, The: Primer and Reference Manual by Gerard J. Holzmann

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Chapter 1. Finding Bugs in Concurrent Systems

 

“For we can get some idea of a whole from a part, but never knowledge or exact opinion.”

 
 --(Polybius, ca. 150 B.C., Histories, Book I:4)

SPIN can be used to verify correctness requirements for systems of concurrently executing processes. The tool works by thoroughly checking either hand-built or mechanically generated models that capture the essential elements of a distributed systems design. If a requirement is not satisfied, SPIN can produce a sample execution of the model to demonstrate this.

There are two basic ways of working with SPIN in systems design. The first method, and the primary focus of this book, is to use the tool to construct verification models that can be shown to have all the ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required