English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

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.

Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV