English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

ZooKeeper is a coordination service, widely used as a backbone of variousdistributed systems. Though its reliability is of critical importance, testingis insufficient for an industrial-strength system of the size and complexity ofZooKeeper, and deep bugs can still be found. To this end, we resort to formalTLA+ specifications to further improve the reliability of ZooKeeper. Ourprimary objective is usability and automation, rather than full verification.We incrementally develop three levels of specifications for ZooKeeper. We firstobtain the protocol specification, which unambiguously specifies the Zabprotocol behind ZooKeeper. We then proceed to a finer grain and obtain thesystem specification, which serves as the super-doc for system development. Inorder to further leverage the model-level specification to improve thereliability of the code-level implementation, we develop the testspecification, which guides the explorative testing of the ZooKeeperimplementation. The formal specifications help eliminate the ambiguities in theprotocol design and provide comprehensive system documentation. They also helpfind critical deep bugs in system implementation, which are beyond the reach ofstate-of-the-art testing techniques. Our specifications have been merged intothe official Apache ZooKeeper project.

Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service