Repository logo
Collections
Browse
Statistics
  • English
  • हिंदी
Log In
New user? Click here to register.Have you forgotten your password?
  1. Home
  2. Theses and Dissertations
  3. M Tech Dissertations
  4. Modeling and Formal Verification of The Dining Philosophers Problem Using SPIN

Modeling and Formal Verification of The Dining Philosophers Problem Using SPIN

Files

202011054.pdf (467.06 KB)

Date

2022

Authors

Makvana, Kripalsinh

Journal Title

Journal ISSN

Volume Title

Publisher

Dhirubhai Ambani Institute of Information and Communication Technology

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.

Description

Keywords

Spin model�s, philosophers problem, modeling and verification

Citation

Makvana, Kripalsinh (2022). Modeling and Formal Verification of The Dining Philosophers Problem Using SPIN. Dhirubhai Ambani Institute of Information and Communication Technology. V, 17 p. (Acc. # T01040).

URI

http://ir.daiict.ac.in/handle/123456789/1120

Collections

M Tech Dissertations

Endorsement

Review

Supplemented By

Referenced By

Full item page
 
Quick Links
  • Home
  • Search
  • Research Overview
  • About
Contact

DAU, Gandhinagar, India

library@dau.ac.in

+91 0796-8261-578

Follow Us

© 2025 Dhirubhai Ambani University
Designed by Library Team