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