{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:29:43Z","timestamp":1759879783093,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031197581"},{"type":"electronic","value":"9783031197598"}],"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_2","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T09:07:32Z","timestamp":1666170452000},"page":"13-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Correct by\u00a0Design Coordination of\u00a0Autonomous Driving Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4412-5684","authenticated-orcid":false,"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2447-7981","authenticated-orcid":false,"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"2_CR1","unstructured":"ASAM OpenDRIVE\u00ae - open dynamic road information for vehicle environment. Technical report V 1.6.0, ASAM e.V., March 2020. https:\/\/www.asam.net\/standards\/detail\/opendrive"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bagschik, G., Menzel, T., Maurer, M.: Ontology based scene creation for the development of automated vehicles. In: Intelligent Vehicles Symposium, pp. 1813\u20131820. IEEE (2018)","DOI":"10.1109\/IVS.2018.8500632"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-319-91638-5_13","volume-title":"Advanced Computing Strategies for Engineering","author":"J Beetz","year":"2018","unstructured":"Beetz, J., Borrmann, A.: Benefits and limitations of linked data approaches for road modeling and data exchange. In: Smith, I., Domer, B. (eds.) EG-ICE. LNCS, vol. 10864, pp. 245\u2013261. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91638-5_13"},{"issue":"2\u20133","key":"2_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"2_CR5","unstructured":"Bozga, M., Sifakis, J.: Specification and validation of autonomous driving systems: a multilevel semantic framework. CoRR abs\/2109.06478 (2021). https:\/\/arxiv.org\/abs\/2109.06478"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Bozga, M., Sifakis, J.: Correct by design coordination of autonomous driving systems. CoRR abs\/2205.10037 (2022). https:\/\/doi.org\/10.48550\/arXiv.2205.10037","DOI":"10.1007\/978-3-031-19759-8_2"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Butz, M., et al.: SOCA: domain analysis for highly automated driving systems. In: ITSC, pp. 1\u20136. IEEE (2020)","DOI":"10.1109\/ITSC45102.2020.9294438"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-71209-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261\u2013275. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-030-58768-0_16","volume-title":"Software Engineering and Formal Methods","author":"A El-Hokayem","year":"2020","unstructured":"El-Hokayem, A., Bensalem, S., Bozga, M., Sifakis, J.: A layered implementation of DR-BIP supporting run-time monitoring and analysis. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 284\u2013302. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_16"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Esterle, K., Gressenbuch, L., Knoll, A.C.: Formalizing traffic rules for machine interpretability. In: CAVS, pp. 1\u20137. IEEE (2020)","DOI":"10.1109\/CAVS51000.2020.9334599"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"Formal Methods and Software Engineering","author":"M Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic Manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404\u2013419. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24559-6_28"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Karimi, A., Duggirala, P.S.: Formalizing traffic rules for uncontrolled intersections. In: ICCPS, pp. 41\u201350. IEEE (2020)","DOI":"10.1109\/ICCPS48487.2020.00012"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Pappas, G.J.: Automatically synthesizing a planning and control subsystem for the DARPA urban challenge. In: CASE, pp. 766\u2013771. IEEE (2008)","DOI":"10.1109\/COASE.2008.4626549"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"Formal Methods","author":"A Mavridou","year":"2021","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 503\u2013523. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27"},{"issue":"10","key":"2_CR15","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u2019\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Poggenhans, F., et al.: Lanelet2: a high-definition map framework for the future of automated driving. In: ITSC, pp. 1672\u20131679. IEEE (2018)","DOI":"10.1109\/ITSC.2018.8569929"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: ITSC, pp. 1658\u20131665. IEEE (2015)","DOI":"10.1109\/ITSC.2015.269"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-01090-4_5","volume-title":"Automated Technology for Verification and Analysis","author":"A Rizaldi","year":"2018","unstructured":"Rizaldi, A., Immler, F., Sch\u00fcrmann, B., Althoff, M.: A formally verified motion planner for autonomous vehicles. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 75\u201390. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_5"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-66845-1_4","volume-title":"Integrated Formal Methods","author":"A Rizaldi","year":"2017","unstructured":"Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E., Nipkow, T.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 50\u201366. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_4"},{"key":"2_CR20","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2021.109910","volume":"134","author":"A Saoud","year":"2021","unstructured":"Saoud, A., Girard, A., Fribourg, L.: Assume-guarantee contracts for continuous-time systems. Automatica 134, 109910 (2021)","journal-title":"Automatica"},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1146\/annurev-control-060117-105157","volume":"1","author":"W Schwarting","year":"2018","unstructured":"Schwarting, W., Alonso-Mora, J., Rus, D.: Planning and decision-making for autonomous vehicles. Annu. Rev. Control Robot. Auton. Syst. 1, 187\u2013210 (2018). https:\/\/doi.org\/10.1146\/annurev-control-060117-105157","journal-title":"Annu. Rev. Control Robot. Auton. Syst."},{"key":"2_CR22","unstructured":"Sharf, M., Besselink, B., Molin, A., Zhao, Q., Johansson, K.H.: Assume\/guarantee contracts for dynamical systems: theory and computational tools. CoRR abs\/2012.12657 (2020)"},{"key":"2_CR23","unstructured":"Sun, M., Bakirtzis, G., Jafarzadeh, H., Fleming, C.: Correct-by-construction: a contract-based semi-automated requirement decomposition process. CoRR abs\/1909.02070 (2019)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Wang, Q., Li, D., Sifakis, J.: Safe and efficient collision avoidance control for autonomous vehicles. In: MEMOCODE, pp. 1\u20136. IEEE (2020)","DOI":"10.1109\/MEMOCODE51338.2020.9315034"},{"key":"2_CR25","unstructured":"Wang, Q., Zheng, X., Zhang, J., Sifakis, J.: A hybrid controller for safe and efficient collision avoidance control. CoRR abs\/2103.15484 (2021). https:\/\/arxiv.org\/abs\/2103.15484"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Waqas, M., Murtaza, M.A., Nuzzo, P., Ioannou, P.: Correct-by-construction design of adaptive cruise control with control barrier functions under safety and regulatory constraints (2022). https:\/\/arxiv.org\/abs\/2203.14110","DOI":"10.23919\/ACC53348.2022.9867464"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Karaman, S., Frazzoli, E.: Synthesis of provably correct controllers for autonomous vehicles in urban environments. In: ITSC, pp. 1168\u20131173. IEEE (2011)","DOI":"10.1109\/ITSC.2011.6083056"},{"issue":"11","key":"2_CR28","doi-asserted-by":"publisher","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","volume":"57","author":"T Wongpiromsarn","year":"2012","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning. IEEE Trans. Autom. Control 57(11), 2817\u20132830 (2012)","journal-title":"IEEE Trans. Autom. Control"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T23:17:35Z","timestamp":1666221455000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19759-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197581","9783031197598"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19759-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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"}}]}}