{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T16:20:37Z","timestamp":1787502037531,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsc {Hybrid}\\textsc {Synch}\\textsc {AADL}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>H<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>B<\/mml:mi>\n                              <mml:mi>R<\/mml:mi>\n                              <mml:mi>I<\/mml:mi>\n                              <mml:mi>D<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>S<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>N<\/mml:mi>\n                              <mml:mi>C<\/mml:mi>\n                              <mml:mi>H<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>AADL<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs. We define the\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsc {Hybrid}\\textsc {Synch}\\textsc {AADL}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>H<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>B<\/mml:mi>\n                              <mml:mi>R<\/mml:mi>\n                              <mml:mi>I<\/mml:mi>\n                              <mml:mi>D<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>S<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>N<\/mml:mi>\n                              <mml:mi>C<\/mml:mi>\n                              <mml:mi>H<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>AADL<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsc {Hybrid}\\textsc {Synch}\\textsc {AADL}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:mi>H<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>B<\/mml:mi>\n                              <mml:mi>R<\/mml:mi>\n                              <mml:mi>I<\/mml:mi>\n                              <mml:mi>D<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>S<\/mml:mi>\n                            <mml:mstyle>\n                              <mml:mi>Y<\/mml:mi>\n                              <mml:mi>N<\/mml:mi>\n                              <mml:mi>C<\/mml:mi>\n                              <mml:mi>H<\/mml:mi>\n                            <\/mml:mstyle>\n                            <mml:mi>AADL<\/mml:mi>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    on a number of applications.\n                  <\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_23","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T20:02:35Z","timestamp":1626465755000},"page":"491-504","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Hybrid SynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL"],"prefix":"10.1007","author":[{"given":"Jaehun","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sharon","family":"Kim","sequence":"additional","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":[[2021,7,15]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027227","volume-title":"Formal Methods for Industrial Applications","year":"1996","unstructured":"Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications. LNCS, vol. 1165. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0027227"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-15317-9_15","volume-title":"Formal Aspects of Component Software","author":"E Ahmad","year":"2015","unstructured":"Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with Hybrid Annex. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 228\u2013247. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15317-9_15"},{"key":"23_CR3","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 ACM SIGAda HILT 2014. ACM (2014)","DOI":"10.1145\/2663171.2663178"},{"key":"23_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: Proceedings of RTSS. IEEE (2009)","DOI":"10.1109\/RTSS.2009.50"},{"key":"23_CR5","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: Proceedings of HCMDSS-MDPnP 2007. IEEE (2007)","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Bae, K., Gao, S.: Modular SMT-based analysis of nonlinear hybrid systems. In: Proceedings of FMCAD, pp. 180\u2013187. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102258"},{"key":"23_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":"23_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 HSCC. ACM (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"23_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":"23_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":"23_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."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: A source transformation and translation tool for hybrid automaton models. In: Proceedings of HSCC 2015. ACM (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: Hylaa: A tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of HSCC 2017. ACM (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"23_CR14","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., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: 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":"23_CR15","doi-asserted-by":"crossref","unstructured":"Baudart, G., Bourke, T., Pouzet, M.: Soundness of the quasi-synchronous abstraction. In: Proceedings of FMCAD, pp. 9\u201316. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886655"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/3-540-45416-0_21","volume-title":"Computer Safety, Reliability and Security","author":"P Caspi","year":"2001","unstructured":"Caspi, P., Mazuet, C., Paligot, N.R.: About the design of distributed control systems: The quasi-synchronous approach. In: Voges, U. (ed.) SAFECOMP 2001. LNCS, vol. 2187, pp. 215\u2013226. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45416-0_21"},{"key":"23_CR17","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":"23_CR18","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":"23_CR19","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., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: 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":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-319-21668-3_25","volume-title":"Computer Aided Verification","author":"A Desai","year":"2015","unstructured":"Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: An abstraction for distributed almost-synchronous systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 429\u2013448. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_25"},{"key":"23_CR21","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":"23_CR22","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley (2012)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Fran\u00e7a, R., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex - experiments and roadmap. In: ICECCS. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"23_CR24","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., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: 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":"23_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"23_CR26","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Proceedings of FMCAD. IEEE (2013)"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-45828-X_20","volume-title":"Embedded Software","author":"A Girault","year":"2002","unstructured":"Girault, A., M\u00e9nier, C.: Automatic production of globally asynchronous locally synchronous systems. In: Sangiovanni-Vincentelli, A., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 266\u2013281. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45828-X_20"},{"key":"23_CR28","unstructured":"Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Proceedings of ACSD 2006. IEEE (2006)"},{"key":"23_CR29","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"T Henzinger","year":"2000","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"23_CR30","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 ICCPS 2010. ACM (2010)","DOI":"10.1145\/1795194.1795215"},{"key":"23_CR31","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"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Larrieu, R., Shankar, N.: A framework for high-assurance quasi-synchronous systems. In: Proceedings of MEMOCODE 2014. IEEE (2014)","DOI":"10.1109\/MEMCOD.2014.6961845"},{"key":"23_CR33","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. manuscript, January 2021. https:\/\/hybridsynchaadl.github.io\/\/docs\/techrep.pdf","DOI":"10.1007\/978-3-030-81685-8_23"},{"issue":"6","key":"23_CR34","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":"23_CR35","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."},{"key":"23_CR36","doi-asserted-by":"crossref","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 5\u201327 (2012)","DOI":"10.1016\/j.tcs.2012.05.040"},{"key":"23_CR37","unstructured":"Potop-Butucaru, D., Caillaud, B.: Correct-by-construction asynchronous implementation of modular synchronous specifications. Fundam. Inform. 78(1), 131\u2013159 (2007)"},{"key":"23_CR38","doi-asserted-by":"crossref","unstructured":"Qian, Y., Liu, J., Chen, X.: Hybrid AADL: A sublanguage extension to AADL. In: Proceedings of MEMOCODE 2014. ACM (2013)","DOI":"10.1145\/2532443.2532473"},{"key":"23_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-015-5","volume-title":"Distributed Consensus in Multi-vehicle Cooperative Control","author":"W Ren","year":"2008","unstructured":"Ren, W., Beard, R.W.: Distributed Consensus in Multi-vehicle Cooperative Control. Springer, London (2008). https:\/\/doi.org\/10.1007\/978-1-84800-015-5"},{"key":"23_CR40","doi-asserted-by":"crossref","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)","DOI":"10.1016\/j.jlamp.2016.10.001"},{"issue":"5","key":"23_CR41","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. Software Eng. 25(5), 651\u2013660 (1999)","journal-title":"IEEE Trans. Software Eng."},{"key":"23_CR42","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"},{"issue":"10","key":"23_CR43","doi-asserted-by":"publisher","first-page":"1300","DOI":"10.1109\/TC.2008.81","volume":"57","author":"S Tripakis","year":"2008","unstructured":"Tripakis, S., Pinello, C., Benveniste, A., Sangiovanni-Vincent, A., Caspi, P., Di Natale, M.: Implementing synchronous models on loosely time triggered architectures. IEEE Trans. Comput. 57(10), 1300\u20131314 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"23_CR44","unstructured":"Yu, G., Bae, K.: Maude-SE: A tight integration of Maude and SMT solvers. In: Proceedings of International Workshop on Rewriting Logic and Its Applications (2020)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T13:42:47Z","timestamp":1672839767000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}