{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T05:22:40Z","timestamp":1771910560123,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031751066","type":"print"},{"value":"9783031751073","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T00:00:00Z","timestamp":1729987200000},"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-75107-3_15","type":"book-chapter","created":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T07:01:50Z","timestamp":1729926110000},"page":"243-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL"],"prefix":"10.1007","author":[{"given":"Jaehun","family":"Lee","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0708-3721","authenticated-orcid":false,"given":"Peter","family":"Csaba \u00d6lveczky","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,27]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","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. 29\u201338. ACM (2014). https:\/\/doi.org\/10.1145\/2663171.2663178","DOI":"10.1145\/2663171.2663178"},{"key":"15_CR2","doi-asserted-by":"publisher","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. 65\u201374. IEEE (2012). https:\/\/doi.org\/10.1109\/ICCPS.2012.15","DOI":"10.1109\/ICCPS.2012.15"},{"key":"15_CR3","doi-asserted-by":"publisher","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. 161\u2013170. IEEE (2009). https:\/\/doi.org\/10.1109\/RTSS.2009.50","DOI":"10.1109\/RTSS.2009.50"},{"key":"15_CR4","unstructured":"Bae, K.: Rewriting-based model checking methods. Ph.D. thesis, University of Illinois at Urbana-Champaign (2014), http:\/\/hdl.handle.net\/2142\/50553"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Science of Computer Programming 91, 3\u201344 (2014). https:\/\/doi.org\/10.1016\/j.scico.2013.09.010","DOI":"10.1016\/j.scico.2013.09.010"},{"key":"15_CR6","doi-asserted-by":"publisher","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. 145\u2013154. ACM (2016). https:\/\/doi.org\/10.1145\/2883817.2883849","DOI":"10.1145\/2883817.2883849"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of Multirate Synchronous AADL. In: Proc. FM\u201914. LNCS, vol.\u00a08442, pp. 94\u2013109. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_7","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proc. FACS\u201917. LNCS, vol. 10487, pp. 78\u201397. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_5","DOI":"10.1007\/978-3-319-68034-7_5"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Science of Computer Programming 178, 20\u201342 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.03.006","DOI":"10.1016\/j.scico.2019.03.006"},{"issue":"12","key":"15_CR10","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 Transactions on CAD of Integrated Circuits and Systems 36(12), 1989\u20132002 (2017). https:\/\/doi.org\/10.1109\/TCAD.2017.2681076","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"key":"15_CR11","doi-asserted-by":"publisher","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. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Caccamo, M., Buttazzo, G., Sha, L.: Capacity sharing for overrun control. In: Proc. RTSS\u201900. pp. 295\u2013304. IEEE (2000). https:\/\/doi.org\/10.1109\/REAL.2000.896018","DOI":"10.1109\/REAL.2000.896018"},{"key":"15_CR13","doi-asserted-by":"publisher","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 (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1","DOI":"10.1007\/978-3-540-71999-1"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Proc. CAV\u201914. LNCS, vol.\u00a08559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"15_CR15","volume-title":"Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language","author":"PH 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":"15_CR16","doi-asserted-by":"publisher","unstructured":"Fran\u00e7a, R., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex - experiments and roadmap. In: Proc. ICECCS\u201907. IEEE (2007). https:\/\/doi.org\/10.1109\/ICECCS.2007.41","DOI":"10.1109\/ICECCS.2007.41"},{"key":"15_CR17","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: Supplementary material, https:\/\/hybridsynchaadl.github.io\/artifact\/isola2024"},{"key":"15_CR18","doi-asserted-by":"publisher","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. 13703, pp. 59\u201376. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19759-8_4","DOI":"10.1007\/978-3-031-19759-8_4"},{"issue":"6","key":"15_CR19","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. Transfer 24(6), 911\u2013948 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00665-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR20","doi-asserted-by":"publisher","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. 12759, pp. 491\u2013504. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23","DOI":"10.1007\/978-3-030-81685-8_23"},{"issue":"3","key":"15_CR21","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. Comp. Sci. 13(3), 516\u2013538 (2019). https:\/\/doi.org\/10.1007\/s11704-018-7039-7","journal-title":"Front. Comp. Sci."},{"issue":"1","key":"15_CR22","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). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR23","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.tcs.2012.05.040","DOI":"10.1016\/j.tcs.2012.05.040"},{"issue":"2","key":"15_CR24","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. Logic Algebraic Program. 79(2), 103\u2013143 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2009.07.003","journal-title":"J. Logic Algebraic Program."},{"key":"15_CR25","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 and Symbolic Computation 20, 161\u2013196 (2007). https:\/\/doi.org\/10.1007\/s10990-007-9001-5","journal-title":"Higher-Order and Symbolic Computation"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Proc. WRLA\u201914. LNCS, vol.\u00a08663. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_3","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"15_CR27","doi-asserted-by":"publisher","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. 357\u2013372. Springer (2006). https:\/\/doi.org\/10.1007\/11693017_26","DOI":"10.1007\/11693017_26"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proc. Internetware\u201913. ACM (2013). https:\/\/doi.org\/10.1145\/2532443.2532473","DOI":"10.1145\/2532443.2532473"},{"issue":"1","key":"15_CR29","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. Journal of Logical and Algebraic Methods in Programming 86(1), 269\u2013297 (2017). https:\/\/doi.org\/10.1016\/j.jlamp.2016.10.001","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"15_CR30","unstructured":"SAE International: Architecture Analysis and Design Language (AADL) annex volume 2: Annex B: Data modeling annex (2011)"},{"key":"15_CR31","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. Software, Services, and Systems 8950, 273\u2013290 (2015). https:\/\/doi.org\/10.1007\/978-3-319-15545-6_18","journal-title":"Software, Services, and Systems"},{"key":"15_CR32","unstructured":"Yu, G., Bae, K.: Maude-SE: a tight integration of Maude and SMT solvers. Preliminary proceedings of WRLA@ETAPS pp. 220\u2013232 (2020)"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"Yu, G., Bae, K.: A flexible framework for integrating Maude and SMT solvers using Python. In: Proc. WRLA\u201924. LNCS, vol. 14953. Springer (2024)","DOI":"10.1007\/978-3-031-65941-6_10"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75107-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,26]],"date-time":"2024-10-26T07:12:58Z","timestamp":1729926778000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75107-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,27]]},"ISBN":["9783031751066","9783031751073"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75107-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,27]]},"assertion":[{"value":"27 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}