Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV - Computer Science > Logic in Computer ScienceReport as inadecuate




Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV - Computer Science > Logic in Computer Science - Download this document for free, or read online. Document in PDF available to download.

Abstract: The finite intrinsic nature of the most distributed algorithms gives us thisability to use model checking tools for verification of this type ofalgorithms. In this paper, I attempt to use NuSMV as a model checking tool forverifying necessary properties of Peterson-s algorithm for leader electionproblem in a unidirectional asynchronous ring topology. Peterson-s algorithmfor an asynchronous ring supposes that each node in the ring has a unique IDand also a queue for dealing with storage problem. By considering that thequeue can have any combination of values, a constructed model for a ring withonly four nodes will have more than a billion states. Although it seems thatmodel checking is not a feasible approach for this problem, I attempt to useseveral effective limiting assumptions for hiring formal model checkingapproach without losing the correct functionality of the Peterson-s algorithm.These enforced limiting assumptions target the degree of freedom in the modelchecking process and significantly decrease the CPU time, memory usage and thetotal number of page faults. By deploying these limitations, the number ofnodes can be increased from four to eight in the model checking process withNuSMV.



Author: Amin Ansari

Source: https://arxiv.org/







Related documents