{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:44Z","timestamp":1776333524393,"version":"3.51.2"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automated driving functions are among the most critical software components to develop. Before deployment in series vehicles, it has to be shown that the functions drive safely and in compliance with traffic rules. Despite the coverage that can be reached with very large amounts of test drives, corner cases remain possible. Furthermore, the development is subject to time-to-delivery constraints due to the highly competitive market, and potential logical errors must be found as early as possible. We describe an approach to improve the development of an actual industrial behavior planner for the <jats:italic>Automated Driving Alliance<\/jats:italic> between Bosch and Cariad. The original process landscape for verification and validation is extended with model checking techniques. The idea is to integrate automated extraction mechanisms that, starting from the C<jats:bold>++<\/jats:bold> code of the planner, generate a higher-level model of the underlying logic. This model, composed in closed loop with expressive environment descriptions, can be exhaustively analyzed with model checking. This results, in case of violations, in traces that can be re-executed in system simulators to guide the search for errors. The approach was exemplarily deployed in series development, and successfully found relevant issues in intermediate versions of the planner at development time.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_3","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"44-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7840-1459","authenticated-orcid":false,"given":"Lukas","family":"K\u00f6nig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2144-6215","authenticated-orcid":false,"given":"Christian","family":"Heinzemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3311-0893","authenticated-orcid":false,"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6353-227X","authenticated-orcid":false,"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1398-9287","authenticated-orcid":false,"given":"Franziska","family":"Henze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9200-3224","authenticated-orcid":false,"given":"Stefan","family":"K\u00fcperkoch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5256-2478","authenticated-orcid":false,"given":"Dennis","family":"Fassbender","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-6471-4049","authenticated-orcid":false,"given":"Michael","family":"Hanselmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"3_CR1","unstructured":"Amid, G.: ASAM OpenSCENARIO V2.0.0. Tech. rep., Association for Standardization of Automation and Measuring Systems (2022)"},{"key":"3_CR2","unstructured":"Aptiv, Audi, Baid, BMW, Continental, Daimler, Fca, Here, Infineon, Intel, Volswagen: Safety first for automated driving. Tech. rep. (2019), https:\/\/www.aptiv.com\/docs\/default-source\/white-papers\/safety-first-for-automated-driving-aptiv-white-paper.pdf, accessed: 25.09.2023"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Artu\u00f1edo, A., Godoy, J., Villagra, J.: A decision-making architecture for automated driving without detailed prior maps. In: 2019 IEEE Intelligent Vehicles Symposium (IV). pp. 1645\u20131652. Paris, France (2019)","DOI":"10.1109\/IVS.2019.8814070"},{"key":"3_CR4","unstructured":"Audi AG, Audi Kommunikation: Audi SocAlty Study (2022), https:\/\/www.audi.com\/content\/dam\/gbp2\/company\/research\/audi-beyond\/2021\/AUDI_SocAITy_Study_dgtl_1201_English_small.pdf, accessed: 25.09.2023"},{"key":"3_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA (2008)"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems. pp. 125\u2013126. QEST 2006, IEEE Computer Society, Los Alamitos, CA, USA (Sep 2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Brooks, R.A.: A robust layered control system for a mobile robot. IEEE Journal on Robotics and Automation 2(1), 14\u201323 (1986)","DOI":"10.1109\/JRA.1986.1087032"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv Symbolic Model Checker. In: Computer Aided Verification. CAV 2014 (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cherukuri, H., Ferrari, A., Spoletini, P.: Towards Explainable Formal Methods: From LTL to Natural Language with Neural Machine Translation. In: Gervasi, V., Vogelsang, A. (eds.) Requirements Engineering: Foundation for Software Quality. pp. 79\u201386. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-98464-9_7"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Mover, S., Roveri, M., Tonetta, S.: Verification modulo theories. Formal Methods in System Design (2023). https:\/\/doi.org\/10.1007\/s10703-023-00434-x","DOI":"10.1007\/s10703-023-00434-x"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods in System Design 49(3), 190\u2013218 (2016)","DOI":"10.1007\/s10703-016-0257-4"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol.\u00a02988, pp. 168\u2013176. Springer, Berlin, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. CAV 2016. Lecture Notes in Computer Science, vol.\u00a09779, pp. 271\u2013291. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Daw, Z., Cleaveland, R., Vetter, M.: Integrating model checking and uml based model-driven development for embedded systems. In: Automated Verification of Critical Systems 2013. Electronic Communications of the EASST, vol.\u00a066 (2013). https:\/\/doi.org\/10.14279\/tuj.eceasst.66.888","DOI":"10.14279\/tuj.eceasst.66.888"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: A modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification. pp. 592\u2013600. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Eberhart, C., Dubut, J., Haydon, J., Hasuo, I.: Formal verification of safety architectures for automated driving. In: 2023 IEEE Intelligent Vehicles Symposium (IV). pp.\u00a01\u20138 (2023). https:\/\/doi.org\/10.1109\/IV55152.2023.10186763","DOI":"10.1109\/IV55152.2023.10186763"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: \u201cA Mathematical Introduction to Logic\u201d. Academic Press, Boston, MA, USA, 2. edn. (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Farrell, M., Bradbury, M., Fisher, M., Dennis, L.A., Dixon, C., Yuan, H., Maple, C.: Using threat analysis techniques to guide formal verification: A case study of cooperative awareness messages. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) Software Engineering and Formal Methods. pp. 471\u2013490. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-30446-1_25"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Fuchs, S., Rass, S., Lamprecht, B., Kyamakya, K.: A Model for Ontology-Based Scene Description for Context-Aware Driver Assistance Systems. In: 1st International ICST Conference on Ambient Media and Systems. Phoenix, AZ, USA (2010). https:\/\/doi.org\/10.4108\/ICST.AMBISYS2008.2869","DOI":"10.4108\/ICST.AMBISYS2008.2869"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Gardner, R.W., Genin, D., McDowell, R., Rouff, C., Saksena, A., Schmidt, A.: Probabilistic model checking of the next-generation airborne collision avoidance system. In: 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC). pp. 1\u201310 (2016). https:\/\/doi.org\/10.1109\/DASC.2016.7777963","DOI":"10.1109\/DASC.2016.7777963"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Geisslinger, M., Poszler, F., Betz, J., L\u00fctge, C., Lienkamp, M.: Autonomous Driving Ethics: from Trolley Problem to Ethics of Risk. Philosophy & Technology 34(4), 1033\u20131055 (2021)","DOI":"10.1007\/s13347-021-00449-4"},{"key":"3_CR22","unstructured":"Gerking, C., Dziwok, S., Heinzemann, C., Sch\u00e4fer, W.: Domain-specific model checking for cyber-physical systems. In: 12th Workshop on Model-Driven Engineering, Verification and Validation. pp. 18\u201327. MoDeVVa 2015, CEUR-WS.org Vol-1514, Ottawa (Sep 2015)"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Griggio, A., Jon\u00e1\u0161, M.: Kratos2: an SMT-Based Model Checker for Imperative Programs. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 423\u2013436. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Griggio, A., Roveri, M.: Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits Systems 35(6), 1026\u20131039 (2016). https:\/\/doi.org\/10.1109\/TCAD.2015.2481869","DOI":"10.1109\/TCAD.2015.2481869"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Halder, P., Althoff, M.: Minimum-Violation Velocity Planning with Temporal Logic Constraints. In: 2022 IEEE 25th International Conference on Intelligent Transportation Systems (ITSC). p. 2520\u20132527. IEEE Press, Macau, China (2022). https:\/\/doi.org\/10.1109\/ITSC55140.2022.9922114","DOI":"10.1109\/ITSC55140.2022.9922114"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Heinzemann, C., Lange, R.: vTSL \u2013 a formally verifiable dsl for specifying robot tasks. In: 2018 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 8308\u20138314. IROS\u201918, IEEE Computer Society, Madrid, Spain (2018). https:\/\/doi.org\/10.1109\/IROS.2018.8593559","DOI":"10.1109\/IROS.2018.8593559"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J.: The model checker spin. Software Engineering, IEEE Transactions on 23(5), 279 \u2013295 (may 1997). https:\/\/doi.org\/10.1109\/32.588521","DOI":"10.1109\/32.588521"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., H.\u00a0Smith, M.: Software model checking: extracting verification models from source code$$\\dagger $$. Software Testing, Verification and Reliability 11(2), 65\u201379 (2001). https:\/\/doi.org\/10.1002\/stvr.228","DOI":"10.1002\/stvr.228"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Ishigooka, T., Saissi, H., Piper, T., Winter, S., Suri, N.: Practical use of formal verification for safety critical cyber-physical systems: A case study. In: 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and Applications. pp. 7\u201312 (2014). https:\/\/doi.org\/10.1109\/CPSNA.2014.20","DOI":"10.1109\/CPSNA.2014.20"},{"key":"3_CR30","unstructured":"ISO\/TC 22\/SC 32 Electrical and electronic components and general system aspects: ISO 21448:2022 Road vehicles \u2013 Safety of the intended functionality (2022), https:\/\/www.iso.org\/standard\/77490.html, accessed: 25.09.2023"},{"key":"3_CR31","unstructured":"Kaleeswaran, A.P., Nordmann, A., Vogel, T., Grunske, L.: A user-study protocol for evaluation of formal verification results and their explanation. arXiv abs\/2108.06376 (2021)"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Kaleeswaran, A.P., Nordmann, A., Vogel, T., Grunske, L.: A systematic literature review on counterexample explanation. Information and Software Technology 145, 1\u201320 (2022). https:\/\/doi.org\/10.1016\/j.infsof.2021.106800","DOI":"10.1016\/j.infsof.2021.106800"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Kaleeswaran, A.P., Nordmann, A., Vogel, T., Grunske, L.: A user study for evaluation of formal verification results and their explanation at bosch. Empirical Software Engineering 28(5) (2023)","DOI":"10.1007\/s10664-023-10353-4"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Kalra, N., Paddock, S.M.: Driving to safety: How many miles of driving would it take to demonstrate autonomous vehicle reliability? Transportation Research Part A: Policy and Practice 94, 182\u2013193 (2016)","DOI":"10.1016\/j.tra.2016.09.010"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Keating, D., McInnes, A., Hayes, M.: An industrial application of model checking to a vessel control system. In: 2011 Sixth IEEE International Symposium on Electronic Design, Test and Application. pp. 83\u201388 (2011). https:\/\/doi.org\/10.1109\/DELTA.2011.24","DOI":"10.1109\/DELTA.2011.24"},{"key":"3_CR36","doi-asserted-by":"publisher","unstructured":"Keller, C.W., Saha, D., Basu, S., Smolka, S.A.: FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 563\u2013569. Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_39","DOI":"10.1007\/978-3-540-31980-1_39"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Kerner, B.S.: Physics of automated driving in framework of three-phase traffic theory. Physical Review E 97(4) (2018). https:\/\/doi.org\/10.1103\/PhysRevE.97.042303","DOI":"10.1103\/PhysRevE.97.042303"},{"key":"3_CR38","doi-asserted-by":"publisher","unstructured":"Kortenkamp, D., Simmons, R.: Robotic Systems Architectures and Programming. In: Siciliano, B., Khatib, O. (eds.) Springer Handbook of Robotics. pp. 187\u2013206. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-30301-5_9","DOI":"10.1007\/978-3-540-30301-5_9"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Krasowski, H., Zhang, Y., Althoff, M.: Safe Reinforcement Learning for Urban Driving using Invariably Safe Braking Sets. In: 2022 IEEE 25th International Conference on Intelligent Transportation Systems (ITSC). pp. 2407\u20132414. Macau, China (2022)","DOI":"10.1109\/ITSC55140.2022.9922166"},{"key":"3_CR40","doi-asserted-by":"publisher","unstructured":"Kriebitz, A., Max, R., L\u00fctge, C.: The German Act on Autonomous Driving: Why Ethics Still Matters. Philosophy & Technology 35(2), \u00a029 (2022). https:\/\/doi.org\/10.1007\/s13347-022-00526-2","DOI":"10.1007\/s13347-022-00526-2"},{"key":"3_CR41","doi-asserted-by":"publisher","unstructured":"Kr\u00e4mer, S., Stiller, C., Bouzouraa, M.E.: LiDAR-Based Object Tracking and Shape Estimation Using Polylines and Free-Space Information. In: 2018 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 4515\u20134522. Madrid, Spanien (2018). https:\/\/doi.org\/10.1109\/IROS.2018.8593385","DOI":"10.1109\/IROS.2018.8593385"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911). LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Leino, K., M., R.: Program Proving Using Intermediate Verification Languages (IVLs) like Boogie and Why3. In: Proceedings of the 2012 ACM Conference on High Integrity Language Technology. pp. 25\u201326. Association for Computing Machinery (2012). https:\/\/doi.org\/10.1145\/2402676.2402689","DOI":"10.1145\/2402676.2402689"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Majzik, I., Semer\u00e1th, O., Hajdu, C., Marussy, K., Szatm\u00e1ri, Z., Micskei, Z., V\u00f6r\u00f6s, A., Babikian, A.A., Varr\u00f3, D.: Towards System-Level Testing with Coverage Guarantees for Autonomous Vehicles. In: Kessentini, M., Yue, T., Pretschner, A., Voss, S., Burgue\u00f1o, L. (eds.) 22nd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2019. pp. 89\u201394. IEEE, Munich, Germany (2019). https:\/\/doi.org\/10.1109\/MODELS.2019.00-12","DOI":"10.1109\/MODELS.2019.00-12"},{"key":"3_CR45","doi-asserted-by":"publisher","unstructured":"Mehdipour, N., Althoff, M., Tebbens, R.D., Belta, C.: Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges. Automatica 152 (2023). https:\/\/doi.org\/10.1016\/j.automatica.2022.110692","DOI":"10.1016\/j.automatica.2022.110692"},{"key":"3_CR46","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. The International Journal of Robotics Research 36(12), 1312\u20131340 (2017). https:\/\/doi.org\/10.1177\/0278364917733549","DOI":"10.1177\/0278364917733549"},{"key":"3_CR47","doi-asserted-by":"publisher","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods in System Design 49, 33\u201374 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0241-z","DOI":"10.1007\/s10703-016-0241-z"},{"key":"3_CR48","unstructured":"Nawaz, M.S., Malik, M., Li, Y., Sun, M., Lali, M.I.U.: A survey on theorem provers in formal methods (2019)"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Nees, M.A.: Safer than the average human driver (who is less safe than me)? examining a popular safety benchmark for self-driving cars. Journal of Safety Research 69, 61\u201368 (2019)","DOI":"10.1016\/j.jsr.2019.02.002"},{"key":"3_CR50","doi-asserted-by":"publisher","unstructured":"Redfield, S.A., Seto, M.L.: Verification challenges for autonomous systems. In: Lawless, W., Mittu, R., Sofge, D., Russell, S. (eds.) Autonomy and Artificial Intelligence: A Threat or Savior?, pp. 103\u2013127. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59719-5_5","DOI":"10.1007\/978-3-319-59719-5_5"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Reid, T., Houts, S., Cammarata, R., Mills, G., Agarwal, S., Vora, A., Pandey, G.: Localization requirements for autonomous vehicles. SAE International Journal of Computer Aided Verification 2(3), 173\u2013190 (2019). https:\/\/doi.org\/10.4271\/12-02-03-0012","DOI":"10.4271\/12-02-03-0012"},{"key":"3_CR52","doi-asserted-by":"publisher","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.) Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, pp. 50\u201366. No. 10510 in Lecture Notes in Computer Science, Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_4","DOI":"10.1007\/978-3-319-66845-1_4"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: A flexible framework for creating software model checkers. In: Proceedings of Testing: Academic and Industrial Conference - Practice And Research Techniques. pp. 3 \u201322. TAIC PART 2006 (aug 2006). https:\/\/doi.org\/10.1109\/taic-part.2006.5","DOI":"10.1109\/taic-part.2006.5"},{"key":"3_CR54","doi-asserted-by":"publisher","unstructured":"Ro\u010dkai, P., Barnat, J., Brim, L.: Model checking C++ programs with exceptions. Science of Computer Programming 128, 68\u201385 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.05.007","DOI":"10.1016\/j.scico.2016.05.007"},{"key":"3_CR55","doi-asserted-by":"publisher","unstructured":"Schlich, B., Kowalewski, S.: Model checking c source code for embedded systems. International Journal on Software Tools for Technology Transfer 11(3), 187\u2013202 (2009). https:\/\/doi.org\/10.1007\/s10009-009-0106-5","DOI":"10.1007\/s10009-009-0106-5"},{"key":"3_CR56","doi-asserted-by":"publisher","unstructured":"Schmidt, \u00c1., Varr\u00f3, D.: Checkvml: A tool for model checking visual modeling languages. In: Stevens, P., Whittle, J., Booch, G. (eds.) UML 2003 - The Unified Modeling Language. Modeling Languages and Applications, Lecture Notes in Computer Science, vol.\u00a02863, pp. 92\u201395. Springer Berlin Heidelberg (Oct 2003). https:\/\/doi.org\/10.1007\/978-3-540-45221-8_8","DOI":"10.1007\/978-3-540-45221-8_8"},{"key":"3_CR57","doi-asserted-by":"publisher","unstructured":"Schmidt, L.M., Kontes, G., Plinge, A., Mutschler, C.: Can You Trust Your Autonomous Car? Interpretable and Verifiably Safe Reinforcement Learning. In: 2021 IEEE Intelligent Vehicles Symposium (IV). pp. 171\u2013178. Nagoya, Japan (2021). https:\/\/doi.org\/10.1109\/IV48863.2021.9575328","DOI":"10.1109\/IV48863.2021.9575328"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Schreurs, M., Steuwer, S.: Autonomous Driving - Political, Legal, Social, and Sustainability Dimensions. Autonomes Fahren: Technische, rechtliche und gesellschaftliche Aspekte pp. 151\u2013173 (2015)","DOI":"10.1007\/978-3-662-45854-9_8"},{"key":"3_CR59","doi-asserted-by":"crossref","unstructured":"Selvaraj, Y., Ahrendt, W., Fabian, M.: Verification of decision making software in an autonomous vehicle: An industrial case study. In: Larsen, K.G., Willemse, T. (eds.) Formal Methods for Industrial Critical Systems. pp. 143\u2013159. Springer International Publishing, Cham (2019)","DOI":"10.1007\/978-3-030-27008-7_9"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Shankar, S., Pajela, G.: A tool integrating model checking into a c verification toolset. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) Model Checking Software, Lecture Notes in Computer Science, vol.\u00a09641, pp. 214\u2013224. Springer International Publishing (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_15","DOI":"10.1007\/978-3-319-32582-8_15"},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Shariff, A., Bonnefon, J.F., Rahwan, I.: How safe is safe enough? Psychological mechanisms underlying extreme safety demands for self-driving cars. Transportation Research Part C: Emerging Technologies 126, 1\u201312 (2021). https:\/\/doi.org\/10.1016\/j.trc.2021.103069","DOI":"10.1016\/j.trc.2021.103069"},{"key":"3_CR62","doi-asserted-by":"publisher","unstructured":"Wachenfeld, W., Winner, H.: The Release of Autonomous Vehicles, pp. 425\u2013450. Springer, Berlin, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-48847-8_21","DOI":"10.1007\/978-3-662-48847-8_21"},{"key":"3_CR63","doi-asserted-by":"publisher","unstructured":"Zhao, T., Yurtsever, E., Paulson, J.A., Rizzoni, G.: Formal Certification Methods for Automated Vehicle Safety Assessment. IEEE Transactions on Intelligent Vehicles 8(1), 232\u2013249 (2022). https:\/\/doi.org\/10.1109\/TIV.2022.3170517","DOI":"10.1109\/TIV.2022.3170517"},{"key":"3_CR64","doi-asserted-by":"publisher","unstructured":"Zhao, T., Yurtsever, E., Paulson, J.A., Rizzoni, G.: Formal certification methods for automated vehicle safety assessment. IEEE Transactions on Intelligent Vehicles 8(1), 232\u2013249 (2023). https:\/\/doi.org\/10.1109\/TIV.2022.3170517","DOI":"10.1109\/TIV.2022.3170517"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57249-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T10:02:36Z","timestamp":1714730556000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","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":"159","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":"53","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":"16","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":"33% - 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":"10","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)"}}]}}