Modeling and Formal Verification of The Dining Philosophers Problem Using SPIN

Abstract

The SPIN tool is used for verifying the correctness of the system. SPIN stands for simple PROMELA interpreter. It�s been used to find design problems in systems. The main idea behind the thesis is to provide an overview of the spin model�s architecture and functionality using the dining philosophers problem. The dining philosophers problem is a standard synchronization related concurrency problem. One solution to the problem is chosen for modeling and verification. For modeling, PROMELA is used, and SPIN is used for verification. SPIN can verify the model by running random simulations or creating a C program. It can do a complete verification to determine whether the system�s behavior is error-free or not with mathematical certainty. PROMELA is used for modeling system models in formal verification that allows for the dynamic development of concurrent processes and identifies interactions between processes in a distributed system. We examined and validated various properties of the Dining Philosophers Problem, such as the absence of deadlock and the absence of individual starvation. Using simulation, we determined the expected execution of the solution. There were no invalid end-states or non-progress cycles discovered.