Skip to content

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.

Notifications You must be signed in to change notification settings

Gulfam92/DistributedSystems-Algorithms-ModelChecking

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 

Repository files navigation

Project Description:

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.

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

No packages published

Languages