{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:02:57Z","timestamp":1779087777410,"version":"3.51.4"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>Today\u2019s distributed systems must satisfy both<jats:italic>qualitative<\/jats:italic>and<jats:italic>quantitative<\/jats:italic>properties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare\/separation logics, for qualitative properties; and timed\/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible to<jats:italic>represent<\/jats:italic>intrinsic features of distributed object systems\u2014such as unbounded data structures, dynamic object creation, and an unbounded number of messages\u2014using finite automata.<\/jats:p><jats:p>In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha\u2019s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into the<jats:italic>Actors2PMaude<\/jats:italic>tool. We illustrate the expressiveness of our framework and our tool\u2019s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs\u2014including an industrial data store and a state-of-the-art transaction system\u2014into quantitative models to analyze and compare the performance of different designs.<\/jats:p>","DOI":"10.1145\/3563299","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"315-344","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Bridging the semantic gap between qualitative and quantitative models of distributed systems"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3578-7432","authenticated-orcid":false,"given":"Si","family":"Liu","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4779-3848","authenticated-orcid":false,"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0708-3721","authenticated-orcid":false,"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[{"name":"University of Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-2902","authenticated-orcid":false,"given":"Min","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.58.1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_1_3_1","volume-title":"Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In Workshop on Foundations of Computer Security (FCS).","author":"Agha Gul","year":"2005","unstructured":"Gul Agha , Carl Gunter , Michael Greenwald , Sanjeev Khanna , Jose Meseguer , Koushik Sen , and Prasanna Thati . 2005 . Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In Workshop on Foundations of Computer Security (FCS). Gul Agha, Carl Gunter, Michael Greenwald, Sanjeev Khanna, Jose Meseguer, Koushik Sen, and Prasanna Thati. 2005. Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories. In Workshop on Foundations of Computer Security (FCS)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_2_1_5_1","volume-title":"PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. Electr. Notes Theor. Comput. Sci., 153, 2","author":"Agha Gul A.","year":"2006","unstructured":"Gul A. Agha , Jos\u00e9 Meseguer , and Koushik Sen . 2006. PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. Electr. Notes Theor. Comput. Sci., 153, 2 ( 2006 ). Gul A. Agha, Jos\u00e9 Meseguer, and Koushik Sen. 2006. PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. Electr. Notes Theor. Comput. Sci., 153, 2 (2006)."},{"key":"e_1_2_1_6_1","volume-title":"CALCO\u201911 (LNCS","author":"AlTurki Musab","unstructured":"Musab AlTurki and Jos\u00e9 Meseguer . 2011. PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool . In CALCO\u201911 (LNCS , Vol. 6859). Springer, 386\u2013 392 . Musab AlTurki and Jos\u00e9 Meseguer. 2011. PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In CALCO\u201911 (LNCS, Vol. 6859). Springer, 386\u2013392."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.069"},{"key":"e_1_2_1_8_1","volume-title":"Pre-computed Reveal Strategies. In Formal Methods. FM 2019 International Workshops (LNCS","volume":"349","author":"Musab","unstructured":"Musab A. Alturki and Grigore Rosu. 2019. Statistical Model Checking of RANDAO\u2019s Resilience to Pre-computed Reveal Strategies. In Formal Methods. FM 2019 International Workshops (LNCS , Vol. 12232). Springer, 337\u2013 349 . Musab A. Alturki and Grigore Rosu. 2019. Statistical Model Checking of RANDAO\u2019s Resilience to Pre-computed Reveal Strategies. In Formal Methods. FM 2019 International Workshops (LNCS, Vol. 12232). Springer, 337\u2013349."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728816.2728827"},{"key":"e_1_2_1_10_1","unstructured":"Amazon. Accessed April 2022. Amazon EC2. https:\/\/aws.amazon.com\/ec2\/ Amazon. Accessed April 2022. Amazon EC2. https:\/\/aws.amazon.com\/ec2\/"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_29"},{"key":"e_1_2_1_12_1","volume-title":"Handbook of Model Checking, Edmund M","author":"Baier Christel","unstructured":"Christel Baier , Luca de Alfaro , Vojtech Forejt , and Marta Kwiatkowska . 2018. Model Checking Probabilistic Systems . In Handbook of Model Checking, Edmund M . Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer , 963\u2013999. Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. 2018. Model Checking Probabilistic Systems. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer, 963\u2013999."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2909870"},{"key":"e_1_2_1_14_1","volume-title":"CMC 2016 (Lecture Notes in Computer Science","volume":"135","author":"Bakir Mehmet Emin","year":"2017","unstructured":"Mehmet Emin Bakir , Marian Gheorghe , Savas Konur , and Mike Stannett . 2017 . Comparative Analysis of Statistical Model Checking Tools. In Membrane Computing - 17th International Conference , CMC 2016 (Lecture Notes in Computer Science , Vol. 10105). Springer, 119\u2013 135 . Mehmet Emin Bakir, Marian Gheorghe, Savas Konur, and Mike Stannett. 2017. Comparative Analysis of Statistical Model Checking Tools. In Membrane Computing - 17th International Conference, CMC 2016 (Lecture Notes in Computer Science, Vol. 10105). Springer, 119\u2013135."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_2_1_16_1","volume-title":"Maltz","author":"Benson Theophilus","year":"2010","unstructured":"Theophilus Benson , Aditya Akella , and David A . Maltz . 2010 . Network traffic characteristics of data centers in the wild. In IMC\u201910. ACM , 267\u2013280. Theophilus Benson, Aditya Akella, and David A. Maltz. 2010. Network traffic characteristics of data centers in the wild. In IMC\u201910. ACM, 267\u2013280."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3_6"},{"key":"e_1_2_1_18_1","volume-title":"Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude. In Assured Cloud Computing","author":"Bobba Rakesh","year":"2018","unstructured":"Rakesh Bobba , Jon Grov , Indranil Gupta , Si Liu , Jos\u00e9 Meseguer , Peter Csaba \u00d6lveczky , and Stephen Skeirik . 2018 . Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude. In Assured Cloud Computing . Wiley-IEEE Computer Society Press , 10\u201348. Rakesh Bobba, Jon Grov, Indranil Gupta, Si Liu, Jos\u00e9 Meseguer, Peter Csaba \u00d6lveczky, and Stephen Skeirik. 2018. Survivability: Design, Formal Modeling, and Validation of Cloud Storage Systems Using Maude. In Assured Cloud Computing. Wiley-IEEE Computer Society Press, 10\u201348."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"e_1_2_1_21_1","unstructured":"Apache Cassandra. Accessed April 2022. Open Source NoSQL Database. https:\/\/cassandra.apache.org Apache Cassandra. Accessed April 2022. Open Source NoSQL Database. https:\/\/cassandra.apache.org"},{"key":"e_1_2_1_22_1","volume-title":"Talcott","author":"Clavel Manuel","year":"2007","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn L . Talcott . 2007 . All About Maude (LNCS, Vol . 4350). Springer . Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn L. Talcott. 2007. All About Maude (LNCS, Vol. 4350). Springer."},{"key":"e_1_2_1_23_1","unstructured":"CloudLab. Accessed April 2022. CloudLab: Flexible scientific infrastructure for research on the future of cloud computing. https:\/\/www.cloudlab.us\/ CloudLab. Accessed April 2022. CloudLab: Flexible scientific infrastructure for research on the future of cloud computing. https:\/\/www.cloudlab.us\/"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Brian F. Cooper Adam Silberstein Erwin Tam Raghu Ramakrishnan and Russell Sears. 2010. Benchmarking cloud serving systems with YCSB. In SOCC\u201910. ACM 143\u2013154. Brian F. Cooper Adam Silberstein Erwin Tam Raghu Ramakrishnan and Russell Sears. 2010. Benchmarking cloud serving systems with YCSB. In SOCC\u201910. ACM 143\u2013154.","DOI":"10.1145\/1807128.1807152"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0361-y"},{"key":"e_1_2_1_26_1","volume-title":"CMSB 2008 (LNCS","volume":"287","author":"Donaldson Robin","unstructured":"Robin Donaldson and David R. Gilbert . 2008. A Model Checking Approach to the Parameter Estimation of Biochemical Pathways . In CMSB 2008 (LNCS , Vol. 5307). Springer, 269\u2013 287 . Robin Donaldson and David R. Gilbert. 2008. A Model Checking Approach to the Parameter Estimation of Biochemical Pathways. In CMSB 2008 (LNCS, Vol. 5307). Springer, 269\u2013287."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2018.8635877"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Giacomo Giuliari Dominik Roos Marc Wyss Juan \u00c1ngel Garc\u00eda-Pardo Markus Legner and Adrian Perrig. 2021. Colibri: a cooperative lightweight inter-domain bandwidth-reservation infrastructure. In CoNEXT\u201921. ACM 104\u2013118. Giacomo Giuliari Dominik Roos Marc Wyss Juan \u00c1ngel Garc\u00eda-Pardo Markus Legner and Adrian Perrig. 2021. Colibri: a cooperative lightweight inter-domain bandwidth-reservation infrastructure. In CoNEXT\u201921. ACM 104\u2013118.","DOI":"10.1145\/3485983.3494871"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_2_1_32_1","volume-title":"Alvin AuYoung, Kimberly Keeton, and Indranil Gupta.","author":"Golab Wojciech M.","year":"2014","unstructured":"Wojciech M. Golab , Muntasir Raihan Rahman , Alvin AuYoung, Kimberly Keeton, and Indranil Gupta. 2014 . Client-Centric Benchmarking of Eventual Consistency for Cloud Storage Systems. In ICDCS. IEEE Computer Society , 493\u2013502. Wojciech M. Golab, Muntasir Raihan Rahman, Alvin AuYoung, Kimberly Keeton, and Indranil Gupta. 2014. Client-Centric Benchmarking of Eventual Consistency for Cloud Storage Systems. In ICDCS. IEEE Computer Society, 493\u2013502."},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"G. Grimmett and D. Stirzaker. 2001. Probability and Random Processes (3rd Ed.). Oxford University Press. G. Grimmett and D. Stirzaker. 2001. Probability and Random Processes (3rd Ed.). Oxford University Press.","DOI":"10.1093\/oso\/9780198572237.001.0001"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Jon Grov and Peter Csaba \u00d6lveczky. 2014. Formal Modeling and Analysis of Google\u2019s Megastore in Real-Time Maude. In Specification Algebra and Software (LNCS Vol. 8373). Springer. Jon Grov and Peter Csaba \u00d6lveczky. 2014. Formal Modeling and Analysis of Google\u2019s Megastore in Real-Time Maude. In Specification Algebra and Software (LNCS Vol. 8373). Springer.","DOI":"10.1007\/978-3-642-54624-2_25"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11422778_62"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"e_1_2_1_38_1","volume-title":"Proc. QEST","author":"Henriques David","year":"2012","unstructured":"David Henriques , Jo\u00e3o G. Martins , Paolo Zuliani , Andr\u00e9 Platzer , and Edmund M. Clarke . 2012. Statistical Model Checking for Markov Decision Processes . In Proc. QEST 2012 . IEEE Computer Society, 84\u201393. David Henriques, Jo\u00e3o G. Martins, Paolo Zuliani, Andr\u00e9 Platzer, and Edmund M. Clarke. 2012. Statistical Model Checking for Markov Decision Processes. In Proc. QEST 2012. IEEE Computer Society, 84\u201393."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2016.01.004"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.03.004"},{"key":"e_1_2_1_41_1","volume-title":"LTSmin: High-Performance Language-Independent Model Checking. In TACAS 2015 (LNCS","volume":"707","author":"Kant Gijs","unstructured":"Gijs Kant , Alfons Laarman , Jeroen Meijer , Jaco van de Pol, Stefan Blom, and Tom van Dijk. 2015 . LTSmin: High-Performance Language-Independent Model Checking. In TACAS 2015 (LNCS , Vol. 9035). Springer, 692\u2013 707 . Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, and Tom van Dijk. 2015. LTSmin: High-Performance Language-Independent Model Checking. In TACAS 2015 (LNCS, Vol. 9035). Springer, 692\u2013707."},{"key":"e_1_2_1_42_1","volume-title":"Proc. FMOODS 2008 (LNCS","volume":"169","author":"Katelman Michael","unstructured":"Michael Katelman , Jos\u00e9 Meseguer , and Jennifer C. Hou . 2008. Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking . In Proc. FMOODS 2008 (LNCS , Vol. 5051). Springer, 150\u2013 169 . Michael Katelman, Jos\u00e9 Meseguer, and Jennifer C. Hou. 2008. Redesign of the LMST Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking. In Proc. FMOODS 2008 (LNCS, Vol. 5051). Springer, 150\u2013169."},{"key":"e_1_2_1_43_1","volume-title":"Probability Theory","author":"Klenke Achim","unstructured":"Achim Klenke . 2006. Probability Theory . Springer . Achim Klenke. 2006. Probability Theory. Springer."},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In CAV\u201911 (LNCS Vol. 6806). Springer 585\u2013591. M. Kwiatkowska G. Norman and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In CAV\u201911 (LNCS Vol. 6806). Springer 585\u2013591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231984"},{"key":"e_1_2_1_46_1","volume-title":"Exploring Design Alternatives for Replicated RAMP Transactions Using Maude","author":"Liang Lei","unstructured":"Lei Liang and Si Liu . 2021. Exploring Design Alternatives for Replicated RAMP Transactions Using Maude . In TASE. IEEE , 111\u2013118. Lei Liang and Si Liu. 2021. Exploring Design Alternatives for Replicated RAMP Transactions Using Maude. In TASE. IEEE, 111\u2013118."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3494517"},{"key":"e_1_2_1_48_1","article-title":"Quantitative Analysis of Consistency in NoSQL Key-Value Stores","volume":"4","author":"Liu Si","year":"2017","unstructured":"Si Liu , Jatin Ganhotra , Muntasir Rahman , Son Nguyen , Indranil Gupta , and Jos\u00e9 Meseguer . 2017 . Quantitative Analysis of Consistency in NoSQL Key-Value Stores . Leibniz Transactions on Embedded Systems , 4 , 1 (2017), 03:1\u201303:26. Si Liu, Jatin Ganhotra, Muntasir Rahman, Son Nguyen, Indranil Gupta, and Jos\u00e9 Meseguer. 2017. Quantitative Analysis of Consistency in NoSQL Key-Value Stores. Leibniz Transactions on Embedded Systems, 4, 1 (2017), 03:1\u201303:26.","journal-title":"Leibniz Transactions on Embedded Systems"},{"key":"e_1_2_1_49_1","unstructured":"Si Liu Jos\u00e9 Meseguer Peter Csaba \u00d6lveczky Min Zhang and David Basin. 2022. Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems. http:\/\/hdl.handle.net\/20.500.11850\/563291 Si Liu Jos\u00e9 Meseguer Peter Csaba \u00d6lveczky Min Zhang and David Basin. 2022. Bridging the Semantic Gap between Qualitative and Quantitative Models of Distributed Systems. http:\/\/hdl.handle.net\/20.500.11850\/563291"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7071693"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68690-5_18"},{"key":"e_1_2_1_52_1","volume-title":"Software, Services, and Systems (LNCS","author":"Liu Si","unstructured":"Si Liu , Peter Csaba \u00d6lveczky , and Jos\u00e9 Meseguer . 2015. Formal Analysis of Leader Election in MANETs Using Real-Time Maude . In Software, Services, and Systems (LNCS , Vol. 8950). Springer, 231\u2013 252 . Si Liu, Peter Csaba \u00d6lveczky, and Jos\u00e9 Meseguer. 2015. Formal Analysis of Leader Election in MANETs Using Real-Time Maude. In Software, Services, and Systems (LNCS, Vol. 8950). Springer, 231\u2013252."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.05.002"},{"key":"e_1_2_1_54_1","volume-title":"Jatin Ganhotra, Indranil Gupta, and Jos\u00e9 Meseguer.","author":"Liu Si","year":"2016","unstructured":"Si Liu , Peter Csaba \u00d6lveczky , Muntasir Raihan Rahman , Jatin Ganhotra, Indranil Gupta, and Jos\u00e9 Meseguer. 2016 . Formal modeling and analysis of RAMP transaction systems. In SAC. ACM. Si Liu, Peter Csaba \u00d6lveczky, Muntasir Raihan Rahman, Jatin Ganhotra, Indranil Gupta, and Jos\u00e9 Meseguer. 2016. Formal modeling and analysis of RAMP transaction systems. In SAC. ACM."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00489-w"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99840-4_8"},{"key":"e_1_2_1_57_1","volume-title":"TACAS\u201919 (LNCS","author":"Liu Si","unstructured":"Si Liu , Peter Csaba \u00d6lveczky , Min Zhang , Qi Wang , and Jos\u00e9 Meseguer . 2019. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude . In TACAS\u201919 (LNCS , Vol. 11428). Springer, 40\u2013 57 . Si Liu, Peter Csaba \u00d6lveczky, Min Zhang, Qi Wang, and Jos\u00e9 Meseguer. 2019. Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In TACAS\u201919 (LNCS, Vol. 11428). Springer, 40\u201357."},{"key":"e_1_2_1_58_1","volume-title":"Stephen Skeirik, Indranil Gupta, and Jos\u00e9 Meseguer.","author":"Liu Si","year":"2014","unstructured":"Si Liu , Muntasir Raihan Rahman , Stephen Skeirik, Indranil Gupta, and Jos\u00e9 Meseguer. 2014 . Formal Modeling and Analysis of Cassandra in Maude. In ICFEM (LNCS , Vol. 8829). Springer. Si Liu, Muntasir Raihan Rahman, Stephen Skeirik, Indranil Gupta, and Jos\u00e9 Meseguer. 2014. Formal Modeling and Analysis of Cassandra in Maude. In ICFEM (LNCS, Vol. 8829). Springer."},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Si Liu Atul Sandur Jos\u00e9 Meseguer Peter Csaba \u00d6lveczky and Qi Wang. 2020. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. In NFM\u201920 (LNCS Vol. 12229). Springer. Si Liu Atul Sandur Jos\u00e9 Meseguer Peter Csaba \u00d6lveczky and Qi Wang. 2020. Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. In NFM\u201920 (LNCS Vol. 12229). Springer.","DOI":"10.1007\/978-3-030-55754-6_2"},{"key":"e_1_2_1_60_1","volume-title":"ATVA\u201918 (LNCS","author":"Mediouni Braham Lotfi","unstructured":"Braham Lotfi Mediouni , Ayoub Nouri , Marius Bozga , Mahieddine Dellabani , Axel Legay , and Saddek Bensalem . 2018. SBIP 2.0 : Statistical Model Checking Stochastic Real-Time Systems . In ATVA\u201918 (LNCS , Vol. 11138). Springer, 536\u2013 542 . Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay, and Saddek Bensalem. 2018. SBIP 2.0: Statistical Model Checking Stochastic Real-Time Systems. In ATVA\u201918 (LNCS, Vol. 11138). Springer, 536\u2013542."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_62_1","volume-title":"Research Directions in Concurrent Object-Oriented Programming","author":"Meseguer Jos\u00e9","unstructured":"Jos\u00e9 Meseguer . 1993. A Logical Theory of Concurrent Objects and its realization in the Maude Language . In Research Directions in Concurrent Object-Oriented Programming , Gul Agha, Peter Wegner, and Akinori Yonezawa (Eds.). MIT Press , 314\u2013390. Jos\u00e9 Meseguer. 1993. A Logical Theory of Concurrent Objects and its realization in the Maude Language. In Research Directions in Concurrent Object-Oriented Programming, Gul Agha, Peter Wegner, and Akinori Yonezawa (Eds.). MIT Press, 314\u2013390."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.07.003"},{"key":"e_1_2_1_64_1","volume-title":"Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems. In HSCC (LNCS","volume":"475","author":"Meseguer J.","unstructured":"J. Meseguer and R. Sharykin . 2006 . Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems. In HSCC (LNCS , Vol. 3927). Springer, 460\u2013 475 . J. Meseguer and R. Sharykin. 2006. Specification and Analysis of Distributed Object-Based Stochastic Hybrid Systems. In HSCC (LNCS, Vol. 3927). Springer, 460\u2013475."},{"key":"e_1_2_1_65_1","unstructured":"Microsoft. 2018. High-level TLA+ specifications for the five consistency levels offered by Azure Cosmos DB. https:\/\/github.com\/Azure\/azure-cosmos-tla Microsoft. 2018. High-level TLA+ specifications for the five consistency levels offered by Azure Cosmos DB. https:\/\/github.com\/Azure\/azure-cosmos-tla"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_2_1_67_1","volume-title":"Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude","author":"\u00d6lveczky Peter Csaba","unstructured":"Peter Csaba \u00d6lveczky . 2017. Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude . Springer . Peter Csaba \u00d6lveczky. 2017. Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude. Springer."},{"key":"e_1_2_1_68_1","first-page":"1","article-title":"Ad hoc On-Demand Distance Vector (AODV) Routing","volume":"3561","author":"Perkins Charles E.","year":"2003","unstructured":"Charles E. Perkins , Elizabeth M. Belding-Royer , and Samir R. Das . 2003 . Ad hoc On-Demand Distance Vector (AODV) Routing . RFC , 3561 (2003), 1 \u2013 37 . Charles E. Perkins, Elizabeth M. Belding-Royer, and Samir R. Das. 2003. Ad hoc On-Demand Distance Vector (AODV) Routing. RFC, 3561 (2003), 1\u201337.","journal-title":"RFC"},{"key":"e_1_2_1_69_1","unstructured":"PRISM. Accessed April 2022. PRISM-SMC. https:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking PRISM. Accessed April 2022. PRISM-SMC. https:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking"},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"R. Rubinstein and D.P. Kroese. 2017. Simulation and the Monte Carlo Method (3rd Ed.). J. Wiley & Sons. R. Rubinstein and D.P. Kroese. 2017. Simulation and the Monte Carlo Method (3rd Ed.). J. Wiley & Sons.","DOI":"10.1002\/9781118631980"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100700"},{"key":"e_1_2_1_72_1","volume-title":"SCION: Scalability, Control, and Isolation on Next-Generation Networks. https:\/\/scion-architecture.net\/","author":"Accessed April SCION.","year":"2022","unstructured":"SCION. Accessed April , 2022 . SCION: Scalability, Control, and Isolation on Next-Generation Networks. https:\/\/scion-architecture.net\/ SCION. Accessed April, 2022. SCION: Scalability, Control, and Isolation on Next-Generation Networks. https:\/\/scion-architecture.net\/"},{"key":"e_1_2_1_73_1","unstructured":"Stefano Sebastio and Andrea Vandin. 2013. MultiVeStA: Statistical Model Checking for Discrete Event Simulators. In ValueTools. ICST\/ACM 310\u2013315. Stefano Sebastio and Andrea Vandin. 2013. MultiVeStA: Statistical Model Checking for Discrete Event Simulators. In ValueTools. ICST\/ACM 310\u2013315."},{"key":"e_1_2_1_74_1","unstructured":"Koushik Sen Mahesh Viswanathan and Gul Agha. 2005. On Statistical Model Checking of Stochastic Systems. In CAV\u201905 (LNCS Vol. 3576). Springer. Koushik Sen Mahesh Viswanathan and Gul Agha. 2005. On Statistical Model Checking of Stochastic Systems. In CAV\u201905 (LNCS Vol. 3576). Springer."},{"key":"e_1_2_1_75_1","volume-title":"Agha","author":"Sen Koushik","year":"2005","unstructured":"Koushik Sen , Mahesh Viswanathan , and Gul A . Agha . 2005 . VESTA : A Statistical Model-checker and Analyzer for Probabilistic Systems. In QEST\u201905. IEEE Computer Society , 251\u2013252. Koushik Sen, Mahesh Viswanathan, and Gul A. Agha. 2005. VESTA: A Statistical Model-checker and Analyzer for Probabilistic Systems. In QEST\u201905. IEEE Computer Society, 251\u2013252."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370686.2370691"},{"key":"e_1_2_1_77_1","doi-asserted-by":"crossref","unstructured":"Stephen Skeirik Rakesh B. Bobba and Jos\u00e9 Meseguer. 2013. Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper. In CCGRID. 636\u2013641. Stephen Skeirik Rakesh B. Bobba and Jos\u00e9 Meseguer. 2013. Formal Analysis of Fault-tolerant Group Key Management Using ZooKeeper. In CCGRID. 636\u2013641.","DOI":"10.1109\/CCGrid.2013.98"},{"key":"e_1_2_1_78_1","volume-title":"Vivek Nigam, Andre Scedrov, and Carolyn L. Talcott.","author":"Urquiza Abra\u00e3o Aires","year":"2019","unstructured":"Abra\u00e3o Aires Urquiza , Musab A. AlTurki , Max I. Kanovich , Tajana Ban Kirigin , Vivek Nigam, Andre Scedrov, and Carolyn L. Talcott. 2019 . Resource-Bounded Intruders in Denial of Service Attacks. In CSF. IEEE , 382\u2013396. Abra\u00e3o Aires Urquiza, Musab A. AlTurki, Max I. Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov, and Carolyn L. Talcott. 2019. Resource-Bounded Intruders in Denial of Service Attacks. In CSF. IEEE, 382\u2013396."},{"key":"e_1_2_1_79_1","volume-title":"Boon Thau Loo, and Andre Scedrov","author":"Wang Anduo","year":"2011","unstructured":"Anduo Wang , Carolyn L. Talcott , Limin Jia , Boon Thau Loo, and Andre Scedrov . 2011 . Analyzing BGP Instances in Maude. In FMOODS\u201911 (LNCS , Vol. 6722). Springer, 334\u2013 348 . Anduo Wang, Carolyn L. Talcott, Limin Jia, Boon Thau Loo, and Andre Scedrov. 2011. Analyzing BGP Instances in Maude. In FMOODS\u201911 (LNCS, Vol. 6722). Springer, 334\u2013348."},{"key":"e_1_2_1_80_1","volume-title":"ICDCS Workshop on Distributed System Validation and Verification","author":"Wang Bow-Yaw","year":"2000","unstructured":"Bow-Yaw Wang , Jos\u00e9 Meseguer , and Carl A. Gunter . 2000. Specification and Formal Analysis of a PLAN Algorithm in Maude . In ICDCS Workshop on Distributed System Validation and Verification 2000 . E49\u2013E56. Bow-Yaw Wang, Jos\u00e9 Meseguer, and Carl A. Gunter. 2000. Specification and Formal Analysis of a PLAN Algorithm in Maude. In ICDCS Workshop on Distributed System Validation and Verification 2000. E49\u2013E56."},{"key":"e_1_2_1_81_1","volume-title":"59th IEEE Conference on Decision and Control, CDC","author":"Wang Yu","year":"2020","unstructured":"Yu Wang , Nima Roohi , Matthew West , Mahesh Viswanathan , and Geir E. Dullerud . 2020. Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning . In 59th IEEE Conference on Decision and Control, CDC 2020 . IEEE, 1392\u20131397. Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud. 2020. Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning. In 59th IEEE Conference on Decision and Control, CDC 2020. IEEE, 1392\u20131397."},{"key":"e_1_2_1_82_1","volume-title":"N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures. In CSF","author":"Weghorn Thilo","year":"2022","unstructured":"Thilo Weghorn , Si Liu , Christoph Sprenger , Adrian Perrig , and David Basin . 2022 . N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures. In CSF 2022. IEEE. To appear Thilo Weghorn, Si Liu, Christoph Sprenger, Adrian Perrig, and David Basin. 2022. N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures. In CSF 2022. IEEE. To appear"},{"key":"e_1_2_1_83_1","volume-title":"An Integrated Experimental Environment for Distributed Systems and Networks","author":"White Brian","unstructured":"Brian White , Jay Lepreau , Leigh Stoller , Robert Ricci , Shashi Guruprasad , Mac Newbold , Mike Hibler , Chad Barb , and Abhijeet Joglekar . 2002. An Integrated Experimental Environment for Distributed Systems and Networks . In OSDI. USENIX Association . Brian White, Jay Lepreau, Leigh Stoller, Robert Ricci, Shashi Guruprasad, Mac Newbold, Mike Hibler, Chad Barb, and Abhijeet Joglekar. 2002. An Integrated Experimental Environment for Distributed Systems and Networks. In OSDI. USENIX Association."},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.05.002"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563299","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":84,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563299"],"URL":"https:\/\/doi.org\/10.1145\/3563299","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}