Earthquake is a dynamic model checker (DMCK) for real implementations of distributed system (such as ZooKeeper).
http://osrg.github.io/earthquake/
Earthquakes permutes C/Java function calls, Ethernet packets, and injected fault events in various orders so as to find implementation-level bugs of the distributed system. When Earthquake finds a bug, Earthquake automatically records the event history and helps you to analyze which permutation of events triggers the bug.
Basically, Earthquake permutes events in a random order, but you can write your own state exploration policy (in Python) for finding deep bugs efficiently.
We have successfully found a distributed race condition bug of ZooKeeper using Earthquake. Please refer to example/zk-found-bug.ether for further information.
- How to set up the environment: doc/how-to-setup-env.md
- Example: Finding a distributed race condition bug of ZooKeeper: example/zk-found-bug.ether
Please see doc/arch.md.
We welcome your contribution to Earthquake. Please feel free to send your pull requests on github!
Copyright (C) 2015 Nippon Telegraph and Telephone Corporation. Released under Apache License 2.0.