Model checking Paxos

Question

I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. But want to do testing via model check? Couldn't find correct article for it. Please share how to do about model checking in Paxos

Thanks

Answer 1

You could use the Spin Model checker to check an abstract description of the system.

For Java based implementations you can use Java Path Finder.

There is also mace, where you can implement and test distributed systems like Paxos, and it has some support to include C code.

Regards, Christian