{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:48:49Z","timestamp":1771573729707,"version":"3.50.1"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,11,1]],"date-time":"2020-11-01T00:00:00Z","timestamp":1604188800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2020,11]]},"DOI":"10.1007\/s11390-020-0538-7","type":"journal-article","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T11:11:43Z","timestamp":1607339503000},"page":"1312-1323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Specification and Verification of the Zab Protocol with TLA+"],"prefix":"10.1007","volume":"35","author":[{"given":"Jia-Qi","family":"Yin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hui-Biao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Fei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,11,30]]},"reference":[{"key":"538_CR1","unstructured":"Burrows M. The chubby lock service for loosely-coupled distributed systems. In Proc. the 7th Int. Symposium on Operating Systems Design and Implementation, November 2006, pp.335-350."},{"key":"538_CR2","doi-asserted-by":"crossref","unstructured":"Junqueira F P, Reed B C. Brief announcement Zab: A practical totally ordered broadcast protocol. In Proc. the 23rd Int. Symposium on Distributed Computing, September 2009, pp.362-363.","DOI":"10.1007\/978-3-642-04355-0_39"},{"key":"538_CR3","unstructured":"Lamport L. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"key":"538_CR4","doi-asserted-by":"crossref","unstructured":"Junqueira F P, Reed B C, Serafini M. Zab: High-performance broadcast for primary-backup systems. In Proc. the 41st Int. Conference on Dependable Systems and Networks, June 2011, pp.245-256.","DOI":"10.1109\/DSN.2011.5958223"},{"key":"538_CR5","unstructured":"Hunt P, Konar M, Junqueira F P, Reed B. ZooKeeper: Wait-free coordination for Internet-scale systems. In Proc. the 2010 USENIX Annual Technical Conference, June 2010."},{"key":"538_CR6","unstructured":"Ongaro D, Ousterhout J K. In search of an understandable consensus algorithm. In Proc. the 2014 USENIX Annual Technical Conference, June 2014, pp.305-319."},{"key":"538_CR7","doi-asserted-by":"crossref","unstructured":"Lamport L, Malkhi D, Zhou L. Vertical paxos and primary-backup replication. In Proc. the 28th Annual ACM Symposium on Principles of Distributed Computing, August 2009, pp.312-313.","DOI":"10.1145\/1582716.1582783"},{"key":"538_CR8","doi-asserted-by":"crossref","unstructured":"Kuppe M A, Lamport L, Ricketts D. The TLA+ toolbox. In Proc. the 5th Workshop on Formal Integrated Development Environment, October 2019, pp.50-62.","DOI":"10.4204\/EPTCS.310.6"},{"key":"538_CR9","doi-asserted-by":"crossref","unstructured":"Lamport L, Matthews J, Tuttle M R, Yu Y. Specifying and verifying systems with TLA+. In Proc. the 10th ACM SIGOPS European Workshop, July 2002, pp.45-48.","DOI":"10.1145\/1133373.1133382"},{"key":"538_CR10","unstructured":"Paiva P Y A, Saotome O, Brandauer C. Specification and verification of a multi-agent coordination protocol with TLA+. In Proc. the 8th Brazilian Symposium on Computing Systems Engineering, November 2018, pp.207-212."},{"key":"538_CR11","doi-asserted-by":"crossref","unstructured":"Chaudhuri K, Doligez D, Lamport L, Merz S. Verifying safety properties with the TLA+ proof system. In Proc. the 5th Int. Joint Conference on Automated Reasoning, July 2010, pp.142-148.","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"538_CR12","doi-asserted-by":"crossref","unstructured":"Cousineau D, Doligez D, Lamport L, Merz S, Ricketts D, Vanzetto H. TLA + proofs. In Proc. the 18th Int. Symposium on Formal Methods, August 2012, pp.147-154.","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"538_CR13","unstructured":"EL-Sanosi I, Ezhilchelvan P D. Improving the latency and throughput of ZooKeeper atomic broadcast. In Proc. the 7th Imperial College Computing Student Workshop, September 2017, Article No. 3."},{"key":"538_CR14","doi-asserted-by":"crossref","unstructured":"EL-Sanosi I, Ezhilchelvan P D. Improving ZooKeeper atomic broadcast performance by coin tossing. In Proc. the 14th European Performance Engineering Workshop, September 2017, pp.249-265.","DOI":"10.1007\/978-3-319-66583-2_16"},{"key":"538_CR15","doi-asserted-by":"crossref","unstructured":"Batson B, Lamport L. High-level specifications: Lessons from industry. In Proc. the 1st Int. Symposium on Formal Methods for Components and Objects, November 2002, pp.242-261.","DOI":"10.1007\/978-3-540-39656-7_10"},{"key":"538_CR16","doi-asserted-by":"crossref","unstructured":"Newcombe C. Why Amazon chose TLA+. In Proc. the 4th Int. Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, June 2014, pp.25-39.","DOI":"10.1007\/978-3-662-43652-3_3"},{"issue":"4","key":"538_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon web services uses formal methods. Commun. ACM, 2015, 58(4): 66-73.","journal-title":"Commun. ACM"},{"issue":"2","key":"538_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1022969405325","volume":"22","author":"R Joshi","year":"2003","unstructured":"Joshi R, Lamport L, Matthews J, Tasiran S, Tuttle M R, Yu Y. Checking cache-coherence protocols with TLA+. Formal Methods Syst. Des., 2003, 22(2): 125-131.","journal-title":"Formal Methods Syst. Des."},{"key":"538_CR19","doi-asserted-by":"crossref","unstructured":"Lu T, Merz S, Weidenbach C. Towards verification of the pastry protocol using TLA+. In Proc. the 13th IFIP WG 6.1 International Conference and the 31st IFIP WG 6.1 Int. Conference, June 2011, pp.244-258.","DOI":"10.1007\/978-3-642-21461-5_16"},{"key":"538_CR20","doi-asserted-by":"crossref","unstructured":"Mokkedem A, Ferguson M J, de Johnston R. A TLA solution to the specification and verification of the RLP1 retransmission protocol. In Proc. the 4th Int. Symposium of Formal Methods Europe, September 1997, pp.398-417.","DOI":"10.1007\/3-540-63533-5_21"},{"key":"538_CR21","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.entcs.2009.05.054","volume":"240","author":"P Regnier","year":"2009","unstructured":"Regnier P, Lima G, Andrade A M S. A TLA+ formal specification and verification of a new real-time communication protocol. Electron. Notes Theor. Comput. Sci., 2009, 240: 221-238.","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"538_CR22","doi-asserted-by":"crossref","unstructured":"Chand S, Liu Y A, Stoller S D. Formal verification of Multi-Paxos for distributed consensus. In Proc. the 21st Int. Symposium on Formal Methods, November 2016, pp.119-136.","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"538_CR23","unstructured":"Gao Y, Li H, Li Y, Liu B, Wang X, Ruan H. Using TLA+ to specify leader election of Raft algorithm with consideration of leadership transfer in multiple controllers. In Proc. the 19th IEEE Int. Conference on Software Quality, Reliability and Security Companion, July 2019, pp.219-226."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0538-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-020-0538-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-020-0538-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T12:00:08Z","timestamp":1607342408000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-020-0538-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["538"],"URL":"https:\/\/doi.org\/10.1007\/s11390-020-0538-7","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11]]},"assertion":[{"value":"11 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}