{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:56Z","timestamp":1776304976071,"version":"3.50.1"},"publisher-location":"Cham","reference-count":111,"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_21","type":"book-chapter","created":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T14:08:29Z","timestamp":1758722909000},"page":"494-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modeling and\u00a0Analyzing Real-Time Systems in\u00a0Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[]},{"given":"Carlos","family":"Olarte","sequence":"additional","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge, MA, USA (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation 28(1), 6:1\u20136:39 (2018)","DOI":"10.1145\/3158668"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Agha, G.A., Kim, W.: Actors: A unifying model for parallel and distributed computing. Journal of Systems Architecture 45(15), 1263\u20131277 (1999)","DOI":"10.1016\/S1383-7621(98)00067-8"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Al-Nayeem, A., Sun, M., Qiu, X., Sha, L., Miller, S.P., Cofer, D.D.: A formal architecture pattern for real-time distributed systems. In: RTSS\u201909. pp. 161\u2013170. IEEE Computer Society, USA (2009)","DOI":"10.1109\/RTSS.2009.50"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Dhurjati, D., Yu, D., Chander, A., Inamura, H.: Formal specification and analysis of timing properties in software systems. In: FASE\u201909. Lecture Notes in Computer Science, vol.\u00a05503, pp. 262\u2013277. Springer (2009)","DOI":"10.1007\/978-3-642-00593-0_18"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J.: Dist-Orc: A rewriting-based distributed implementation of Orc with formal analysis. In: RTRTS\u201910. EPTCS, vol.\u00a036, pp. 26\u201345 (2010)","DOI":"10.4204\/EPTCS.36.2"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model checking and quantitative analysis tool. In: Algebra and Coalgebra in Computer Science (CALCO 2011). Lecture Notes in Computer Science, vol.\u00a06859. Springer (2011)","DOI":"10.1007\/978-3-642-22944-2_28"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183\u2013235 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L.: A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets. Fundamenta Informaticae 192(3-4), 261\u2013312 (2024)","DOI":"10.3233\/FI-242195"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Arias, J., Bae, K., Olarte, C., \u00d6lveczky, P.C., Petrucci, L., R\u00f8mming, F.: Symbolic analysis and parameter synthesis for networks of parametric timed automata with global variables using Maude and SMT solving. Science of Computer Programming 233, 103074 (2024)","DOI":"10.1016\/j.scico.2023.103074"},{"key":"21_CR11","doi-asserted-by":"crossref","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. Science of Computer Programming 103, 13\u201350 (2015)","DOI":"10.1016\/j.scico.2014.09.011"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Science of Computer Programming 91, 3\u201344 (2014)","DOI":"10.1016\/j.scico.2013.09.010"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C.: MSYNC: A generalized formal design pattern for virtually synchronous multirate cyber-physical systems. ACM Transactions on Embedded Computing Systems 20(5s), 105:1\u2013105:26 (2021)","DOI":"10.1145\/3477036"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C.: Formal model engineering of distributed CPSs using AADL: From behavioral AADL models to Multirate Hybrid Synchronous AADL. In: FACS\u201923. Lecture Notes in Computer Science, vol. 14485, pp. 127\u2013152. Springer (2023)","DOI":"10.1007\/978-3-031-52183-6_7"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: ICFEM\u201911. Lecture Notes in Computer Science, vol.\u00a06991, pp. 651\u2013667. Springer (2011)","DOI":"10.1007\/978-3-642-24559-6_43"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Science of Computer Programming 77(12), 1235\u20131271 (2012)","DOI":"10.1016\/j.scico.2010.10.002"},{"key":"21_CR17","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: HSCC\u201916. pp. 145\u2013154. ACM (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: FM\u201914. Lecture Notes in Computer Science, vol.\u00a08442, pp. 94\u2013109. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: FASE\u201912. Lecture Notes in Computer Science, vol.\u00a07212, pp. 59\u201362. Springer (2012)","DOI":"10.1007\/978-3-642-28872-2_4"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Science of Computer Programming 178, 20\u201342 (2019)","DOI":"10.1016\/j.scico.2019.03.006"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Formal Methods for the Design of Real-Time Systems (SFM-RT 2004). LNCS, vol.\u00a03185, pp. 200\u2013236. Springer (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Berger, U., James, P., Lawrence, A., Roggenbach, M., Seisenberger, M.: Verification of the European Rail Traffic Management System in Real-Time Maude. Science of Computer Programming 154, 61\u201388 (2018)","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rk, J., de\u00a0Boer, F.S., Johnsen, E.B., Schlatte, R., Tarifa, S.L.T.: User-defined schedulers for real-time concurrent objects. Innovations in Systems and Software Engineering 9(1), 29\u201343 (2013)","DOI":"10.1007\/s11334-012-0184-5"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Boronat, A., \u00d6lveczky, P.C.: Formal real-time model transformations in MOMENT2. In: FASE\u201910. Lecture Notes in Computer Science, vol.\u00a06013, pp. 29\u201343. Springer (2010)","DOI":"10.1007\/978-3-642-12029-9_3"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Broccia, G., Milazzo, P., \u00d6lveczky, P.C.: Formal modeling and analysis of safety-critical human multitasking. Innovations in Systems and Software Engineering 15(3-4), 169\u2013190 (2019)","DOI":"10.1007\/s11334-019-00333-7"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Cerone, A.: A cognitive framework based on rewriting logic for the analysis of interactive systems. In: SEFM\u201916. Lecture Notes in Computer Science, vol.\u00a09763, pp. 287\u2013303. Springer (2016)","DOI":"10.1007\/978-3-319-41591-8_20"},{"key":"21_CR27","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Maude Manual (Version 3.5). SRI International (2024), available at http:\/\/maude.cs.illinois.edu"},{"key":"21_CR28","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude \u2013 A High-Performance Logical Framework, LNCS, vol.\u00a04350. Springer (2007)"},{"key":"21_CR29","unstructured":"Ding, H., Zheng, C., Agha, G., Sha, L.: Automated verification of the dependability of object-oriented real-time systems. In: WORDS\u201903. pp. 171\u2013178. IEEE Computer Society (2003)"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F.: Rewriting logic and Maude for the formalization and analysis of DSMLs, and the prototyping of MDSE tools. J. Object Technol. 21(4), 4:1\u201312 (2022)","DOI":"10.5381\/jot.2022.21.4.a2"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Pozas, N., Rocha, C.: Business processes resource management using rewriting logic and deep-learning-based predictive monitoring. J. Log. Algebraic Methods Program. 136, 100928 (2024)","DOI":"10.1016\/j.jlamp.2023.100928"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Rocha, C., Sala\u00fcn, G.: Stochastic analysis of BPMN with time in rewriting logic. Sci. Comput. Program. 168, 1\u201317 (2018)","DOI":"10.1016\/j.scico.2018.08.007"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Rocha, C., Sala\u00fcn, G.: Resource provisioning strategies for BPMN processes: Specification and analysis using Maude. J. Log. Algebraic Methods Program. 123, 100711 (2021)","DOI":"10.1016\/j.jlamp.2021.100711"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., Sala\u00fcn, G.: Verifying timed BPMN processes using Maude. In: Proc. of COORDINATION. LNCS, vol. 10319, pp. 219\u2013236. Springer (2017)","DOI":"10.1007\/978-3-319-59746-1_12"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Eker, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Verdejo, A.: The Maude strategy language. Journal of Logical and Algebraic Methods in Programming 134, 100887 (2023)","DOI":"10.1016\/j.jlamp.2023.100887"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Fadlisyah, M., \u00d6lveczky, P.C.: The HI-Maude tool. In: CALCO\u201913. Lecture Notes in Computer Science, vol.\u00a08089, pp. 322\u2013327. Springer (2013)","DOI":"10.1007\/978-3-642-40206-7_25"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"Fadlisyah, M., \u00d6lveczky, P.C., \u00c1brah\u00e1m, E.: Object-oriented formal modeling and analysis of interacting hybrid systems in HI-Maude. In: SEFM\u201911. Lecture Notes in Computer Science, vol.\u00a07041, pp. 415\u2013430. Springer (2011)","DOI":"10.1007\/978-3-642-24690-6_29"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Fadlisyah, M., \u00d6lveczky, P.C., \u00c1brah\u00e1m, E.: Formal modeling and analysis of interacting hybrid systems in HI-Maude: What happened at the 2010 sauna world championships? Science of Computer Programming 99, 95\u2013127 (2015)","DOI":"10.1016\/j.scico.2014.06.010"},{"key":"21_CR39","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley, USA (2012)"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Grov, J., \u00d6lveczky, P.C.: Formal modeling and analysis of Google\u2019s Megastore in Real-Time Maude. In: Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. Lecture Notes in Computer Science, vol.\u00a08373, pp. 494\u2013519. Springer (2014)","DOI":"10.1007\/978-3-642-54624-2_25"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Grov, J., \u00d6lveczky, P.C.: Increasing consistency in multi-site data stores: Megastore-CGC and its formal analysis. In: SEFM\u201914. Lecture Notes in Computer Science, vol.\u00a08702, pp. 159\u2013174. Springer (2014)","DOI":"10.1007\/978-3-319-10431-7_12"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Hansen, S.T., \u00d6lveczky, P.C.: Modeling, algorithm synthesis, and instrumentation for co-simulation in Maude. In: WRLA\u201922. Lecture Notes in Computer Science, vol. 13252, pp. 130\u2013150. Springer (2022)","DOI":"10.1007\/978-3-031-12441-9_7"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Kasera, S.K., Bhattacharyya, S., Keaton, M., Kiwior, D., Zabele, S., Kurose, J.F., Towsley, D.: Scalable fair reliable multicast using active services. IEEE Network 14(1), 48\u201357 (2000)","DOI":"10.1109\/65.819171"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Katelman, M., Meseguer, J., Hou, J.C.: Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking. In: FMOODS\u201908. Lecture Notes in Computer Science, vol.\u00a05051, pp. 150\u2013169. Springer (2008)","DOI":"10.1007\/978-3-540-68863-1_10"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Kopetz, H., Bauer, G.: The time-triggered architecture. Proceedings of the IEEE 91(1), 112\u2013126 (2003)","DOI":"10.1109\/JPROC.2002.805821"},{"key":"21_CR46","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: ISoLA\u201922. Lecture Notes in Computer Science, vol. 13703, pp. 47\u201364. Springer (2022)","DOI":"10.1007\/978-3-031-19759-8_4"},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: Rigorous model engineering of hierarchical multirate CPSs in MR-HybridSynchAADL. In: ISoLA\u201924. Lecture Notes in Computer Science, vol. 15220, pp. 243\u2013262. Springer (2024)","DOI":"10.1007\/978-3-031-75107-3_15"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C., Kim, S., Kang, M.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. International Journal on Software Tools for Technology Transfer 24(6), 911\u2013948 (2022)","DOI":"10.1007\/s10009-022-00665-z"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: Modeling and formal analysis of virtually synchronous CPSs in AADL. In: CAV\u201921. Lecture Notes in Computer Science, vol. 12759, pp. 491\u2013504. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K.: Formal semantics and analysis of multitask PLC ST programs with preemption. In: FM\u201924. Lecture Notes in Computer Science, vol. 14933, pp. 425\u2013442. Springer (2024)","DOI":"10.1007\/978-3-031-71162-6_22"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of PLC ST programs using rewriting modulo SMT. In: FTSCS\u201922. pp. 56\u201367. ACM (2022)","DOI":"10.1145\/3563822.3568016"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Lepri, D., \u00c1brah\u00e1m, E., \u00d6lveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Science of Computer Programming 99, 128\u2013192 (2015)","DOI":"10.1016\/j.scico.2014.06.006"},{"key":"21_CR53","doi-asserted-by":"crossref","unstructured":"Li, R., Zhu, H., Banach, R.: An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency. The Journal of Logic and Algebraic Programming 139, 100973 (2024)","DOI":"10.1016\/j.jlamp.2024.100973"},{"key":"21_CR54","doi-asserted-by":"crossref","unstructured":"Lien, E., \u00d6lveczky, P.C.: Formal modeling and analysis of an IETF multicast protocol. In: Seventh IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009). pp. 273\u2013282. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.11"},{"key":"21_CR55","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhou, M., Song, X., Gu, M., Sun, J.: Formal modeling and verification of a rate-monotonic scheduling implementation with Real-Time Maude. IEEE Transactions on Industrial Electronics 64(4), 3239\u20133249 (2017)","DOI":"10.1109\/TIE.2016.2633476"},{"key":"21_CR56","unstructured":"Liu, S., Ganhotra, J., Rahman, M.R., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Transactions on Embedded Systems 4(1), 03:1\u201303:26 (2017)"},{"key":"21_CR57","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3563299"},{"key":"21_CR58","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Ganhotra, J., Gupta, I., Meseguer, J.: Exploring design alternatives for RAMP transactions through statistical model checking. In: ICFEM\u201917. Lecture Notes in Computer Science, vol. 10610, pp. 298\u2013314. Springer (2017)","DOI":"10.1007\/978-3-319-68690-5_18"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: Modeling and analyzing mobile ad hoc networks in Real-Time Maude. Journal of Logical and Algebraic Methods in Programming 85(1), 34\u201366 (2016)","DOI":"10.1016\/j.jlamp.2015.05.002"},{"key":"21_CR60","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Rahman, M.R., Ganhotra, J., Gupta, I., Meseguer, J.: Formal modeling and analysis of RAMP transaction systems. In: SAC\u201916. pp. 1700\u20131707. ACM (2016)","DOI":"10.1145\/2851613.2851838"},{"key":"21_CR61","doi-asserted-by":"crossref","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 of Computing 31(5), 503\u2013540 (2019)","DOI":"10.1007\/s00165-019-00489-w"},{"key":"21_CR62","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Meseguer, J.: Formal modeling and analysis of the Walter transactional data store. In: WRLA\u201918. Lecture Notes in Computer Science, vol. 11152, pp. 136\u2013152. Springer (2018)","DOI":"10.1007\/978-3-319-99840-4_8"},{"key":"21_CR63","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in Maude. In: TACAS\u201919. Lecture Notes in Computer Science, vol. 11428, pp. 40\u201357. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_3"},{"key":"21_CR64","doi-asserted-by":"crossref","unstructured":"Liu, S., Rahman, M.R., Skeirik, S., Gupta, I., Meseguer, J.: Formal modeling and analysis of Cassandra in Maude. In: ICFEM\u201914. Lecture Notes in Computer Science, vol.\u00a08829, pp. 332\u2013347. Springer (2014)","DOI":"10.1007\/978-3-319-11737-9_22"},{"key":"21_CR65","doi-asserted-by":"crossref","unstructured":"Liu, S., Sandur, A., Meseguer, J., \u00d6lveczky, P.C., Wang, Q.: Generating correct-by-construction distributed implementations from formal Maude designs. In: NFM\u201920. Lecture Notes in Computer Science, vol. 12229. Springer (2020)","DOI":"10.1007\/978-3-030-55754-6_2"},{"key":"21_CR66","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a lingua franca for deterministic concurrent systems. ACM Transactions on Embedded Computing Systems 20(4), 36:1\u201336:27 (2021)","DOI":"10.1145\/3448128"},{"key":"21_CR67","doi-asserted-by":"crossref","unstructured":"Marin, M., \u00d6lveczky, P.C., Reja, M., Rukhaia, M., Bae, K.: Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic. In: Rebeca for Actor Analysis in Action. Lecture Notes in Computer Science, vol. 15560. Springer (2025)","DOI":"10.1007\/978-3-031-85134-6_4"},{"key":"21_CR68","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73\u2013155 (1992)","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"21_CR69","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Recent Trends in Algebraic Development Techniques (WADT\u201997). LNCS, vol.\u00a01376, pp. 18\u201361. Springer (1997)","DOI":"10.1007\/3-540-64299-4_26"},{"key":"21_CR70","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Methods Program. 81(7-8), 721\u2013781 (2012)","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"21_CR71","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Taming distributed system complexity through formal patterns. Science of Computer Programming 83, 3\u201334 (2014)","DOI":"10.1016\/j.scico.2013.07.004"},{"key":"21_CR72","doi-asserted-by":"crossref","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theoretical Computer Science 451, 1\u201337 (2012)","DOI":"10.1016\/j.tcs.2012.05.040"},{"key":"21_CR73","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Sharykin, R.: Specification and analysis of distributed object-based stochastic hybrid systems. In: HSCC\u201906. Lecture Notes in Computer Science, vol.\u00a03927, pp. 460\u2013475. Springer (2006)","DOI":"10.1007\/11730637_35"},{"key":"21_CR74","doi-asserted-by":"crossref","unstructured":"Misra, J., Cook, W.R.: Computation orchestration. Software and Systems Modeling 6(1), 83\u2013110 (2007)","DOI":"10.1007\/s10270-006-0012-1"},{"key":"21_CR75","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Formal analysis of android application behavior with Real-Time Maude. In: CPSNA\u201915. pp. 7\u201312. IEEE Computer Society (2015)","DOI":"10.1109\/CPSNA.2015.11"},{"key":"21_CR76","doi-asserted-by":"crossref","unstructured":"Nakajima, S.: Using Real-Time Maude to model check energy consumption behavior. In: FM\u201915. Lecture Notes in Computer Science, vol.\u00a09109, pp. 378\u2013394. Springer (2015)","DOI":"10.1007\/978-3-319-19249-9_24"},{"key":"21_CR77","doi-asserted-by":"crossref","unstructured":"Nigam, V., Kim, M., Mason, I.A., Talcott, C.L.: Detection and diagnosis of deviations in distributed systems of autonomous agents. Mathematical Structures in Computer Science 32(9), 1254\u20131282 (2022)","DOI":"10.1017\/S0960129522000251"},{"key":"21_CR78","doi-asserted-by":"crossref","unstructured":"Nigam, V., Talcott, C.L.: Automating safety proofs about cyber-physical systems using rewriting modulo SMT. In: WRLA\u201922. Lecture Notes in Computer Science, vol. 13252, pp. 212\u2013229. Springer (2022)","DOI":"10.1007\/978-3-031-12441-9_11"},{"key":"21_CR79","doi-asserted-by":"crossref","unstructured":"Olarte, C., \u00d6lveczky, P.C.: Timed strategies for real-time rewrite theories. In: WRLA\u201924. Lecture Notes in Computer Science, vol. 14953. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65941-6_7"},{"key":"21_CR80","unstructured":"Olarte, C., \u00d6lveczky, P.C.: RT-strategies (2025), https:\/\/depot.lipn.univ-paris13.fr\/real-time-maude\/rtm-strategies"},{"key":"21_CR81","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Semantics, simulation, and formal analysis of modeling languages for embedded systems in Real-Time Maude. In: Formal Modeling: Actors, Open Systems, Biological Systems \u2013 Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, LNCS, vol.\u00a07000, pp. 368\u2013402. Springer (2011)","DOI":"10.1007\/978-3-642-24933-4_19"},{"key":"21_CR82","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Rewriting Logic and Its Applications (WRLA 2014). Lecture Notes in Computer science, vol.\u00a08663, pp. 42\u201379. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"21_CR83","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Formalizing and validating the P-Store replicated data store in Maude. In: WADT\u201916. Lecture Notes in Computer Science, vol. 10644, pp. 189\u2013207. Springer (2016)","DOI":"10.1007\/978-3-319-72044-9_13"},{"key":"21_CR84","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: FMOODS\/FORTE\u201910. Lecture Notes in Computer Science, vol.\u00a06117, pp. 47\u201362. Springer (2010)","DOI":"10.1007\/978-3-642-13464-7_5"},{"key":"21_CR85","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: FASE\u201906. Lecture Notes in Computer Science, vol.\u00a03922, pp. 357\u2013372. Springer (2006)","DOI":"10.1007\/11693017_26"},{"key":"21_CR86","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285(2), 359\u2013405 (2002)","DOI":"10.1016\/S0304-3975(01)00363-2"},{"key":"21_CR87","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. In: WRLA\u201906. Electronic Notes in Theoretical Computer Science, vol.\u00a0176, pp. 5\u201327. Elsevier (2006)","DOI":"10.1016\/j.entcs.2007.06.005"},{"key":"21_CR88","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161\u2013196 (2007)","DOI":"10.1007\/s10990-007-9001-5"},{"key":"21_CR89","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The Real-Time Maude tool. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). Lecture Notes in Computer Science, vol.\u00a04963, pp. 332\u2013336. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_23"},{"key":"21_CR90","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design 29(3), 253\u2013293 (2006)","DOI":"10.1007\/s10703-006-0015-0"},{"key":"21_CR91","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Prabhakar, P., Liu, X.: Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude. In: IPDPS\u201908. pp.\u00a01\u20138. IEEE (2008)","DOI":"10.1109\/IPDPS.2008.4536574"},{"key":"21_CR92","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science 410(2-3), 254\u2013280 (2009)","DOI":"10.1016\/j.tcs.2008.09.022"},{"key":"21_CR93","doi-asserted-by":"crossref","unstructured":"Pita, I., Riesco, A.: Specifying and analyzing the Kademlia protocol in Maude. In: ICTAC\u201915. Lecture Notes in Computer Science, vol.\u00a09399, pp. 524\u2013541. Springer (2015)","DOI":"10.1007\/978-3-319-25150-9_30"},{"key":"21_CR94","unstructured":"Ptolemaeus, C. (ed.): System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org (2014), http:\/\/ptolemy.org\/books\/Systems"},{"key":"21_CR95","doi-asserted-by":"crossref","unstructured":"Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: A graphical approach for modeling time-dependent behavior of DSLs. In: IEEE Symposium on Visual Languages and Human-Centric Computing, VL\/HCC 2009. pp. 51\u201355. IEEE Computer Society (2009)","DOI":"10.1109\/VLHCC.2009.5295300"},{"key":"21_CR96","doi-asserted-by":"crossref","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.A.: Rewriting modulo SMT and open system analysis. Journal of Logical and Algebraic Methods in Programming 86(1), 269\u2013297 (2017)","DOI":"10.1016\/j.jlamp.2016.10.001"},{"key":"21_CR97","doi-asserted-by":"crossref","unstructured":"Romero, J.R., Rivera, J.E., Dur\u00e1n, F., Vallecillo, A.: Formal and tool support for model driven engineering with Maude. J. Object Technol. 6(9), 187\u2013207 (2007)","DOI":"10.5381\/jot.2007.6.9.a10"},{"key":"21_CR98","doi-asserted-by":"crossref","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. Journal of Logical and Algebraic Methods in Programming 123, 100700 (2021)","DOI":"10.1016\/j.jlamp.2021.100700"},{"key":"21_CR99","doi-asserted-by":"crossref","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng. 29(1), \u00a07 (2022)","DOI":"10.1007\/s10515-021-00307-9"},{"key":"21_CR100","doi-asserted-by":"crossref","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: QMaude: Quantitative specification and verification in rewriting logic. In: Formal Methods (FM 2023). Lecture Notes in Computer Science, vol. 14000. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_15"},{"key":"21_CR101","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering 25(5), 651\u2013660 (1999)","DOI":"10.1109\/32.815324"},{"key":"21_CR102","doi-asserted-by":"crossref","unstructured":"Sabahi-Kaviani, Z., Khosravi, R., \u00d6lveczky, P.C., Khamespanah, E., Sirjani, M.: Formal semantics and efficient analysis of Timed Rebeca in Real-Time Maude. Science of Computer Programming 113, 85\u2013118 (2015)","DOI":"10.1016\/j.scico.2015.07.003"},{"key":"21_CR103","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Computer Aided Verification (CAV 2004). Lecture Notes in Computer Science, vol.\u00a03114. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"21_CR104","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Computer Aided Verification (CAV 2005). Lecture Notes in Computer Science, vol.\u00a03576. Springer (2005)","DOI":"10.1007\/11513988_26"},{"key":"21_CR105","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: Second International Conference on the Quantitative Evaluation of Systems (QEST 2005). IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"21_CR106","doi-asserted-by":"crossref","unstructured":"Skeirik, S., Bobba, R.B., Meseguer, J.: Formal analysis of fault-tolerant group key management using ZooKeeper. In: CCGrid\u201913. pp. 636\u2013641. IEEE Computer Society (2013)","DOI":"10.1109\/CCGrid.2013.98"},{"key":"21_CR107","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J.: Formal specification of button-related fault-tolerance micropatterns. In: WRLA\u201914. Lecture Notes in Computer Science, vol.\u00a08663, pp. 263\u2013279. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_15"},{"key":"21_CR108","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J., Sha, L.: A formal pattern architecture for safe medical systems. In: WRLA\u201910. Lecture Notes in Computer Science, vol.\u00a06381, pp. 157\u2013173. Springer (2010)","DOI":"10.1007\/978-3-642-16310-4_11"},{"key":"21_CR109","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Computer Aided Verification (CAV 2002). Lecture Notes in Computer Science, vol.\u00a02404. Springer (2002)","DOI":"10.1007\/3-540-45657-0_17"},{"key":"21_CR110","doi-asserted-by":"crossref","unstructured":"Yu, G., Bae, K.: A flexible framework for integrating Maude and SMT solvers using Python. In: WRLA\u201924. Lecture Notes in Computer Science, vol. 14953, pp. 179\u2013192. Springer (2024)","DOI":"10.1007\/978-3-031-65941-6_10"},{"key":"21_CR111","doi-asserted-by":"crossref","unstructured":"Zhu, L., Liu, P., Shi, J., Wang, Z., Zhu, H.: A timing verification framework for AUTOSAR OS component development based on Real-Time Maude. In: TASE\u201913. pp. 29\u201336. IEEE Computer Society (2013)","DOI":"10.1109\/TASE.2013.12"}],"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_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T18:32:37Z","timestamp":1760725957000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05291-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032052902","9783032052919"],"references-count":111,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05291-9_21","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"}}]}}