I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article for it. Are there any standard references on how to do model checking for Paxos?

  • 3
    $\begingroup$ Have you tried a Google search with the title of your question? There are several related articles. Have you read them? If they do not answer your question, please point out why. $\endgroup$ – Vijay D Jun 17 '13 at 2:49

You can find a formal model and proof of Paxos and Byzantine Paxos written by L. Lamport et al at http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html.

The model can be checked using the TLA+ toolbox.

Notice that the author of the Paxos algorithm, the formal model above, and even the TLA+ modeling language is the same person:)


I think you can get a better idea by referring the following paper, Model Checking for Programming Languages using VeriSoft by Patrice Godefroid

  • 1
    $\begingroup$ I have not downvoted but please avoid from providing such generic answers which are not specific to the question being asked. $\endgroup$ – Vijay D Jun 17 '13 at 2:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.