September 2003
Intermediate to advanced
608 pages
14h 14m
English
“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 ...
Read now
Unlock full access