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 7. PROMELA Semantics

 

The whole is often more than the sum of its parts.

 
 --(Aristotle, Metaphysica, 10f–1045a, ca. 330 B.C.)

As we have seen in the earlier chapters, a SPIN model can be used to specify the behavior of collections of asynchronously executing processes in a distributed system. By simulating the execution of a SPIN model we can in principle generate a large directed graph of all reachable system states. Each node in that graph represents a possible state of the model, and each edge represents a single possible execution step by one of the processes. PROMELA is defined in such a way that we know up-front that this graph will always be finite. There can, for instance, be no more than a finite number of processes and message ...

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