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

Appendix A. Automata Products

 

“Beyond each corner new directions lie in wait.”

 
 --(Stanislaw Lec, 1909–1966)

SPIN is based on the fact that we can use finite state automata to model the behavior of asynchronous processes in distributed systems. If process behavior is formalized by automata, the combined execution of a system of asynchronous processes can be described as a product of automata.

Consider, for instance, a system A of n processes, each process given in automaton form, say: A1, A2, . . ., An. Next, consider an LTL formula f and the Büchi automaton B that corresponds to its negation ¬f. Using the automata theoretic verification procedure, we can check if A satisfies f by computing the global system automaton S

We use the operator ∏ here ...

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