{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:16:02Z","timestamp":1771024562962,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":42,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819986637","type":"print"},{"value":"9789819986644","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,12,15]],"date-time":"2023-12-15T00:00:00Z","timestamp":1702598400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,15]],"date-time":"2023-12-15T00:00:00Z","timestamp":1702598400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-99-8664-4_11","type":"book-chapter","created":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T06:05:13Z","timestamp":1702533913000},"page":"189-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Leveraging TLA$$^+$$ Specifications to\u00a0Improve the\u00a0Reliability of\u00a0the\u00a0ZooKeeperCoordination Service"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7523-8759","authenticated-orcid":false,"given":"Lingzhi","family":"Ouyang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8921-036X","authenticated-orcid":false,"given":"Yu","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8359-9010","authenticated-orcid":false,"given":"Binyu","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7970-1384","authenticated-orcid":false,"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,15]]},"reference":[{"key":"11_CR1","unstructured":"Apache ZooKeeper\u2019s issue tracking system. https:\/\/issues.apache.org\/jira\/projects\/ZOOKEEPER\/issues"},{"key":"11_CR2","unstructured":"Issue: ZK-2845. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-2845"},{"key":"11_CR3","unstructured":"Issue: ZK-3615. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3615"},{"key":"11_CR4","unstructured":"Issue: ZK-3911. https:\/\/issues.apache.org\/jira\/browse\/ZOOKEEPER-3911"},{"key":"11_CR5","unstructured":"MET. https:\/\/github.com\/Lingzhi-Ouyang\/MET"},{"key":"11_CR6","unstructured":"Three levels of TLA$$^+$$ specifications for ZooKeeper. https:\/\/github.com\/Disalg-ICS-NJU\/zookeeper-tla-spec"},{"key":"11_CR7","unstructured":"TLA$$^+$$ home page. https:\/\/lamport.azurewebsites.net\/tla\/tla.html"},{"key":"11_CR8","unstructured":"TLA$$^+$$ specification for Paxos. https:\/\/github.com\/tlaplus\/Examples\/blob\/master\/specifications\/PaxosHowToWinATuringAward\/Paxos.tla"},{"key":"11_CR9","unstructured":"TLA$$^+$$ specification for PaxosStore. https:\/\/github.com\/Starydark\/PaxosStore-tla"},{"key":"11_CR10","unstructured":"TLA$$^+$$ specification for Raft. https:\/\/github.com\/ongardie\/raft.tla"},{"key":"11_CR11","unstructured":"TLA$$^+$$ specifications for the Apache ZooKeeper project. https:\/\/github.com\/apache\/zookeeper\/tree\/master\/zookeeper-specifications"},{"key":"11_CR12","unstructured":"The use of TLA$$^+$$ in industry. https:\/\/lamport.azurewebsites.net\/tla\/industrial-use.html"},{"key":"11_CR13","unstructured":"Zab\u2019s wiki. https:\/\/cwiki.apache.org\/confluence\/display\/ZOOKEEPER\/Zab1.0"},{"key":"11_CR14","unstructured":"ZooKeeper home page. https:\/\/zookeeper.apache.org\/"},{"key":"11_CR15","unstructured":"Bourque, P., Fairley, R.E., Society, I.C.: Guide to the Software Engineering Body of Knowledge (SWEBOK(R)): Version 3.0, 3rd edn. IEEE Computer Society Press, Washington, DC, USA (2014)"},{"issue":"9","key":"11_CR16","doi-asserted-by":"publisher","first-page":"1346","DOI":"10.14778\/3397230.3397233","volume":"13","author":"AJJ Davis","year":"2020","unstructured":"Davis, A.J.J., Hirschhorn, M., Schvimer, J.: eXtreme modelling in practice. Proc. VLDB Endow. 13(9), 1346\u20131358 (2020). https:\/\/doi.org\/10.14778\/3397230.3397233","journal-title":"Proc. VLDB Endow."},{"key":"11_CR17","unstructured":"Dorminey, S.: Kayfabe: model-based program testing with TLA$$^+$$\/TLC. Technical report, Microsoft Azure WAN (2020). https:\/\/conf.tlapl.us\/2020\/11-Star_Dorminey-Kayfabe_Model_based_program_testing_with_TLC.pdf"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00446-002-0070-8","volume":"16","author":"E Gafni","year":"2003","unstructured":"Gafni, E., Lamport, L.: Disk Paxos. Distrib. Comput. 16(1), 1\u201320 (2003). https:\/\/doi.org\/10.1007\/s00446-002-0070-8","journal-title":"Distrib. Comput."},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Gu, X., Cao, W., Zhu, Y., Song, X., Huang, Y., Ma, X.: Compositional model checking of consensus protocols specified in TLA$$^+$$ via interaction-preserving abstraction. In: Proceedings of International Symposium on Reliable Distributed Systems (SRDS 2022). IEEE (2022). https:\/\/doi.org\/10.1109\/srds55811.2022.00018","DOI":"10.1109\/srds55811.2022.00018"},{"issue":"4","key":"11_CR20","doi-asserted-by":"publisher","first-page":"473","DOI":"10.21655\/ijsi.1673-7288.00257","volume":"11","author":"X Gu","year":"2021","unstructured":"Gu, X., Wei, H., Qiao, L., Huang, Y.: Raft with out-of-order executions. Int. J. Softw. Informatics 11(4), 473\u2013503 (2021). https:\/\/doi.org\/10.21655\/ijsi.1673-7288.00257","journal-title":"Int. J. Softw. Informatics"},{"key":"11_CR21","unstructured":"Gunawi, H.S., et al.: FATE and DESTINI: a framework for cloud recovery testing. In: Proceedings of the 8th USENIX conference on Networked Systems Design and Implementation. p. 239 (2011). https:\/\/dl.acm.org\/doi\/10.5555\/1972457.1972482"},{"key":"11_CR22","unstructured":"Huang, B., Ouyang, L.: Pull request for ZOOKEEPER-3615: provide formal specification and verification using TLA$$^+$$ for Zab #1690. https:\/\/github.com\/apache\/zookeeper\/pull\/1690"},{"key":"11_CR23","unstructured":"Hunt, P., Konar, M., Junqueira, F.P., Reed, B.: ZooKeeper: wait-free coordination for internet-scale systems. In: Proceedings of ATC 2010, USENIX Annual Technical Conference, pp. 145\u2013158. USENIX (2010). https:\/\/dl.acm.org\/doi\/10.5555\/1855840.1855851"},{"key":"11_CR24","unstructured":"Junqueira, F.P., Reed, B.C., Serafini, M.: Dissecting Zab. Technical report, YL-2010-007, Yahoo! Research, Sunnyvale, CA, USA (2010). https:\/\/cwiki.apache.org\/confluence\/download\/attachments\/24193444\/yl-2010-007.pdf"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Junqueira, F.P., Reed, B.C., Serafini, M.: Zab: high-performance broadcast for primary-backup systems. In: Proceedings of DSN 2011, IEEE\/IFIP Conference on Dependable Systems and Networks, pp. 245\u2013256. IEEE (2011). https:\/\/doi.org\/10.1109\/DSN.2011.5958223","DOI":"10.1109\/DSN.2011.5958223"},{"key":"11_CR26","unstructured":"Kim, B.H., Kim, T., Lie, D.: Modulo: finding convergence failure bugs in distributed systems with divergence resync models. https:\/\/www.usenix.org\/conference\/atc22\/presentation\/kim-beom-heyn"},{"key":"11_CR27","unstructured":"Kuprianov, A., Konnov, I.: Model-based testing with TLA$$^+$$ and Apalache. Technical report, Informal Systems (2020). https:\/\/conf.tlapl.us\/2020\/09-Kuprianov_and_Konnov-Model-based_testing_with_TLA_+_and_Apalache.pdf"},{"issue":"2","key":"11_CR28","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s00446-006-0005-x","volume":"19","author":"L Lamport","year":"2006","unstructured":"Lamport, L.: Fast Paxos. Distrib. Comput. 19(2), 79\u2013103 (2006). https:\/\/doi.org\/10.1007\/s00446-006-0005-x","journal-title":"Distrib. Comput."},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The PlusCal Code for Byzantizing Paxos by Refinement. TechReport, Microsoft Research (2011)","DOI":"10.1007\/978-3-642-24100-0_22"},{"key":"11_CR30","unstructured":"Lamport, L., Merz, S., D, D.: A TLA$$^+$$ specification of Paxos and its refinement (2019). https:\/\/github.com\/tlaplus\/Examples\/tree\/master\/specifications\/Paxos"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Leesatapornwongsa, T., Gunawi, H.S.: SAMC: a fast model checker for finding Heisenbugs in distributed systems (demo). In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 423\u2013427. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2771783.2784771","DOI":"10.1145\/2771783.2784771"},{"key":"11_CR32","unstructured":"Leesatapornwongsa, T., Hao, M., Joshi, P., Lukman, J.F., Gunawi, H.S.: SAMC: semantic-aware model checking for fast discovery of deep bugs in cloud systems. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI 2014, pp. 399\u2013414. USENIX Association, Berkeley (2014). https:\/\/dl.acm.org\/doi\/10.5555\/2685048.2685080"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Lukman, J.F., et al.: Flymc: highly scalable testing of complex interleavings in distributed systems. In: Proceedings of the Fourteenth EuroSys Conference 2019, pp. 1\u201316 (2019). https:\/\/doi.org\/10.1145\/3302424.3303986","DOI":"10.1145\/3302424.3303986"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-63390-9_12","volume-title":"Computer Aided Verification","author":"O Mari\u0107","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 217\u2013237. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12"},{"key":"11_CR35","unstructured":"Medeiros, A.: ZooKeeper\u2019s atomic broadcast protocol: theory and practice (2012). https:\/\/www.tcs.hut.fi\/Studies\/T-79.5001\/reports\/2012-deSouzaMedeiros.pdf"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Moraru, I., Andersen, D.G., Kaminsky, M.: There is more consensus in egalitarian parliaments. In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, pp. 358\u2013372 (2013). https:\/\/doi.org\/10.1145\/2517349.2517350","DOI":"10.1145\/2517349.2517350"},{"issue":"4","key":"11_CR37","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 58(4), 66\u201373 (2015). https:\/\/doi.org\/10.1145\/2699417","journal-title":"Commun. ACM"},{"key":"11_CR38","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference, USENIX ATC 2014, pp. 305\u2013320. USENIX Association, Berkeley (2014). https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Ozkan, B.K., Majumdar, R., Niksic, F., Befrouei, M.T., Weissenbacher, G.: Randomized testing of distributed systems with probabilistic guarantees. Proc. ACM Program. Lang. 2(OOPSLA), 1\u201328 (2018). https:\/\/doi.org\/10.1145\/3276530","DOI":"10.1145\/3276530"},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"Ozkan, B.K., Majumdar, R., Oraee, S.: Trace aware random testing for distributed systems. Proc. ACM Program. Lang. 3(OOPSLA), 1\u201329 (2019). https:\/\/doi.org\/10.1145\/3360606","DOI":"10.1145\/3360606"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Wang, D., Dou, W., Gao, Y., Wu, C., Wei, J., Huang, T.: Model checking guided testing for distributed systems. In: Proceedings of the Eighteenth European Conference on Computer Systems, pp. 127\u2013143 (2023). https:\/\/doi.org\/10.1145\/3552326.3587442","DOI":"10.1145\/3552326.3587442"},{"key":"11_CR42","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1007\/s11390-020-0538-7","volume":"35","author":"JQ Yin","year":"2020","unstructured":"Yin, J.Q., Zhu, H.B., Fei, Y.: Specification and verification of the Zab protocol with TLA$$^+$$. J. Comput. Sci. Technol. 35, 1312\u20131323 (2020). https:\/\/doi.org\/10.1007\/s11390-020-0538-7","journal-title":"J. Comput. Sci. Technol."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-99-8664-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,14]],"date-time":"2023-12-14T06:07:58Z","timestamp":1702534078000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-99-8664-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,15]]},"ISBN":["9789819986637","9789819986644"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-981-99-8664-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,15]]},"assertion":[{"value":"15 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nanjing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lcs.ios.ac.cn\/setta2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"78","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}