Model Checking Systems of Replicated Processes with Spin

This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking distributed systems with several instances of the same process. Our technique uses symmetry which appears in the system. Exchanging those instances is not as simple as it seems, because there can be a lot of references to process locations in the system. We implemented a solution using the Spin model checker, and added two keywords to the Promela language to handle these new concepts.

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Fabrice Derepas, Paul Gastin
• Keywords: Reduction Technique, SPIN 2001, State Explosion Problem, Technique Uses Symmetry, Theoretical Computer Science