{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:56Z","timestamp":1781238836040,"version":"3.54.1"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031851339","type":"print"},{"value":"9783031851346","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-85134-6_4","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T04:01:24Z","timestamp":1742443284000},"page":"70-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Semantics and\u00a0Formal Analysis of\u00a0Lingua Franca CPS Specifications in\u00a0Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Mircea","family":"Marin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mario","family":"Reja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mikheil","family":"Rukhaia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cimini, M., Ing\u00f3lfsd\u00f3ttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using Timed Rebeca. In: 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2011). EPTCS, vol.\u00a058, pp. 1\u201319 (2011)","DOI":"10.4204\/EPTCS.58.1"},{"key":"4_CR2","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: Proceedings of the RTSS, pp. 161\u2013170. IEEE, USA (2009)","DOI":"10.1109\/RTSS.2009.50"},{"key":"4_CR3","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: International Conference on Fundamental Approaches to Software Engineering, pp. 262\u2013277. Springer (2009)","DOI":"10.1007\/978-3-642-00593-0_18"},{"key":"4_CR4","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. Sci. Comput. Program. 233 (2024)","DOI":"10.1016\/j.scico.2023.103074"},{"key":"4_CR5","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."},{"issue":"5s","key":"4_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3477036","volume":"20","author":"K Bae","year":"2021","unstructured":"Bae, K., \u00d6lveczky, P.C.: MSYNC: a generalized formal design pattern for virtually synchronous multirate cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 20(5s), 1\u201326 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"4_CR7","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: Proceedings of the International Conference on Formal Aspects of Component Software (FACS 2023). Lecture Notes in Computer Science. Springer (2023)","DOI":"10.1007\/978-3-031-52183-6_7"},{"key":"4_CR8","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: Proceedings of the ICFEM 2011. LNCS, vol. 6991. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24559-6_43"},{"issue":"12","key":"4_CR9","doi-asserted-by":"publisher","first-page":"1235","DOI":"10.1016\/j.scico.2010.10.002","volume":"77","author":"K Bae","year":"2012","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. Sci. Comput. Program. 77(12), 1235\u20131271 (2012)","journal-title":"Sci. Comput. Program."},{"key":"4_CR10","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 of the HSCC, pp. 145\u2013154. ACM, New York (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: Proceedings of the FM 2014. LNCS, vol. 8442. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: Proceedings of the FASE 2012. LNCS, vol. 7212. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28872-2_4"},{"issue":"9","key":"4_CR13","doi-asserted-by":"publisher","first-page":"1270","DOI":"10.1109\/5.97297","volume":"79","author":"A Benveniste","year":"1991","unstructured":"Benveniste, A., Berry, G.: The synchronous approach to reactive and real-time systems. Proc. IEEE 79(9), 1270\u20131282 (1991)","journal-title":"Proc. IEEE"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Bousse, E., Degueule, T., Vojtisek, D., Mayerhofer, T., Deantoni, J., Combemale, B.: Execution Framework of the GEMOC Studio (Tool Demo). In: Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language Engineering, pp. 84\u201389 (2016)","DOI":"10.1145\/2997364.2997384"},{"key":"4_CR15","unstructured":"Cassandras, C.G.: Discrete Event Systems, Modeling and Performance Analysis. Irwin (1993)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Chen, X., Ro\u015fu, G.: $$\\mathbb{K}$$\u2014a semantic framework for programming languages and formal analysis. In: 5th International School on Engineering Trustworthy Software Systems (SETSS 2019), pp. 122\u2013158. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-55089-9_4"},{"key":"4_CR17","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude \u2013 A High-Performance Logical Framework. Lecture Notes in Computer Science, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Combemale, B., De Antoni, J., Larsen, M.V., Mallet, F., Barais, O., Baudry, B., France, R.B.: Reifying concurrency for executable metamodeling. In: Software Language Engineering: 6th International Conference, SLE 2013, Indianapolis, IN, USA, 26\u201328 October 2013, Proceedings 6, pp. 365\u2013384. Springer (2013)","DOI":"10.1007\/978-3-319-02654-1_20"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Deantoni, J., Cambeiro, J., Bateni, S., Lin, S., Lohstroh, M.: Debugging and verification tools for Lingua Franca in GEMOC studio. In: 2021 Forum on Specification & Design Languages (FDL), pp. 01\u201308. IEEE (2021)","DOI":"10.1109\/FDL53530.2021.9568383"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Edwards, S., Hui, J.: The sparse synchronous model. In: Forum for Specification and Design Languages (FDL 2020). IEEE (2020)","DOI":"10.1109\/FDL50818.2020.9232938"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez-Burgue\u00f1o, A., \u00d6lveczky, P.C.: Formalizing and analyzing security ceremonies with heterogeneous devices in ANP and PDL. In: Proceedings of the Fundamentals of Software Engineering (FSEN 2019). Lecture Notes in Computer Science, vol. 11761, pp. 129\u2013144. Springer (2019)","DOI":"10.1007\/978-3-030-31517-7_9"},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.scico.2016.03.004","volume":"128","author":"A Jafari","year":"2016","unstructured":"Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: PTRebeca: Modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22\u201350 (2016)","journal-title":"Sci. Comput. Program."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Jahandideh, I., Ghassemi, F., Sirjani, M.: Hybrid Rebeca: Modeling and analyzing of cyber-physical systems. In: International Workshop on Cyber Physical Systems: Model-Based Design (CyPhy 2018 and WESE 2018). Lecture Notes in Computer Science, vol. 11615, pp. 3\u201327. Springer (2018)","DOI":"10.1007\/978-3-030-23703-5_1"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Lee, E.A., Sirjani, M.: What Good are Models? In: Bae, K., \u00d6lveczky, P.C. (eds.) Formal Aspects of Component Software (FACS 2018). Lecture Notes in Computer Science, vol. 11222, pp. 3\u201331. Springer (2018)","DOI":"10.1007\/978-3-030-02146-7_1"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Lee, E.A., Zheng, H.: Leveraging synchronous language principles for heterogeneous modeling and design of embedded systems. In: Proceedings of the EMSOF 2007 (2007)","DOI":"10.1145\/1289927.1289949"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: International Symposium on Leveraging Applications of Formal Methods. LNCS, vol. 13703, pp. 47\u201364. Springer (2022)","DOI":"10.1007\/978-3-031-19759-8_4"},{"issue":"6","key":"4_CR27","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/s10009-022-00665-z","volume":"24","author":"J Lee","year":"2022","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C., Kim, S., Kang, M.: Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL. Int. J. Softw. Tools Technol. Transf. 24(6), 911\u2013948 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR28","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: Proceedings of the CAV 2021. LNCS, vol. 12759, pp. 491\u2013504. Springer, Heidelberg (2021)","DOI":"10.1007\/978-3-030-81685-8_23"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.scico.2014.06.006","volume":"99","author":"D Lepri","year":"2015","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. Sci. Comput. Program. 99, 128\u2013192 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"5s","key":"4_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3609134","volume":"22","author":"S Lin","year":"2023","unstructured":"Lin, S., et al.: Towards Building Verifiable CPS using Lingua Franca. ACM Trans. Embed. Comput. Syst. 22(5s), 1\u201324 (2023)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"4_CR31","unstructured":"Lohstroh, M., et al.: Reactors: A deterministic model for composable reactive systems. In: 8th International Workshop on Model-based Design of Cyber Physical Systems (CyPhy 2019). LNCS, vol. 11971. Springer (2019)"},{"key":"4_CR32","unstructured":"Lohstroh, M.: Reactors: A Deterministic Model of Concurrent Computation for Reactive Systems. Ph.D. thesis, EECS Department, University of California, Berkeley (2020)"},{"issue":"4","key":"4_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3448128","volume":"20","author":"M Lohstroh","year":"2021","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a Lingua Franca for Deterministic Concurrent Systems. ACM Trans. Embed. Comput. Syst. (TECS) 20(4), 1\u201327 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., et al.: Actors revisited for time-critical systems. In: Proceedings of the 56th Design Automation Conference 2019 (DAC 2019), pp. 152:1-152:4. ACM (2019)","DOI":"10.1145\/3316781.3323469"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Marin, M., \u00d6lveczky, P.C., Reja, M., Rukhaia, M., Bae, K., Dundua, B.: Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic (2024). http:\/\/olveczky.se\/lf2maude-techrep.pdf","DOI":"10.1007\/978-3-031-85134-6_4"},{"issue":"4","key":"4_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3617687","volume":"20","author":"C Menard","year":"2023","unstructured":"Menard, C., Lohstroh, M., Bateni, S., Chorlian, M., Deng, A., Donovan, P., Fournier, C., Lin, S., Suchert, F., Tanneberger, T., et al.: High-performance deterministic concurrency using Lingua Franca. ACM Trans. Archit. Code Optim. 20(4), 1\u201329 (2023)","journal-title":"ACM Trans. Archit. Code Optim."},{"issue":"1","key":"4_CR37","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":"4_CR38","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. Theoret. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"4_CR39","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theoret. Comput. Sci. 373(3), 213\u2013237 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR40","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: Proceedings of the FMOODS\/FORTE 2010. LNCS, vol.\u00a06117, pp. 47\u201362. Springer (2010)","DOI":"10.1007\/978-3-642-13464-7_5"},{"issue":"1\u20132","key":"4_CR41","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. High.-Order Symb. Comput. 20(1\u20132), 161\u2013196 (2007)","journal-title":"High.-Order Symb. Comput."},{"key":"4_CR42","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. Lecture Notes in Computer Science, vol.\u00a07000, pp. 368\u2013402. Springer (2011)","DOI":"10.1007\/978-3-642-24933-4_19"},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Proc. WRLA 2014. LNCS, vol. 8663. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_3"},{"issue":"2","key":"4_CR44","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"PC \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoret. Comput. Sci. 285(2), 359\u2013405 (2002)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"4_CR45","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"4_CR46","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.scico.2015.07.003","volume":"113","author":"Z Sabahi-Kaviani","year":"2015","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. Sci. Comput. Program. 113, 85\u2013118 (2015)","journal-title":"Sci. Comput. Program."},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Sabahi-Kaviani, Z., Khosravi, R., Sirjani, M., \u00d6lveczky, P.C., Khamespanah, E.: Formal semantics and analysis of Timed Rebeca in Real-Time Maude. In: Formal Techniques for Safety-Critical Systems (FTSCS 2013). Communications in Computer and Information Science, vol.\u00a0419, pp. 178\u2013194. Springer (2013)","DOI":"10.1007\/978-3-319-05416-2_12"},{"key":"4_CR48","unstructured":"Sirjani, M.: Rebeca: Theory, applications, and tools. In: Formal Methods for Components and Objects (FMCO 2006). LNCS, vol.\u00a04709. Springer (2006)"},{"issue":"7","key":"4_CR49","doi-asserted-by":"publisher","first-page":"1068","DOI":"10.3390\/math8071068","volume":"8","author":"M Sirjani","year":"2020","unstructured":"Sirjani, M., Lee, E.A., Khamespanah, E.: Verification of cyberphysical systems. Mathematics 8(7), 1068 (2020)","journal-title":"Mathematics"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Yu, G., Bae, K.: A flexible framework for integrating Maude and SMT solvers using Python. In: Proceedings of the International Workshop on Rewriting Logic and its Applications (WRLA 2024). Lecture Notes in Computer Science, vol. 14953. Springer (2024)","DOI":"10.1007\/978-3-031-65941-6_10"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Lee, E.A., Liu, J.: A programming model for time-synchronized distributed real-time systems. In: Proceedings of the RTAS 2007. IEEE (2007)","DOI":"10.1109\/RTAS.2007.5"}],"container-title":["Lecture Notes in Computer Science","Rebeca for Actor Analysis in Action"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-85134-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T08:35:18Z","timestamp":1743496518000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85134-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031851339","9783031851346"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85134-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 March 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}