Please use this identifier to cite or link to this item:
http://drsr.daiict.ac.in//handle/123456789/1120
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Bhateja, Puneet | - |
dc.contributor.author | Makvana, Kripalsinh | - |
dc.date.accessioned | 2024-08-22T05:21:05Z | - |
dc.date.available | 2024-08-22T05:21:05Z | - |
dc.date.issued | 2022 | - |
dc.identifier.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). | - |
dc.identifier.uri | http://drsr.daiict.ac.in//handle/123456789/1120 | - |
dc.description.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. | - |
dc.publisher | Dhirubhai Ambani Institute of Information and Communication Technology | - |
dc.subject | Spin model�s | - |
dc.subject | philosophers problem | - |
dc.subject | modeling and verification | - |
dc.classification.ddc | 813.54 MAK | - |
dc.title | Modeling and Formal Verification of The Dining Philosophers Problem Using SPIN | - |
dc.type | Dissertation | - |
dc.degree | M. Tech | - |
dc.student.id | 202011054 | - |
dc.accession.number | T01040 | - |
Appears in Collections: | M Tech Dissertations |
Files in This Item:
File | Size | Format | |
---|---|---|---|
202011054.pdf | 467.06 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.