To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
Formal Verification of Ring-based Leader Election Protocol using Predicate Diagrams |
|
Author |
Cecilia E. Nugraheni |
| Citation |
Vol. 9 No. 8 pp. 1-8 |
|
Abstract |
Leader election is one of fundamental tasks in distributed computing. The objective of the protocol is for the processes among themselves to establish a designated process, called the leader. There are two basic properties that the leader election implementation needs to obey: (1) safety: it is never the case that there are two or more leaders at the same time and (2) liveness: in a stable situation (i.e. processes stop dying for a while), a leader will eventually be elected. In this paper we considered a ring-based leader election protocol proposed by Chang and Roberts. We have proven or verified that this protocol satisfies the both properties. The proof is done by viewing the distributed systems as parameterized systems and using a class diagram called predicate diagrams* to do the verification. We use TLA* for formalization and use TLA+ style for writing specifications. |
|
Keywords |
Leader election protocol, distributed systems, verification, TLA* TLA+, predicate diagrams* |
|
URL |
