{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T18:16:46Z","timestamp":1787509006692,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197581","type":"print"},{"value":"9783031197598","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19759-8_4","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T05:07:32Z","timestamp":1666156052000},"page":"47-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["An Extension of\u00a0HybridSynchAADL and\u00a0Its Application to\u00a0Collaborating Autonomous UAVs"],"prefix":"10.1007","author":[{"given":"Jaehun","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0708-3721","authenticated-orcid":false,"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","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: Proceedings of the ACM SIGAda Annual Conference on High Integrity Language Technology (HILT 2014). ACM, NY (2014)","DOI":"10.1145\/2663171.2663178"},{"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 (2009)","DOI":"10.1109\/RTSS.2009.50"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal methods based development of a PCA infusion pump reference model: generic infusion pump (GIP) project. In: HCMDSS-MDPnP, pp. 23\u201333. IEEE (2007)","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using Multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015)","journal-title":"Sci. Comput. Program."},{"key":"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. Embedd. Comput. Syst. 20(5s), 1\u201326 (2021)","journal-title":"ACM Trans. Embedd. Comput. Syst."},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/978-3-642-24559-6_43","volume-title":"Formal Methods and Software Engineering","author":"K Bae","year":"2011","unstructured":"Bae, K., \u00d6lveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 651\u2013667. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24559-6_43"},{"key":"4_CR8","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, NY (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-06410-9_7","volume-title":"FM 2014: Formal Methods","author":"K Bae","year":"2014","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94\u2013109. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_7"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-28872-2_4","volume-title":"Fundamental Approaches to Software Engineering","author":"K Bae","year":"2012","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 59\u201362. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_4"},{"key":"4_CR11","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)","journal-title":"Sci. Comput. Program."},{"issue":"12","key":"4_CR12","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)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_4"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"4_CR18","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":"4_CR19","doi-asserted-by":"crossref","unstructured":"Fran\u00e7a, R., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex \u2013 experiments and roadmap. In: Proceedings of the ICECCS 2007. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Kim, C., Sun, M., Mohan, S., Yun, H., Sha, L., Abdelzaher, T.F.: A framework for the safe interoperability of medical devices in the presence of network failures. In: Proceedings of the 1st ACM\/IEEE International Conference on Cyber-Physical Systems (ICCPS), pp. 149\u2013158 (2010)","DOI":"10.1145\/1795194.1795215"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_15"},{"issue":"1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1109\/JPROC.2002.805821","volume":"91","author":"H Kopetz","year":"2003","unstructured":"Kopetz, H., Bauer, G.: The time-triggered architecture. Proc. IEEE 91(1), 112\u2013126 (2003)","journal-title":"Proc. IEEE"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Lee, J., Bae, K., \u00d6lveczky, P.C.: An extension of HybridSynchAADL and its application to collaborating autonomous UAVs (2022). http:\/\/hybridsynchaadl.github.io\/artifact\/isola2022\/techrep.pdf","DOI":"10.1007\/978-3-031-19759-8_4"},{"key":"4_CR25","doi-asserted-by":"publisher","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 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00665-z","DOI":"10.1007\/s10009-022-00665-z"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-81685-8_23","volume-title":"Computer Aided Verification","author":"J Lee","year":"2021","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: Hybrid\u00a0SynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 491\u2013504. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23"},{"issue":"6","key":"4_CR27","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1049\/cce:19990604","volume":"10","author":"G Leen","year":"1999","unstructured":"Leen, G., Heffernan, D., Dunne, A.: Digital networks in the automotive vehicle. Comput. Control Eng. J. 10(6), 257\u2013266 (1999)","journal-title":"Comput. Control Eng. J."},{"issue":"3","key":"4_CR28","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/s11704-018-7039-7","volume":"13","author":"J Liu","year":"2018","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 (2018). https:\/\/doi.org\/10.1007\/s11704-018-7039-7","journal-title":"Front. Comput. Sci."},{"issue":"1","key":"4_CR29","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)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2012.05.040","volume":"451","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proceedings of the Internetware 2013. ACM, NY (2013)","DOI":"10.1145\/2532443.2532473"},{"issue":"1","key":"4_CR32","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)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"4_CR33","unstructured":"SAE International: Architecture analysis and design language (AADL) annex volume 2: Annex B: Data modeling annex (2011)"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Steiner, W., Bauer, G., Hall, B., Paulitsch, M., Varadarajan, S.: TTEthernet dataflow concept. In: 2009 Eighth IEEE International Symposium on Network Computing and Applications, pp. 319\u2013322. IEEE (2009)","DOI":"10.1109\/NCA.2009.28"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Steiner, W., Rushby, J.: TTA and PALS: formally verified design patterns for distributed cyber-physical systems. In: 2011 IEEE\/AIAA 30th Digital Avionics Systems Conference, pp. 7B5\u20131. IEEE (2011)","DOI":"10.1109\/DASC.2011.6096120"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-15545-6_18","volume-title":"Software, Services, and Systems","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. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 273\u2013290. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15545-6_18"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19759-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T19:18:43Z","timestamp":1666207123000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19759-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197581","9783031197598"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19759-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","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":"Rhodes","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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}