{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T16:36:21Z","timestamp":1758040581096,"version":"3.44.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T00:00:00Z","timestamp":1738886400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T00:00:00Z","timestamp":1738886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100012550","name":"Nemzeti Kutat\u00e1si, Fejleszt\u00e9si \u00e9s Innovaci\u00f3s Alap","doi-asserted-by":"publisher","award":["2022-1.2.4-EUREKA-2023-00013","UNKP-24-3-BME-213"],"award-info":[{"award-number":["2022-1.2.4-EUREKA-2023-00013","UNKP-24-3-BME-213"]}],"id":[{"id":"10.13039\/501100012550","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Communication models are a key aspect in the design and implementation of distributed system architectures. Application logic must consider the guarantees of these models, which fundamentally influence its correctness. Modern multi-core processor architectures face a similar problem when it comes to accessing shared memory: the guarantees of an architecture have a fundamental impact on the observable behavior of software. The formalization of these guarantees in a declarative way has led to powerful tools and algorithms to define reusable constraints on patterns of memory access events and their relationships, enabling the efficient description and automatic formal analysis of software properties with respect to a specific architecture. The <jats:sc>Cat<\/jats:sc> memory modeling language provides a standard means of specifying these constraints. Despite the parallels, the axiomatic modeling and analysis of communication models in distributed systems remain a relatively unexplored area. In this paper, we address this gap and demonstrate how communication models can be mapped to the <jats:sc>Cat<\/jats:sc> language. We create a standard library of reusable patterns and demonstrate our approach, called <jats:sc>NetworCat<\/jats:sc>, on the simple examples of UDP and TCP, and we also present its applicability to the vastly configurable OMG-DDS service. This adaptation-based approach enables the use of ever-improving verification tools built for shared memory concurrency on distributed systems. We believe this not only benefits distributed system analyses by broadening the toolset for verification but also positively impacts the field of memory-model-aware verification by widening its audience to another domain.\n<\/jats:p>","DOI":"10.1007\/s10270-024-01258-x","type":"journal-article","created":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T04:46:27Z","timestamp":1738903587000},"page":"1495-1514","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Networcat: applying analysis techniques of shared memory software on message-passing distributed systems"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6551-5860","authenticated-orcid":false,"given":"Levente","family":"Bajczi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8204-7595","authenticated-orcid":false,"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,2,7]]},"reference":[{"key":"1258_CR1","unstructured":"Loo, B.T.: The design and implementation of declarative networks. PhD thesis, University of California at Berkeley (2006)"},{"key":"1258_CR2","doi-asserted-by":"publisher","unstructured":"Guerraoui, R., Yabandeh, M.: Model checking a networked system without the network. NSDI\u201911: In Proceedings of the 8th USENIX conference on Networked systems design and implementation (2011). https:\/\/doi.org\/10.5555\/1972457.1972481","DOI":"10.5555\/1972457.1972481"},{"key":"1258_CR3","doi-asserted-by":"publisher","unstructured":"Lobo, J., Ma, J., Russo, A., Le, F.: Declarative distributed computing. Correct Reasoning, 454\u2013470 (2012). https:\/\/doi.org\/10.1007\/978-3-642-30743-0_31","DOI":"10.1007\/978-3-642-30743-0_31"},{"issue":"11","key":"1258_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/1592761.1592785","volume":"52","author":"BT Loo","year":"2009","unstructured":"Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative networking. Commun. of the ACM 52(11), 87\u201395 (2009). https:\/\/doi.org\/10.1145\/1592761.1592785","journal-title":"Commun. of the ACM"},{"issue":"4\u20135","key":"1258_CR5","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1017\/s1471068413000513","volume":"13","author":"J Ma","year":"2013","unstructured":"Ma, J., Le, F., Wood, D., Russo, A., Lobo, J.: A declarative approach to distributed computing: specification, execution and analysis. Theory Pract. Log. Programm. 13(4\u20135), 815\u2013830 (2013). https:\/\/doi.org\/10.1017\/s1471068413000513","journal-title":"Theory Pract. Log. Programm."},{"key":"1258_CR6","volume-title":"Distributed algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed algorithms. Morgan Kaufmann, San Francisco (1996)"},{"issue":"8","key":"1258_CR7","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978). https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"1258_CR8","volume-title":"A calculus of communicating systems. Lecture notes in computer science","author":"R Milner","year":"1980","unstructured":"Milner, R.: A calculus of communicating systems. Lecture notes in computer science, vol. 92. Springer, Berlin, Germany (1980)"},{"issue":"1","key":"1258_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"I. Inf. Comput."},{"key":"1258_CR10","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-540-92995-6_5","volume":"5418","author":"A Wang","year":"2008","unstructured":"Wang, A., Basu, P., Loo, B.T., Sokolsky, O.: Declarative network verification. Practical Asp. Declar. Lang. 5418, 61\u201375 (2008). https:\/\/doi.org\/10.1007\/978-3-540-92995-6_5","journal-title":"Practical Asp. Declar. Lang."},{"key":"1258_CR11","doi-asserted-by":"publisher","first-page":"107126","DOI":"10.1109\/ACCESS.2023.3320050","volume":"11","author":"T Kapus","year":"2023","unstructured":"Kapus, T.: Improved formal verification of SDN-based firewalls by using $$\\text{ TLA}^{\\text{+ }}$$. IEEE Access 11, 107126\u2013107134 (2023). https:\/\/doi.org\/10.1109\/ACCESS.2023.3320050","journal-title":"IEEE Access"},{"key":"1258_CR12","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: IronFleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, pp. 1\u201317. ACM, Monterey, CA (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"1258_CR13","doi-asserted-by":"publisher","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015). https:\/\/doi.org\/10.14279\/TUJ.ECEASST.72.1013","DOI":"10.14279\/TUJ.ECEASST.72.1013"},{"key":"1258_CR14","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, Portland, OR, USA, June 15-17, pp. 357\u2013368. ACM, Portland, OR, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"},{"issue":"POPL","key":"1258_CR15","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3158116","volume":"2","author":"I Sergey","year":"2018","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. Proc. ACM Program. Lang. 2(POPL), 28\u201312830 (2018). https:\/\/doi.org\/10.1145\/3158116","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOPSLA","key":"1258_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3360570","volume":"3","author":"R Mogk","year":"2019","unstructured":"Mogk, R., Drechsler, J., Salvaneschi, G., Mezini, M.: A fault-tolerant programming model for distributed interactive applications. Proc. ACM on Programm. Lang. 3(OOPSLA), 1\u201329 (2019). https:\/\/doi.org\/10.1145\/3360570","journal-title":"Proc. ACM on Programm. Lang."},{"issue":"2","key":"1258_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7\u20131774 (2014). https:\/\/doi.org\/10.1145\/2627752","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1258_CR18","doi-asserted-by":"publisher","unstructured":"Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and Litmus tests. In: Cohen, A., Vechev, M.T. (eds.) 38th ACM SIGPLAN conference on programming language design and implementation, PLDI 2017, pp. 467\u2013481. ACM, Barcelona, Spain (2017). https:\/\/doi.org\/10.1145\/3062341.3062353","DOI":"10.1145\/3062341.3062353"},{"key":"1258_CR19","doi-asserted-by":"publisher","unstructured":"Trippel, C., Manerkar, Y.A., Lustig, D., et al.: TriCheck: Memory model verification at the trisection of software, hardware, and ISA. In: Chen, Y., Temam, O., Carter, J. (eds.) 22nd international conference on architectural support for programming languages and operating systems, ASPLOS 2017, pp. 119\u2013133. ACM, Xi\u2019an, China (2017). https:\/\/doi.org\/10.1145\/3037697.3037719","DOI":"10.1145\/3037697.3037719"},{"key":"1258_CR20","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: McKinley, K.S., Fisher, K. (eds.) conference on programming language design and implementation, PLDI, pp. 96\u2013110. ACM, Phoenix, Arizona, United States (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","DOI":"10.1145\/3314221.3314609"},{"key":"1258_CR21","doi-asserted-by":"publisher","unstructured":"Le\u00f3n, H.P., Furbach, F., Heljanko, K., et al.: BMC with memory models as modules. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) 2018 formal methods in computer aided design, FMCAD, pp. 1\u20139. IEEE, Austin, TX, USA (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603021","DOI":"10.23919\/FMCAD.2018.8603021"},{"issue":"1","key":"1258_CR22","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/200836.200869","volume":"42","author":"H Attiya","year":"1995","unstructured":"Attiya, H., Bar-Noy, A., Dolev, D.: Sharing memory robustly in message-passing systems. J. ACM 42(1), 124\u2013142 (1995). https:\/\/doi.org\/10.1145\/200836.200869","journal-title":"J. ACM"},{"key":"1258_CR23","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Moln\u00e1r, V.: NetworCat: axiomatic analysis of distributed systems. Budapest University of Technology and Economics. https:\/\/doi.org\/10.5281\/zenodo.8147152","DOI":"10.5281\/zenodo.8147152"},{"key":"1258_CR24","unstructured":"Waterman, A., Asanovi\u0107, K.: The RISC-V instruction set manual version 2.2 (2017). https:\/\/riscv.org\/wp-content\/uploads\/2017\/05\/riscv-spec-v2.2.pdf"},{"key":"1258_CR25","unstructured":"Alglave, J., Cousot, P., Maranget, L.: Syntax and semantics of the weak consistency model specification language cat. CoRR arXiv:1608.07531 (2016)"},{"issue":"POPL","key":"1258_CR26","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/3158105","volume":"2","author":"M Kokologiannakis","year":"2018","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., et al.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17\u201311732 (2018). https:\/\/doi.org\/10.1145\/3158105","journal-title":"Proc. ACM Program. Lang."},{"key":"1258_CR27","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., et al.: Repairing sequential consistency in C\/C++11. In: 38th ACM SIGPLAN conference on programming language design and implementation. PLDI 2017, pp. 618\u2013632. association for computing machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"1258_CR28","doi-asserted-by":"publisher","unstructured":"Gavrilenko, N., Le\u00f3n, H.P., Furbach, F., et al.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) computer aided verification - 31st international conference, CAV 2019. Lecture Notes in Computer Science, vol. 11561, pp. 355\u2013365. Springer, New York, NY, USA (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"1258_CR29","doi-asserted-by":"publisher","unstructured":"Rakamaric, Z., Emmi, M.: SMACK: Decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) computer aided verification - 26th international conference, CAV 2014. Lecture notes in computer science, vol. 8559, pp. 106\u2013113. Springer, Vienna, Austria (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"1258_CR30","unstructured":"MQTT Version 5.0. Technical report, OASIS Standard (March 2019). https:\/\/docs.oasis-open.org\/mqtt\/mqtt\/v5.0\/mqtt-v5.0.html"},{"key":"1258_CR31","unstructured":"OMG data distribution service (DDS) version 1.4. technical report, object management group (April 2015). https:\/\/www.omg.org\/spec\/DDS\/1.4\/PDF"},{"key":"1258_CR32","unstructured":"Programming languages - C. International standard, International Organization for Standardization, International Electrotechnical Commission (2010). https:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1548.pdf"},{"key":"1258_CR33","doi-asserted-by":"publisher","unstructured":"User datagram protocol. RFC Editor (1980). https:\/\/doi.org\/10.17487\/RFC0768. https:\/\/www.rfc-editor.org\/info\/rfc768","DOI":"10.17487\/RFC0768"},{"key":"1258_CR34","doi-asserted-by":"publisher","unstructured":"Eddy, W.: Transmission control protocol (TCP). RFC Editor (2022). https:\/\/doi.org\/10.17487\/RFC9293. https:\/\/www.rfc-editor.org\/info\/rfc9293","DOI":"10.17487\/RFC9293"},{"key":"1258_CR35","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-031-57256-2_22","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"P-C Chien","year":"2024","unstructured":"Chien, P.-C., Lee, N.-Z.: CPV: a circuit-based program verifier. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and algorithms for the construction and analysis of systems, pp. 365\u2013370. Springer, Cham (2024)"},{"key":"1258_CR36","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chien, P.-C., Lee, N.-Z.: Bridging hardware and software analysis with Btor2C: a word-level-circuit-to-C translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and algorithms for the construction and analysis of systems, pp. 152\u2013172. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-30820-8_12"},{"key":"1258_CR37","volume-title":"Model checking software: 30th international symposium, SPIN 2024. Lecture notes in computer science","author":"L Bajczi","year":"2025","unstructured":"Bajczi, L., Moln\u00e1r, V.: Solving constrained horn clauses as C programs with CHC2C. In: Neele, T., Wijs, A. (eds.) Model checking software: 30th international symposium, SPIN 2024. Lecture notes in computer science. Springer, Luxembourg City, Luxembourg (2025)"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01258-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01258-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01258-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T08:56:15Z","timestamp":1757580975000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01258-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,7]]},"references-count":37,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["1258"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01258-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2025,2,7]]},"assertion":[{"value":"26 February 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 December 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}