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 ...
Get Spin Model Checker, The: Primer and Reference Manual now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
