Spin Model Checking

By Gerard J. Holzmann

Dr. Dobb's Journal October 1997

Figure 2: Automaton for one of the processes in the mutual-exclusion example.

Back to Article