Summary In this paper, we extend work on model‐based testing for Apache ZooKeeper, to handle watchers (triggers) and improve scalability. In a distributed asynchronous shared storage like ZooKeeper, watchers deliver notifications on state changes. They are difficult to test because watcher notifications involve an initial action that sets the watcher, followed by another action that changes the previously seen state. We show how to generate test cases for concurrent client sessions executing against ZooKeeper with the tool Modbat. The tests are verified against an oracle that takes into account all possible timings of network communication. The oracle has to verify that there exists a chain of events that triggers both the initial callback and the subsequent watcher notification. We show in detail how the oracle computes whether watch triggers are correct and how the model was adapted and improved to handle these features. Together with a new search improvement that increases both speed and accuracy, we are able to verify large test setups and confirm several defects with our model.

Apache ZooKeeper is a distributed data storage that is highly concurrent and asynchronous due to network communication, testing such a system is very challenging. Our solution using the tool "Modbat" generates test cases for concurrent client sessions, and processes results from synchronous and asynchronous callbacks. We use an embedded model checker to compute the test oracle for non-deterministic outcomes, the oracle model evolves dynamically with each new test step. Our work has detected multiple previously unknown defects in ZooKeeper. Finally, a thorough coverage evaluation of the core classes show how code and branch coverage strongly relate to feature coverage in the model, and hence modeling effort.

Modbat makes testing easier by providing a user-friendly modeling language to describe the behavior of systems, from such a model, test cases are generated and executed. Modbat's domain-specific language is based on Scala, its features include probabilistic and non-deterministic transitions, component models with inheritance, and exceptions. We demonstrate the versatility of Modbat by finding a confirmed defect in the currently latest version of Java, and by testing SAT solvers.