Model checking Paxos

2
votes

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

1
algorithmdistributed-systempaxosmodel-checkingconsensus
I suspect you'd have better luck on cstheory.stackexchange.com – btilly

1 Answers

1
votes

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