{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,6]],"date-time":"2024-05-06T05:54:33Z","timestamp":1714974873415},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s10009-023-00723-0","type":"journal-article","created":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T13:02:13Z","timestamp":1698930133000},"page":"625-639","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Correct by design coordination of autonomous driving systems"],"prefix":"10.1007","volume":"25","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,11,2]]},"reference":[{"key":"723_CR1","unstructured":"ASAM OpenDRIVE\u00ae open dynamic road information for vehicle environment. Tech. Rep. V 1.6.0, ASAM e.V, (2020) https:\/\/www.asam.net\/standards\/detail\/opendrive"},{"key":"723_CR2","first-page":"1813","volume-title":"Intelligent Vehicles Symposium","author":"G. Bagschik","year":"2018","unstructured":"Bagschik, G., Menzel, T., Maurer, M.: Ontology based scene creation for the development of automated vehicles. In: Intelligent Vehicles Symposium, pp.\u00a01813\u20131820. IEEE, Los Alamitos (2018)"},{"key":"723_CR3","first-page":"245","volume-title":"EG-ICE, Lecture Notes in Computer Science","author":"J. Beetz","year":"2018","unstructured":"Beetz, J., Borrmann, A.: Benefits and limitations of linked data approaches for road modeling and data exchange. In: EG-ICE, Lecture Notes in Computer Science, vol.\u00a010864, pp.\u00a0245\u2013261. Springer, Berlin (2018)"},{"issue":"2\u20133","key":"723_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A. Benveniste","year":"2018","unstructured":"Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J., Reinkemeier, P., Sangiovanni-Vincentelli, A.L., Damm, W., Henzinger, T.A., Larsen, K.G.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"723_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-3-031-19759-8_2","volume-title":"ISoLA (3)","author":"M. Bozga","year":"2022","unstructured":"Bozga, M., Sifakis, J.: Correct by design coordination of autonomous driving systems. In: ISoLA (3). Lecture Notes in Computer Science, vol.\u00a013703, pp.\u00a013\u201329. Springer, Berlin (2022)"},{"key":"723_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-031-22337-2_5","volume-title":"Principles of Systems Design","author":"M. Bozga","year":"2022","unstructured":"Bozga, M., Sifakis, J.: Specification and validation of autonomous driving systems: a multilevel semantic framework. In: Principles of Systems Design. Lecture Notes in Computer Science, vol.\u00a013660, pp.\u00a085\u2013106. Springer, Berlin (2022)"},{"key":"723_CR7","first-page":"1","volume-title":"ITSC","author":"M. Butz","year":"2020","unstructured":"Butz, M., Heinzemann, C., Herrmann, M., Oehlerking, J., Rittel, M., Schalm, N., Ziegenbein, D.: SOCA: domain analysis for highly automated driving systems. In: ITSC, pp.\u00a01\u20136. IEEE, Los Alamitos (2020)"},{"key":"723_CR8","first-page":"261","volume-title":"TACAS, Lecture Notes in Computer Science","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: TACAS, Lecture Notes in Computer Science, vol.\u00a04424, pp.\u00a0261\u2013275. Springer, Berlin (2007)"},{"key":"723_CR9","first-page":"284","volume-title":"SEFM, Lecture Notes in Computer Science","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: SEFM, Lecture Notes in Computer Science, vol.\u00a012310, pp.\u00a0284\u2013302. Springer, Berlin (2020)"},{"key":"723_CR10","first-page":"1","volume-title":"CAVS","author":"K. Esterle","year":"2020","unstructured":"Esterle, K., Gressenbuch, L., Knoll, A.C.: Formalizing traffic rules for machine interpretability. In: CAVS, pp.\u00a01\u20137. IEEE, Los Alamitos (2020)"},{"key":"723_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1007\/978-3-642-24559-6_28","volume-title":"ICFEM","author":"M. Hilscher","year":"2011","unstructured":"Hilscher, M., Linker, S., Olderog, E., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: ICFEM. Lecture Notes in Computer Science, vol.\u00a06991, pp.\u00a0404\u2013419. Springer, Berlin (2011)"},{"key":"723_CR12","first-page":"41","volume-title":"ICCPS","author":"A. Karimi","year":"2020","unstructured":"Karimi, A., Duggirala, P.S.: Formalizing traffic rules for uncontrolled intersections. In: ICCPS, pp.\u00a041\u201350. IEEE, Los Alamitos (2020)"},{"key":"723_CR13","first-page":"766","volume-title":"CASE","author":"H. Kress-Gazit","year":"2008","unstructured":"Kress-Gazit, H., Pappas, G.J.: Automatically synthesizing a planning and control subsystem for the DARPA urban challenge. In: CASE, pp.\u00a0766\u2013771. IEEE, Los Alamitos (2008)"},{"key":"723_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"FM","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: FM. Lecture Notes in Computer Science, vol.\u00a013047, pp.\u00a0503\u2013523. Springer, Berlin (2021)"},{"issue":"10","key":"723_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\u201d. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"723_CR16","first-page":"1672","volume-title":"ITSC","author":"F. Poggenhans","year":"2018","unstructured":"Poggenhans, F., Pauls, J., Janosovits, J., Orf, S., Naumann, M., Kuhnt, F., Mayr, M.: Lanelet2: a high-definition map framework for the future of automated driving. In: ITSC, pp.\u00a01672\u20131679. IEEE, Los Alamitos (2018)"},{"key":"723_CR17","first-page":"1658","volume-title":"ITSC","author":"A. Rizaldi","year":"2015","unstructured":"Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: ITSC, pp.\u00a01658\u20131665. IEEE, Los Alamitos (2015)"},{"key":"723_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-319-66845-1_4","volume-title":"IFM","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: IFM. Lecture Notes in Computer Science, vol.\u00a010510, pp.\u00a050\u201366. Springer, Berlin (2017)"},{"key":"723_CR19","first-page":"75","volume-title":"ATVA, Lecture Notes in Computer Science","author":"A. Rizaldi","year":"2018","unstructured":"Rizaldi, A., Immler, F., Sch\u00fcrmann, B., Althoff, M.: A formally verified motion planner for autonomous vehicles. In: ATVA, Lecture Notes in Computer Science, vol.\u00a011138, pp.\u00a075\u201390. Springer, Berlin (2018)"},{"key":"723_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. Automa 134, 109910 (2021)","journal-title":"Automa"},{"key":"723_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":"723_CR22","doi-asserted-by":"crossref","unstructured":"Sharf, M., Besselink, B., Molin, A., Zhao, Q., Johansson, K.H.: Assume\/guarantee contracts for dynamical systems: Theory and computational tools CoRR (2020). arXiv:2012.12657","DOI":"10.1016\/j.ifacol.2021.08.469"},{"key":"723_CR23","unstructured":"Sun, M., Bakirtzis, G., Jafarzadeh, H., Fleming, C.: Correct-by-construction: a contract-based semi-automated requirement decomposition process. CoRR (2019). arXiv:1909.02070"},{"key":"723_CR24","first-page":"1","volume-title":"MEMOCODE","author":"Q. Wang","year":"2020","unstructured":"Wang, Q., Li, D., Sifakis, J.: Safe and efficient collision avoidance control for autonomous vehicles. In: MEMOCODE, pp.\u00a01\u20136. IEEE, Los Alamitos (2020)"},{"key":"723_CR25","unstructured":"Wang, Q., Zheng, X., Zhang, J., Sifakis, J.: A hybrid controller for safe and efficient collision avoidance control CoRR (2021). https:\/\/arxiv.org\/abs\/2103.15484. arXiv:2103.15484"},{"key":"723_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":"723_CR27","first-page":"1168","volume-title":"ITSC","author":"T. Wongpiromsarn","year":"2011","unstructured":"Wongpiromsarn, T., Karaman, S., Frazzoli, E.: Synthesis of provably correct controllers for autonomous vehicles in urban environments. In: ITSC, pp.\u00a01168\u20131173. IEEE, Los Alamitos (2011)"},{"issue":"11","key":"723_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":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00723-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-023-00723-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-023-00723-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T13:09:36Z","timestamp":1701090576000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-023-00723-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,2]]},"references-count":28,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["723"],"URL":"https:\/\/doi.org\/10.1007\/s10009-023-00723-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,11,2]]},"assertion":[{"value":"10 October 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}