ZooKeeper is a coordination service, widely used as a backbone of various distributed systems. Though its reliability is of critical importance, testing is insufficient for an industrial-strength system of the size and complexity of ZooKeeper, and deep bugs can still be found. To this end, we resort to formal TLA+ specifications to further improve the reliability of ZooKeeper. Our primary objective is usability and automation, rather than full verification. We incrementally develop three levels of specifications for ZooKeeper. We first obtain the protocol specification, which unambiguously specifies the Zab protocol behind ZooKeeper. We then proceed to a finer grain and obtain the system specification, which serves as the super-doc for system development. In order to further leverage the model-level specification to improve the reliability of the code-level implementation, we develop the test specification, which guides the explorative testing of the ZooKeeper implementation. The formal specifications help eliminate the ambiguities in the protocol design and provide comprehensive system documentation. They also help find critical deep bugs in system implementation, which are beyond the reach of state-of-the-art testing techniques. Our specifications have been merged into the official Apache ZooKeeper project.

翻译：ZooKeeper是一种协调服务，被广泛用作各类分布式系统的核心支柱。尽管其可靠性至关重要，但对于ZooKeeper这样规模和复杂度的工业级系统而言，仅靠测试并不足够，仍可能发现深层缺陷。为此，我们借助形式化的TLA+规约来进一步提升ZooKeeper的可靠性。我们的主要目标是易用性和自动化，而非完全验证。我们为ZooKeeper逐步开发了三个层次的规约。首先，我们获得了协议规约，该规约清晰定义了ZooKeeper背后的Zab协议。随后，我们进行更细粒度的建模，得到系统规约，该规约作为系统开发的超级文档。为了进一步利用模型级规约提升代码级实现的可靠性，我们开发了测试规约，用于指导ZooKeeper实现的探索性测试。这些形式化规约有助于消除协议设计中的歧义，并提供全面的系统文档。此外，它们还帮助发现了系统实现中的关键深层缺陷，这些缺陷超出了现有最先进测试技术的检测范围。我们的规约已被纳入Apache ZooKeeper官方项目。