{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T21:12:33Z","timestamp":1780521153307,"version":"3.54.1"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032052902","type":"print"},{"value":"9783032052919","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-05291-9_19","type":"book-chapter","created":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T14:08:16Z","timestamp":1758722896000},"page":"446-474","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Programming and\u00a0Verifying Actor Systems in\u00a0Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G.: Actors. MIT Press (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"19_CR2","unstructured":"Agha, G., Hewitt, C.: Concurrent programming using actors. In: Yonezawa, A., Tokoro, M. (eds.) Object-Oriented Concurrent Programming, pp. 37\u201353. MIT Press (1988)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Agha, G., Fr\u00f8lund, S., Panwar, R., Sturman, D.: A linguistic framework for dynamic composition of dependability protocols. In: Landwehr, C.E., Randell, B., Simoncini, L. (eds.) Dependable Computing for Critical Applications 3, pp. 345\u2013363. Springer Vienna (1993)","DOI":"10.1007\/978-3-7091-4009-3_15"},{"issue":"2","key":"19_CR4","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","DOI":"10.1145\/3158668"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110, 100501 (2020)","DOI":"10.1016\/j.jlamp.2019.100501"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_28"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.02.069","volume":"234","author":"M AlTurki","year":"2009","unstructured":"AlTurki, M., Meseguer, J., Gunter, C.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. Electr. Notes Theor. Comput. Sci. 234, 3\u201318 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"19_CR9","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: Rewriting Techniques and Applications (RTA 2013). LIPIcs, vol.\u00a021, pp. 81\u201396. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2013)"},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using Multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015)","journal-title":"Sci. Comput. Program."},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/j.scico.2014.02.006","volume":"99","author":"K Bae","year":"2015","unstructured":"Bae, K., Meseguer, J.: Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99, 193\u2013234 (2015)","journal-title":"Sci. Comput. Program."},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.09.010","volume":"91","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3\u201344 (2014)","journal-title":"Sci. Comput. Program."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proceedings 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 145\u2013154 (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"19_CR14","doi-asserted-by":"publisher","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94\u2013109. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_7","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., \u00d6lveczky, P.C., Skeirik, S.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. In: Campbell, R.H., Kamhoua, C.A., Kwiat, K.A. (eds.) Assured Cloud Computing, chap.\u00a02, pp. 10\u201348. Wiley-IEEE Computer Society Press (2018)","DOI":"10.1002\/9781119428497.ch2"},{"issue":"1\u20133","key":"19_CR16","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Chadha, R., Gunter, C.A., Meseguer, J., Shankesi, R., Viswanathan, M.: Modular preservation of safety properties by cookie-based DoS-protection wrappers. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 39\u201358. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_4","DOI":"10.1007\/978-3-540-68863-1_4"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Chen, S., Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.M.: A systematic approach to uncover security flaws in GUI logic. In: IEEE Symposium on Security and Privacy, pp. 71\u201385. IEEE (2007)","DOI":"10.1109\/SP.2007.6"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"19_CR20","unstructured":"Clavel, M., et al.: Maude manual (version 3.5) (2024). https:\/\/maude.cs.illinois.edu\/manual.pdf"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.12.009","volume":"373","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. Theoret. Comput. Sci. 373, 70\u201391 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Rewriting semantics of meta-objects and composable distributed services. In: ENTCS 36, Proceedings of the 3rd. International Workshop on Rewriting Logic and its Applications. Elsevier (2000)","DOI":"10.1016\/S1571-0661(05)80132-X"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming open distributed systems in Maude. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, 9-11 September 2024, pp. 7:1\u20137:12. ACM (2024). https:\/\/doi.org\/10.1145\/3678232.3678237","DOI":"10.1145\/3678232.3678237"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Eker, S., Lincoln, P., Meseguer, J.: Principles of Mobile Maude. In: Kotz, D., Mattern, F. (eds.) ASA\/MA -2000. LNCS, vol. 1882, pp. 73\u201385. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-540-45347-5_7","DOI":"10.1007\/978-3-540-45347-5_7"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: MTT: The Maude Termination Tool (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313\u2013319. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_27","DOI":"10.1007\/978-3-540-71070-7_27"},{"key":"19_CR27","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination Modulo Combinations of Equational Theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 246\u2013262. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_15","DOI":"10.1007\/978-3-642-04222-5_15"},{"key":"19_CR28","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic and Logic Programming 81, 816\u2013850 (2012)","journal-title":"J. Algebraic and Logic Programming"},{"key":"19_CR29","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2025.101048","volume":"144","author":"F Dur\u00e1n","year":"2025","unstructured":"Dur\u00e1n, F., Ram\u00edrez, C., Rocha, C., Pozas, N.: A rewriting logic semantics for the analysis of P programs. J. Log. Algebraic Methods Program. 144, 101048 (2025)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F.J., Escobar, S., Meseguer, J., Sapi\u00f1a, J.: NuITP: An inductive theorem prover for equational program verification. In: Bruni, A., Momigliano, A., Pradella, M., Rossi, M., Cheney, J. (eds.) Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, 9-11 September 2024, pp. 6:1\u20136:11. ACM (2024), https:\/\/doi.org\/10.1145\/3678232.3678236","DOI":"10.1145\/3678232.3678236"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Eckhardt, J., M\u00fchlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78\u201393. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_6","DOI":"10.1007\/978-3-642-28872-2_6"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Gal\u00e1n, D., Garc\u00eda, V., Escobar, S., Meadows, C.A., Meseguer, J.: Protocol dialects as formal patterns. In: Tsudik, G., Conti, M., Liang, K., Smaragdakis, G. (eds.) Computer Security - ESORICS 2023 - 28th European Symposium on Research in Computer Security, The Hague, The Netherlands, 25-29 September 2023, Proceedings, Part II. LNCS, vol. 14345, pp. 42\u201361. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-51476-0_","DOI":"10.1007\/978-3-031-51476-0_"},{"key":"19_CR34","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Grimmett, G., Stirzaker, D.: Probability and Random Processes (3rd edn.). Oxford University Press (2001)","DOI":"10.1093\/oso\/9780198572237.001.0001"},{"key":"19_CR36","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.scico.2014.07.003","volume":"99","author":"R Guti\u00e9rrez","year":"2015","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. Sci. Comput. Program. 99, 235\u2013261 (2015)","journal-title":"Sci. Comput. Program."},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Gutierrez-Nolasco, S., Venkatasubramanian, N., Talcott, C.: A semantic model for safe protocol interaction. In: Proceedings of the 2006 ACM Symposium on Applied Computing, pp. 1599\u20131600. SAC 2006, Association for Computing Machinery (2006)","DOI":"10.1145\/1141277.1141650"},{"key":"19_CR38","doi-asserted-by":"publisher","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151\u2013155. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_14","DOI":"10.1007\/11814771_14"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Hewitt, C., de\u00a0Jong, P.: Open systems. In: Brodie, M.L., Mylopoulos, J., Schmidt, J.W. (eds.) Perspectives from Artificial Intelligence, Databases, and Programming Languages, pp. 147\u2013164. Springer (1982)","DOI":"10.1007\/978-1-4612-5196-5_6"},{"key":"19_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"19_CR41","doi-asserted-by":"publisher","unstructured":"Katelman, M., Meseguer, J., Hou, J.: Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 150\u2013169. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_10","DOI":"10.1007\/978-3-540-68863-1_10"},{"key":"19_CR42","unstructured":"Kumar, N., Sen, K., Meseguer, J., Agha, G.: Probabilistic rewrite theories: Unifying models, logics and tools. Tech. Rep. UIUCDCS-R-2003-2347, CS Dept., University of Illinois at Urbana-Champaign (2003). http:\/\/formalmethods.web.engr.illinois.edu\/papers\/SKMAfme.pdf"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Liu, S., Duan, H., Heimes, L., Bearzi, M., Vieli, J., Basin, D.A., Perrig, A.: A formal framework for end-to-end DNS resolution. In: Schulzrinne, H., Misra, V., Kohler, E., Maltz, D.A. (eds.) Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM 2023, New York, NY, USA, 10-14 September 2023, pp. 932\u2013949. ACM (2023)","DOI":"10.1145\/3603269.3604870"},{"issue":"OOPSLA2","key":"19_CR44","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1145\/3563299","volume":"6","author":"S Liu","year":"2022","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.A.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR45","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/j.jlamp.2015.05.002","volume":"85","author":"S Liu","year":"2016","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: Modeling and analyzing mobile ad hoc networks in Real-Time Maude. J. Log. Algebr. Meth. Program. 85, 34\u201366 (2016)","journal-title":"J. Log. Algebr. Meth. Program."},{"issue":"5","key":"19_CR46","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/s00165-019-00489-w","volume":"31","author":"S Liu","year":"2019","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Gupta, I., Meseguer, J.: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31(5), 503\u2013540 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00489-w","journal-title":"Formal Aspects Comput."},{"key":"19_CR47","doi-asserted-by":"publisher","unstructured":"Liu, S., \u00d6lveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 40\u201357. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_3","DOI":"10.1007\/978-3-030-17465-1_3"},{"key":"19_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-55754-6_2","volume-title":"NASA Formal Methods","author":"S Liu","year":"2020","unstructured":"Liu, S., Sandur, A., Meseguer, J., \u00d6lveczky, P.C., Wang, Q.: Generating correct-by-construction distributed implementations from formal Maude designs. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 22\u201340. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_2"},{"issue":"2","key":"19_CR49","first-page":"103","volume":"79","author":"J Meseguer","year":"2010","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Algebraic simulations. J. Log. Algebr. Program 79(2), 103\u2013143 (2010)","journal-title":"Program"},{"key":"19_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47993-7_1","volume-title":"ECOOP 2002 \u2014 Object-Oriented Programming","author":"J Meseguer","year":"2002","unstructured":"Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1\u201336. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-47993-7_1"},{"key":"19_CR51","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects. In: ECOOP-OOPSLA 1990 Conference on Object-Oriented Programming, Ottawa, Canada, October 1990, pp. 101\u2013115. ACM (1990)","DOI":"10.1145\/97945.97958"},{"key":"19_CR52","unstructured":"Meseguer, J.: Rewriting as a unified model of concurrency. Tech. Rep. SRI-CSL-90-02, SRI International, Computer Science Laboratory (1990), revised June 1990"},{"issue":"1","key":"19_CR53","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR54","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. MIT Press (1993)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"19_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-47910-4_13","volume-title":"ECOOP 1993 \u2014 Object-Oriented Programming","author":"J Meseguer","year":"1993","unstructured":"Meseguer, J.: Solving the inheritance anomaly in concurrent object-oriented programming. In: Nierstrasz, O.M. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 220\u2013246. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-47910-4_13"},{"key":"19_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-61604-7_64","volume-title":"CONCUR 1996: Concurrency Theory","author":"J Meseguer","year":"1996","unstructured":"Meseguer, J.: Rewriting logic as a semantic framework for concurrency: a progress report. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 331\u2013372. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_64"},{"key":"19_CR57","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic Logic Programm. 81, 721\u2013781 (2012)","journal-title":"J. Algebraic Logic Programm."},{"key":"19_CR58","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.07.004","volume":"83","author":"J Meseguer","year":"2014","unstructured":"Meseguer, J.: Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83, 3\u201334 (2014)","journal-title":"Sci. Comput. Program."},{"key":"19_CR59","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110, 100483 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"19_CR60","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Building correct-by-construction systems with formal patterns. In: Madeira, A., Martins, M.A. (eds.) Recent Trends in Algebraic Development Techniques - 26th IFIP WG 1.3 International Workshop, WADT 2022, Aveiro, Portugal, 28-30 June 2022, Revised Selected Papers. LNCS, vol. 13710, pp. 3\u201324. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-43345-0_1","DOI":"10.1007\/978-3-031-43345-0_1"},{"key":"19_CR61","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Checking sufficient completeness by inductive theorem proving. In: Bae, K. (ed.) Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, 2-3 April 2022, Revised Selected Papers. LNCS, vol. 13252, pp. 171\u2013190. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_9","DOI":"10.1007\/978-3-031-12441-9_9"},{"key":"19_CR62","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Capturing system designs with formal executable specifications. In: Boronat, A., Fraser, G. (eds.) Fundamental Approaches to Software Engineering - 28th International Conference, FASE 2025. LNCS, vol. 15693, pp. 1\u201332. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90900-9_1","DOI":"10.1007\/978-3-031-90900-9_1"},{"key":"19_CR63","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2012.05.040","volume":"451","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR64","doi-asserted-by":"crossref","unstructured":"Miller, S., Cofer, D., Sha, L., Meseguer, J., Al-Nayeem, A.: Implementing logical synchrony in integrated modular avionics. In: Proceedings of the 28th Digital Avionics Systems Conference. IEEE (2009)","DOI":"10.1109\/DASC.2009.5347579"},{"issue":"1\u20132","key":"19_CR65","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"PC \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order Symbolic Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"Higher-Order Symbolic Comput."},{"key":"19_CR66","series-title":"Undergraduate Topics in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-6687-0","volume-title":"Designing Reliable Distributed Systems","author":"PC \u00d6lveczky","year":"2017","unstructured":"\u00d6lveczky, P.C.: Designing Reliable Distributed Systems. UTCS, Springer, London (2017). https:\/\/doi.org\/10.1007\/978-1-4471-6687-0"},{"key":"19_CR67","doi-asserted-by":"crossref","unstructured":"Rubinstein, R., Kroese, D.: Simulation and the Monte Carlo Method, 3rd edn. Wiley (2017)","DOI":"10.1002\/9781118631980"},{"key":"19_CR68","doi-asserted-by":"publisher","unstructured":"Rubio, R.: Maude as a library: An efficient all-purpose programming interface. In: Bae, K. (ed.) Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022. LNCS, vol. 13252, pp. 274\u2013294. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_14","DOI":"10.1007\/978-3-031-12441-9_14"},{"key":"19_CR69","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100700","volume":"123","author":"R Rubio","year":"2021","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebraic Methods Program. 123, 100700 (2021)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"19_CR70","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s10515-021-00307-9","volume":"29","author":"R Rubio","year":"2022","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng. 29(1), 7 (2022)","journal-title":"Autom. Softw. Eng."},{"key":"19_CR71","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: QMaude: quantitative specification and verification in rewriting logic. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, 6-10 March 2023, Proceedings. LNCS, vol. 14000, pp. 240\u2013259. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_15","DOI":"10.1007\/978-3-031-27481-7_15"},{"key":"19_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-35861-6_14","volume-title":"Formal Aspects of Component Software","author":"R Sasse","year":"2013","unstructured":"Sasse, R., King, S.T., Meseguer, J., Tang, S.: IBOS: a correct-by-construction modular browser. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 224\u2013241. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35861-6_14"},{"key":"19_CR73","unstructured":"Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horv\u00e1th, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools \u201913, Torino, Italy, 10-12 December 2013, pp. 310\u2013315. ICST\/ACM (2013)"},{"key":"19_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"key":"19_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_26"},{"key":"19_CR76","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005, pp. 251\u2013252 (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"19_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-030-63595-4_10","volume-title":"Rewriting Logic and Its Applications","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Meseguer, J., Rocha, C.: Verification of the IBOS browser security properties in reachability logic. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 176\u2013196. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_10"},{"key":"19_CR78","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J.: Distributed real-time emulation of formally-defined patterns for safe medical device control. In: Proceedings of the RTRTS 2010. Electronic Proceedings in Theoretical Computer Science, vol.\u00a036, pp. 158\u2013177 (2010)","DOI":"10.4204\/EPTCS.36.9"},{"key":"19_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-12904-4_15","volume-title":"Rewriting Logic and Its Applications","author":"M Sun","year":"2014","unstructured":"Sun, M., Meseguer, J.: Formal specification of button-related fault-tolerance micropatterns. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 263\u2013279. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_15"},{"key":"19_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-16310-4_11","volume-title":"Rewriting Logic and Its Applications","author":"M Sun","year":"2010","unstructured":"Sun, M., Meseguer, J., Sha, L.: A formal pattern architecture for safe medical systems. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 157\u2013173. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_11"},{"key":"19_CR81","doi-asserted-by":"publisher","unstructured":"Talcott, C.: Dialects for the CoAP IoT messaging protocol. In: Giusto, C.D., Ravara, A. (eds.) COORDINATION 2025. LNCS, vol. 15731. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-95589-1_9","DOI":"10.1007\/978-3-031-95589-1_9"},{"issue":"1","key":"19_CR82","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1005561.1005564","volume":"13","author":"N Venkatasubramanian","year":"2004","unstructured":"Venkatasubramanian, N., Talcott, C.L., Agha, G.: A formal model for reasoning about adaptive QoS-enabled middleware. ACM Trans. Softw. Eng. Methodol. 13(1), 86\u2013147 (2004)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"19_CR83","doi-asserted-by":"crossref","unstructured":"Weghorn, T., Liu, S., Sprenger, C., Perrig, A., Basin, D.: N-tube: formally verified secure bandwidth reservation in path-aware internet architectures. In: 2022 IEEE 35th Computer Security Foundations Symposium (CSF), pp. 147\u2013162 (2022)","DOI":"10.1109\/CSF54842.2022.9919646"}],"container-title":["Lecture Notes in Computer Science","Concurrent Programming, Open Systems and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05291-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T20:58:39Z","timestamp":1780520319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05291-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032052902","9783032052919"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05291-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}