In: IEEE Trans. on Parallel and Distributed Systems, Vol. 10, No. 7, pages 714-732. 1999.
Abstract: In this paper, we present a computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Colored Petri Nets (CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a significant increase in the number of states which can be analyzed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. OF-nets and OS-graphs are not our invention. Our contribution is the development of the tool and verification of the example, demonstrating how the method of occurrence graphs with symmetries can be put into practice.
Keywords: analysis of distributed systems, colored Petri nets, formal verification, high-level Petri nets, mutual exclusion, occurrence graphs, state spaces, symmetries.