In this project, a decentralized consensus algorithm, BenOr is implemented using PlusCal and TLA+. BenOr protocol is a binary protocol which decides commit or abort for each instance. For more details about the algorithm, please refer the proof document in the following link
[BenOr Research paper link] (https://www.researchgate.net/publication/255574059_Correctness_Proof_of_Ben-Or's_Randomized_Consensus_Algorithm).
In this project, to test the specs for different scenarios and analyze what can go wrong in distributed set up, TLA+ model checker is used for the validation and model checking.
Gulfam92/DistributedSystems-Algorithms-ModelChecking
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Implementation and validation of the model checking of various Distributed System algorithms like BenOr, Paxos, etc. using PlusCal and TLA+, also analyze the temporal and invariant properties.
Topics
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published