{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:23:36Z","timestamp":1771471416933,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031765537","type":"print"},{"value":"9783031765544","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_2","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:11Z","timestamp":1731410291000},"page":"24-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Systematic Literature Review on\u00a0a\u00a0Decade of\u00a0Industrial TLA+\u00a0Practice"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-8745-7800","authenticated-orcid":false,"given":"Roman","family":"B\u00f6gli","sequence":"first","affiliation":[]},{"given":"Leandro","family":"Lerena","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9493-3404","authenticated-orcid":false,"given":"Christos","family":"Tsigkanos","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2582-5557","authenticated-orcid":false,"given":"Timo","family":"Kehrer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Braithwaite, S., et al.: A Tendermint Light Client (2020). https:\/\/doi.org\/10.48550\/arXiv.2010.07031","DOI":"10.48550\/arXiv.2010.07031"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Davis, A.J.J., Hirschhorn, M., Schvimer, J.: eXtreme modelling in practice. Proc. VLDB Endowment 13(9), 1346\u20131358 (2020). https:\/\/doi.org\/10.14778\/3397230.3397233","DOI":"10.14778\/3397230.3397233"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1007\/978-3-030-90870-6_42","volume-title":"Formal Methods","author":"S Gao","year":"2021","unstructured":"Gao, S., et al.: Formal verification of consensus in the Taurus distributed database. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 741\u2013751. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_42"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Gu, X., Cao, W., Zhu, Y., Song, X., Huang, Y., Ma, X.: Compositional model checking of consensus protocols via interaction-preserving abstraction. In: 2022 41st International Symposium on Reliable Distributed Systems (SRDS), pp. 82\u201393 (2022).https:\/\/doi.org\/10.1109\/SRDS55811.2022.00018","DOI":"10.1109\/SRDS55811.2022.00018"},{"key":"2_CR5","unstructured":"Hackett, F., Rowe, J., Kuppe, M.A.: Going Beyond an Incident Report with TLA$$^+$$ (2023). https:\/\/www.usenix.org\/sites\/default\/files\/login_-_going_beyond_an_incident_report_with_tla_.pdf"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Hackett, F., Rowe, J., Kuppe, M.A.: Understanding inconsistency in azure cosmos DB with TLA+. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pp. 1\u201312. IEEE (2023). https:\/\/doi.org\/10.1109\/ICSE-SEIP58684.2023.00006","DOI":"10.1109\/ICSE-SEIP58684.2023.00006"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Jakobs, C., Werner, M., Schmidt, K., Hansch, G.: Following the white rabbit: integrity verification based on risk analysis results. In: Proceedings of the 5th ACM Computer Science in Cars Symposium. CSCS \u201921, pp.\u00a01\u20139, New York, NY, USA. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3488904.3493377","DOI":"10.1145\/3488904.3493377"},{"key":"2_CR8","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-17581-2_14","volume-title":"Formal Techniques for Safety-Critical Systems","author":"A Methni","year":"2015","unstructured":"Methni, A., Lemerre, M., Ben Hedia, B., Haddad, S., Barkaoui, K.: Specifying and verifying concurrent C programs with TLA+. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2014. CCIS, vol. 476, pp. 206\u2013222. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17581-2_14"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Newcombe, C.: Why Amazon Chose TLA$$^{+}$$. In: Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. pp. 25\u201339. Springer, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_3","DOI":"10.1007\/978-3-662-43652-3_3"},{"issue":"4","key":"2_CR10","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":"2_CR11","doi-asserted-by":"publisher","unstructured":"Padhy, S., Stubbs, J.: Designing and proving properties of the abaco autoscaler using TLA+. In: Bloem, R., Dimitrova, R., Fan, C., Sharygina, N. (eds.) Software Verification, pp. 86\u2013103. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_6","DOI":"10.1007\/978-3-030-95561-8_6"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Resch, S., Paulitsch, M.: Using TLA+ in the development of a safety-critical fault-tolerant middleware. In: 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 146\u2013152 (2017). https:\/\/doi.org\/10.1109\/ISSREW.2017.43","DOI":"10.1109\/ISSREW.2017.43"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Roohitavaf, M., Ren, K., Zhang, G., Ben-romdhane, S.: LogPlayer: fault-tolerant exactly-once delivery using gRPC asynchronous streaming (2019). https:\/\/doi.org\/10.48550\/arXiv.1911.11286","DOI":"10.48550\/arXiv.1911.11286"},{"key":"2_CR14","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-34647-8_14","volume-title":"Critical Infrastructure Protection XIII","author":"M Sabraoui","year":"2019","unstructured":"Sabraoui, M., Hieb, J., Lauf, A., Graham, J.: Modeling and machine-checking bump-in-the-wire security for industrial control systems. In: ICCIP 2019. IAICT, vol. 570, pp. 271\u2013288. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34647-8_14"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Salierno, G., Morvillo, S., Leonardi, L., Cabri, G.: Specification and verification of railway safety-critical systems using TLA$$^{+}$$: a case study. In: 2020 IEEE 29th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 207\u2013212 (2020). https:\/\/doi.org\/10.1109\/WETICE49692.2020.00048","DOI":"10.1109\/WETICE49692.2020.00048"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Schultz, W., Zhou, S., Dardik, I., Tripakis, S.: Design and analysis of a logless dynamic reconfiguration protocol (2021). https:\/\/doi.org\/10.48550\/arXiv.2102.11960","DOI":"10.48550\/arXiv.2102.11960"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Buyya, R., et al.: A manifesto for future generation cloud computing: research directions for the next decade. ACM Comput. Surv. 51(5), 105:1\u2013105:38 (2018). https:\/\/doi.org\/10.1145\/3241737","DOI":"10.1145\/3241737"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Carrera-Rivera, A., Ochoa, W., Larrinaga, F., Lasa, G.: How-to conduct a systematic literature review: a quick guide for computer science research. MethodsX 9, 101895 (2022). https:\/\/doi.org\/10.1016\/j.mex.2022.101895","DOI":"10.1016\/j.mex.2022.101895"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Dedehayir, O., Steinert, M.: The hype cycle model: A review and future directions. Technological Forecasting and Social Change 108, 28\u201341 (2016). https:\/\/doi.org\/10.1016\/j.techfore.2016.04.005","DOI":"10.1016\/j.techfore.2016.04.005"},{"key":"2_CR21","unstructured":"Kitchenham, B.A., Charters, S.: Guidelines for performing systematic literature reviews in software engineering. Technical rep.ort EBSE 2007-001, Keele University and Durham University Joint Report (2007). https:\/\/www.elsevier.com\/__data\/promis_misc\/525444systematicreviewsguide.pdf"},{"key":"2_CR22","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002). https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2018\/05\/book-02-08-08.pdf"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-03466-4_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"L Lamport","year":"2009","unstructured":"Lamport, L.: The PlusCal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36\u201360. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03466-4_2"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: An update. Inf. Software Technol. 64, 1\u201318 (2015). https:\/\/doi.org\/10.1016\/j.infsof.2015.03.007","DOI":"10.1016\/j.infsof.2015.03.007"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Reid, A., Church, L., Flur, S., de\u00a0Haas, S., Johnson, M., Laurie, B.: Towards making formal methods normal: meeting developers where they are (2020). https:\/\/doi.org\/10.48550\/arXiv.2010.16345","DOI":"10.48550\/arXiv.2010.16345"},{"key":"2_CR27","unstructured":"Rogers, E.M.: Diffusion of Innovations. Social science, Free Press, New York London Toronto Sydney, 5 edn. (2003). ISBN: 978-0-7432-2209-9"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Yasin, A., Fatima, R., Wen, L., Afzal, W., Azhar, M., Torkar, R.: On using grey literature and google scholar in systematic literature reviews in software engineering. IEEE Access 8, 36226\u201336243 (2020). https:\/\/doi.org\/10.1109\/ACCESS.2020.2971712","DOI":"10.1109\/ACCESS.2020.2971712"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Zimmermann, T.: Card-sorting: from text to themes. In: Menzies, T., Williams, L., Zimmermann, T. (eds.) Perspectives on Data Science for Software Engineering, pp. 137\u2013141. Morgan Kaufmann, Boston (2016). https:\/\/doi.org\/10.1016\/B978-0-12-804206-9.00027-1","DOI":"10.1016\/B978-0-12-804206-9.00027-1"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:22Z","timestamp":1737200302000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}