{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T18:27:42Z","timestamp":1787509662219,"version":"build-2736575974"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T00:00:00Z","timestamp":1766361600000},"content-version":"vor","delay-in-days":21,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"funder":[{"DOI":"10.13039\/501100002541","name":"Pohang University of Science and Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002541","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s10009-025-00831-z","type":"journal-article","created":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T07:51:26Z","timestamp":1766389886000},"page":"597-622","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["MR-HybridSynchAADL: formal modeling and analysis of multirate CPSs with advanced control programs and continuous dynamics"],"prefix":"10.1007","volume":"27","author":[{"given":"Jaehun","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,12,22]]},"reference":[{"key":"831_CR1","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1145\/2663171.2663178","volume-title":"Proc. HILT\u201914","author":"E. Ahmad","year":"2014","unstructured":"Ahmad, E., Larson, B.R., Barrett, S.C., Zhan, N., Dong, Y.: Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. In: Proc. HILT\u201914, pp.\u00a029\u201338. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2663171.2663178"},{"key":"831_CR2","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1109\/RTSS.2009.50","volume-title":"Proc. RTSS\u201909","author":"A. Al-Nayeem","year":"2009","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: Proc. RTSS\u201909, pp.\u00a0161\u2013170. IEEE (2009). https:\/\/doi.org\/10.1109\/RTSS.2009.50"},{"key":"831_CR3","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/ICCPS.2012.15","volume-title":"Proc. ICCPS\u201912","author":"A. Al-Nayeem","year":"2012","unstructured":"Al-Nayeem, A., Sha, L., Cofer, D.D., Miller, S.M.: Pattern-based composition and analysis of virtually synchronized real-time distributed systems. In: Proc. ICCPS\u201912, pp.\u00a065\u201374. IEEE (2012). https:\/\/doi.org\/10.1109\/ICCPS.2012.15"},{"issue":"3\u20134","key":"831_CR4","doi-asserted-by":"publisher","first-page":"261","DOI":"10.3233\/FI-242195","volume":"192","author":"J. Arias","year":"2024","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. Fundam. Inform. 192(3\u20134), 261\u2013312 (2024). https:\/\/doi.org\/10.3233\/FI-242195","journal-title":"Fundam. Inform."},{"key":"831_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2023.103074","volume":"233","author":"J. Arias","year":"2024","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, 103074 (2024). https:\/\/doi.org\/10.1016\/J.SCICO.2023.103074","journal-title":"Sci. Comput. Program."},{"key":"831_CR6","unstructured":"Bae, K.: Rewriting-based model checking methods. Ph.D. thesis, University of Illinois at Urbana-Champaign (2014) http:\/\/hdl.handle.net\/2142\/50553"},{"issue":"5s","key":"831_CR7","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. 20(5s), 1\u201326 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"831_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-319-68034-7_5","volume-title":"Proc. FACS\u201917","author":"K. Bae","year":"2017","unstructured":"Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proc. FACS\u201917. LNCS, vol.\u00a010487, pp.\u00a078\u201397. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5"},{"key":"831_CR9","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K. Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.03.006","journal-title":"Sci. Comput. Program."},{"key":"831_CR10","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). https:\/\/doi.org\/10.1016\/j.scico.2013.09.010","journal-title":"Sci. Comput. Program."},{"key":"831_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-06410-9_7","volume-title":"Proc. FM\u201914","author":"K. Bae","year":"2014","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Proc. FM\u201914. LNCS, vol.\u00a08442, pp.\u00a094\u2013109. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_7"},{"key":"831_CR12","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/2883817.2883849","volume-title":"Proc. HSCC\u201916","author":"K. Bae","year":"2016","unstructured":"Bae, K., \u00d6lveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proc. HSCC\u201916, pp.\u00a0145\u2013154. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2883817.2883849"},{"issue":"12","key":"831_CR13","doi-asserted-by":"publisher","first-page":"1989","DOI":"10.1109\/TCAD.2017.2681076","volume":"36","author":"Y. Bao","year":"2017","unstructured":"Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 36(12), 1989\u20132002 (2017). https:\/\/doi.org\/10.1109\/TCAD.2017.2681076","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"831_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Proc. CAV\u201911","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proc. CAV\u201911. LNCS, vol.\u00a06806, pp.\u00a0171\u2013177. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"831_CR15","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/3302504.3311804","volume-title":"Proc. HSCC\u201919","author":"S. Bogomolov","year":"2019","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: Proc. HSCC\u201919, pp.\u00a039\u201344. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3302504.3311804"},{"key":"831_CR16","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1109\/REAL.2000.896018","volume-title":"Proc. RTSS\u201900","author":"M. Caccamo","year":"2000","unstructured":"Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: Proc. RTSS\u201900, pp.\u00a0295\u2013304. IEEE (2000). https:\/\/doi.org\/10.1109\/REAL.2000.896018"},{"key":"831_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Proc. CAV\u201913","author":"X. Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Proc. CAV\u201913. LNCS, vol.\u00a08044, pp.\u00a0258\u2013263. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"831_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Proc. TACAS\u201915","author":"A. Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Proc. TACAS\u201915. LNCS, vol.\u00a09035, pp.\u00a052\u201367. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_4"},{"key":"831_CR19","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude \u2013 a High-Performance Logical Framework","author":"M. Clavel","year":"2007","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. LNCS, vol.\u00a04350. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"831_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Proc. CAV\u201914","author":"B. Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Proc. CAV\u201914. LNCS, vol.\u00a08559, pp.\u00a0737\u2013744. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"831_CR21","volume-title":"Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language","author":"P.H. Feiler","year":"2012","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":"831_CR22","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1109\/ICECCS.2007.41","volume-title":"Proc. ICECCS\u201907","author":"R. Fran\u00e7a","year":"2007","unstructured":"Fran\u00e7a, R., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL behaviour annex\u00a0- experiments and roadmap. In: Proc. ICECCS\u201907, pp.\u00a0377\u2013382. IEEE (2007). https:\/\/doi.org\/10.1109\/ICECCS.2007.41"},{"key":"831_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Proc. CAV\u201911","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proc. CAV\u201911. LNCS, vol.\u00a06806, pp.\u00a0379\u2013395. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"831_CR24","volume-title":"Architecture Analysis and Design Language (AADL) Annex Volume 2: Annex B: Data Modeling Annex","author":"S.A.E. International","year":"2011","unstructured":"International, S.A.E.: Architecture Analysis and Design Language (AADL) Annex Volume 2: Annex B: Data Modeling Annex (2011)"},{"key":"831_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Proc. TACAS\u201915","author":"S. Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.M.: dReach: $\\delta $-reachability analysis for hybrid systems. In: Proc. TACAS\u201915. LNCS, vol.\u00a07898, pp.\u00a0200\u2013205. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15"},{"issue":"2","key":"831_CR26","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3567425","volume":"22","author":"A. Kundu","year":"2023","unstructured":"Kundu, A., Das, S., Ray, R.: SAT-reach: a bounded model checker for affine hybrid systems. ACM Trans. Embed. Comput. Syst. 22(2), 26:1\u201326:36 (2023). https:\/\/doi.org\/10.1145\/3567425","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"831_CR27","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-032-07106-4_14","volume-title":"Proc. SAS\u201925","author":"J. Lee","year":"2025","unstructured":"Lee, J., Bae, K.: Formal analysis of networked PLC controllers interacting with physical environments. In: Proc. SAS\u201925. LNCS, vol.\u00a016100, pp.\u00a0328\u2013356. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-032-07106-4_14"},{"key":"831_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-031-71162-6_22","volume-title":"Formal Methods","author":"J. Lee","year":"2025","unstructured":"Lee, J., Bae, K.: Formal semantics and analysis of multitask PLC ST programs with preemption. In: Formal Methods. LNCS, vol.\u00a014933, pp.\u00a0425\u2013442. Springer, Cham (2025)"},{"key":"831_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-81685-8_23","volume-title":"Proc. CAV\u201921","author":"J. Lee","year":"2021","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Proc. CAV\u201921. LNCS, vol.\u00a012759, pp.\u00a0491\u2013504. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23"},{"key":"831_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-031-19759-8_4","volume-title":"Proc. ISOLA\u201922","author":"J. Lee","year":"2022","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs. In: Proc. ISOLA\u201922. LNCS, vol.\u00a013703, pp.\u00a059\u201376. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-19759-8_4"},{"issue":"6","key":"831_CR31","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). https:\/\/doi.org\/10.1007\/s10009-022-00665-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"831_CR32","first-page":"56","volume-title":"Proc. FTSCS\u201922","author":"J. Lee","year":"2022","unstructured":"Lee, J., Kim, S., Bae, K.: Bounded model checking of PLC ST programs using rewriting modulo SMT. In: Proc. FTSCS\u201922, pp.\u00a056\u201367. ACM, New York (2022)"},{"key":"831_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-031-75107-3_15","volume-title":"Proc. ISOLA\u201924","author":"J. Lee","year":"2024","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: Rigorous model engineering of hierarchical multirate CPSs in MR-HybridSynchAADL. In: Proc. ISOLA\u201924. Lecture Notes in Computer Science, vol.\u00a015220, pp.\u00a0243\u2013262. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-75107-3_15"},{"key":"831_CR34","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: Supplementary material. https:\/\/hybridsynchaadl.github.io\/artifact\/isola2024"},{"key":"831_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-031-37706-8_18","volume-title":"Proc. CAV\u201923","author":"Y. Li","year":"2023","unstructured":"Li, Y., Zhu, H., Braught, K., Shen, K., Mitra, S.: Verse: a Python library for reasoning about multi-agent hybrid system scenarios. In: Proc. CAV\u201923. LNCS, vol.\u00a013964, pp.\u00a0351\u2013364. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_18"},{"issue":"3","key":"831_CR36","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/s11704-018-7039-7","volume":"13","author":"J. Liu","year":"2019","unstructured":"Liu, J., Li, T., Ding, Z., Qian, Y., Sun, H., He, J.: AADL+: a simulation-based methodology for cyber-physical systems. Front. Comput. Sci. 13(3), 516\u2013538 (2019). https:\/\/doi.org\/10.1007\/s11704-018-7039-7","journal-title":"Front. Comput. Sci."},{"issue":"4","key":"831_CR37","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. 20(4), 1\u201327 (2021)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"831_CR38","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-031-85134-6_4","volume-title":"Rebeca for Actor Analysis in Action \u2013 Essays Dedicated to Marjan Sirjani on the Occasion of Her 60th Birthday","author":"M. Marin","year":"2025","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 \u2013 Essays Dedicated to Marjan Sirjani on the Occasion of Her 60th Birthday. LNCS, vol.\u00a015560, pp.\u00a070\u2013101. Springer, Berlin (2025). https:\/\/doi.org\/10.1007\/978-3-031-85134-6_4"},{"issue":"1","key":"831_CR39","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. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theor. Comput. Sci."},{"key":"831_CR40","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). https:\/\/doi.org\/10.1016\/j.tcs.2012.05.040","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"831_CR41","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.jlap.2009.07.003","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":"J. Log. Algebr. Program."},{"key":"831_CR42","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Proc. WRLA\u201914","author":"P.C. \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Proc. WRLA\u201914. LNCS, vol.\u00a08663, pp.\u00a042\u201379. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3"},{"key":"831_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11693017_26","volume-title":"Proc. FASE\u201922","author":"P.C. \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Proc. FASE\u201922. LNCS, vol.\u00a03922, pp.\u00a0357\u2013372. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11693017_26"},{"key":"831_CR44","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symb. Comput. 20, 161\u2013196 (2007). https:\/\/doi.org\/10.1007\/s10990-007-9001-5","journal-title":"High.-Order Symb. Comput."},{"key":"831_CR45","doi-asserted-by":"publisher","first-page":"27:1","DOI":"10.1145\/2532443.2532473","volume-title":"Proc. Internetware\u201913","author":"Y. Qian","year":"2013","unstructured":"Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proc. Internetware\u201913, pp.\u00a027:1\u201327:4. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2532443.2532473"},{"issue":"1","key":"831_CR46","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. Algebr. Methods Program. 86(1), 269\u2013297 (2017). https:\/\/doi.org\/10.1016\/j.jlamp.2016.10.001","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"5","key":"831_CR47","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1109\/32.815324","volume":"25","author":"J. Rushby","year":"1999","unstructured":"Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Softw. Eng. 25(5), 651\u2013660 (1999)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"831_CR48","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-57288-8_20","volume-title":"Proc. NFM\u201917","author":"S. Schupp","year":"2017","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Makhlouf, I.B., Kowalewski, S.: HyPro: a C++ library of state set representations for hybrid systems reachability analysis. In: Proc. NFM\u201917. LNCS, vol.\u00a010227, pp.\u00a0288\u2013294 (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_20"},{"key":"831_CR49","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-15545-6_18","volume":"8950","author":"C. Talcott","year":"2015","unstructured":"Talcott, C., Arbab, F., Yadav, M.: Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. Softw. Serv. Syst. 8950, 273\u2013290 (2015). https:\/\/doi.org\/10.1007\/978-3-319-15545-6_18","journal-title":"Softw. Serv. Syst."},{"key":"831_CR50","series-title":"LNCS","volume-title":"Proc. WRLA\u201924","author":"G. Yu","year":"2024","unstructured":"Yu, G., Bae, K.: A flexible framework for integrating Maude and SMT solvers using Python. In: Proc. WRLA\u201924. LNCS, vol.\u00a014953. Springer, Berlin (2024)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00831-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00831-z","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00831-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T16:12:58Z","timestamp":1771863178000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00831-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":50,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["831"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00831-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"13 December 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}