{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T18:30:39Z","timestamp":1768415439610,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["DUT20TD107"],"award-info":[{"award-number":["DUT20TD107"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Self-driving cars over the last decade have achieved significant progress like driving millions of miles without any human intervention. However, behavioral safety in applying deep-neural-network-based (DNN based) systems for self-driving cars could not be guaranteed. Several real-world accidents involving self-driving cars have already happened, some of which have led to fatal collisions. In this paper, we present a novel and automated technique for verifying steering angle safety for self-driving cars. The technique is based on deep learning verification (DLV), which is an automated verification framework for safety of image classification neural networks. We extend DLV by leveraging neuron coverage and slack relationship to solve the judgement problem of predicted behaviors, and thus, to achieve verification of steering angle safety for self-driving cars. We evaluate our technique on the NVIDIA\u2019s end-to-end self-driving architecture, which is a crucial ingredient in many modern self-driving cars. Experimental results show that our technique can successfully find adversarial misclassifications (i.e., incorrect steering decisions) within given regions if they exist. Therefore, we can achieve safety verification (if no misclassification is found for all DNN layers, in which case the network can be said to be stable or reliable w.r.t. steering decisions) or falsification (in which case the adversarial examples can be used to fine-tune the network).<\/jats:p>","DOI":"10.1007\/s00165-021-00539-2","type":"journal-article","created":{"date-parts":[[2021,3,4]],"date-time":"2021-03-04T13:07:12Z","timestamp":1614863232000},"page":"325-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["SDLV: Verification of Steering Angle Safety for Self-Driving Cars"],"prefix":"10.1145","volume":"33","author":[{"given":"Huihui","family":"Wu","sequence":"first","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"},{"name":"Key Laboratory for Ubiquitous Network and Service Software of Liaoning Province, Dalian, China"}]},{"given":"Deyun","family":"Lv","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"},{"name":"Key Laboratory for Ubiquitous Network and Service Software of Liaoning Province, Dalian, China"}]},{"given":"Tengxiang","family":"Cui","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"},{"name":"Key Laboratory for Ubiquitous Network and Service Software of Liaoning Province, Dalian, China"}]},{"given":"Gang","family":"Hou","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"},{"name":"Key Laboratory for Ubiquitous Network and Service Software of Liaoning Province, Dalian, China"}]},{"given":"Masahiko","family":"Watanabe","sequence":"additional","affiliation":[{"name":"NTT DATA Automobiligence Research Center, Yokohama, Japan"}]},{"given":"Weiqiang","family":"Kong","sequence":"additional","affiliation":[{"name":"School of Software Technology, Dalian University of Technology, Dalian, China"},{"name":"Key Laboratory for Ubiquitous Network and Service Software of Liaoning Province, Dalian, China"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2014.2312453"},{"key":"e_1_2_1_2_2_2","unstructured":"Bastani O Ioannou Y Lampropoulos L Vytiniotis D Nori AV Criminisi A (2016) Measuring neural net robustness with constraints. In: Advances in neural information processing systems 29: annual conference on neural information processing systems 2016 December 5\u201310 2016 Barcelona Spain pp 2613\u20132621"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bengio Y Lamblin P Popovici D Larochelle H (2006) Greedy layer-wise training of deep networks. In: Advances in neural information processing systems 19 proceedings of the twentieth annual conference on neural information processing systems Vancouver British Columbia Canada December 4\u20137 2006 pp 153\u2013160","DOI":"10.7551\/mitpress\/7503.003.0024"},{"key":"e_1_2_1_2_4_2","unstructured":"Bojarski M Del Testa D Dworakowski D Firner B Flepp B Goyal P Jackel LD Monfort M Muller U Zhang J Zhang X Zhao J Zieba K (2016) End to end learning for self-driving cars. CoRR arXiv:1604.07316"},{"key":"e_1_2_1_2_5_2","unstructured":"Chauffeur model (2016)"},{"key":"e_1_2_1_2_6_2","unstructured":"The numbers dont lie: self-driving cars are getting good (2017)"},{"key":"e_1_2_1_2_7_2","unstructured":"Hinton GE Rumelhart DE Williams RJ (1998) Learning representations by back-propagating errors. In: Cognitive modeling 1998"},{"key":"e_1_2_1_2_8_2","unstructured":"Epoch model (2016)"},{"key":"e_1_2_1_2_9_2","unstructured":"Fawzi A Fawzi O Frossard P (2015) Analysis of classifiers' robustness to adversarial perturbations. CoRR arXiv:1502.02590"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Feth P Schneider D Adler R (2017) A conceptual safety supervisor definition and evaluation framework for autonomous systems. In: Computer safety reliability and security\u201436th international conference SAFECOMP 2017 Trento Italy September 13\u201315 2017 proceedings pp 135\u2013148","DOI":"10.1007\/978-3-319-66266-4_9"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/3086952"},{"key":"e_1_2_1_2_12_2","unstructured":"Google's self-driving car caused its first crash (2016)"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Hauke J Kossowski T (2011) Comparison of values of Pearsons and Spearmans correlation coefficients on the same sets of data. In: Quaestiones geographicae p 87","DOI":"10.2478\/v10117-011-0021-1"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Huang X Kwiatkowska M Wang S Wu M (2017) Safety verification of deep neural networks. In: Computer aided verification\u201429th international conference CAV 2017 Heidelberg Germany July 24\u201328 2017 proceedings part I pp 3\u201329","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_2_1_2_15_2","unstructured":"Huang X"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Katz G Barrett CW Dill DL Julian K Kochenderfer MJ (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Computer aided verification\u201429th international conference CAV 2017 Heidelberg Germany July 24\u201328 2017 proceedings part I pp 97\u2013117","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Katz G Barrett CW Dill DL Julian K Kochenderfer MJ (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. CoRR arXiv:1702.01135","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Kane A Chowdhury O Datta A Koopman P (2015) A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Runtime verification\u20136th international conference RV 2015 Vienna Austria September 22\u201325 2015. Proceedings pp 102\u2013117","DOI":"10.1007\/978-3-319-23820-3_7"},{"key":"e_1_2_1_2_19_2","unstructured":"Keras (2019). https:\/\/keras.io"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Kalra N Paddock SM (2016) Driving to safety: how many miles of driving would it take to demonstrate autonomous vehicle reliability?. In: Transportation research part A: policy and practice vol 94 p 182C193","DOI":"10.1016\/j.tra.2016.09.010"},{"key":"e_1_2_1_2_21_2","unstructured":"Nair V Hinton GE (2010) Rectified linear units improve restricted Boltzmann machines. In: Proceedings of the 27th international conference on machine learning (ICML-10) June 21\u201324 2010 Haifa Israel pp 807\u2013814"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Naumann M K\u00f6nigshof H Stiller C (2019) Provably safe and smooth lane changes in mixed trafic. In: 2019 IEEE intelligent transportation systems conference ITSC 2019 Auckland New Zealand October 27\u201330 2019 pp 1832\u20131837","DOI":"10.1109\/ITSC.2019.8917461"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Pei K Cao Y Yang J Jana S (2017) Deepxplore: automated whitebox testing of deep learning systems. In: Proceedings of the 26th symposium on operating systems principles Shanghai China October 28\u201331 2017 pp 1\u201318","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_2_1_2_24_2","unstructured":"Pek C Koschi M Althoff M (2019) An online verification framework for motion planning of self-driving vehicles with safety guarantees. In: AAET"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Papernot N McDaniel PD Goodfellow IJ Jha S Celik ZB Swami A (2016) Practical black-box attacks against deep learning systems using adversarial examples. CoRR arXiv:1602.02697","DOI":"10.1145\/3052973.3053009"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/2350156.2350160"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Pek C Zahn P Althoff M (2017) Verifying the safety of lane change maneuvers of self-driving vehicles based on formalized traffic rules. In: IEEE intelligent vehicles symposium IV 2017 Los Angeles CA USA June 11\u201314 2017 pp 1477\u20131483","DOI":"10.1109\/IVS.2017.7995918"},{"key":"e_1_2_1_2_28_2","unstructured":"Rambo model (2016)"},{"key":"e_1_2_1_2_29_2","unstructured":"Rambo model (2017). https:\/\/github.com\/udacity\/self-driving-car\/tree\/master\/steering-models\/community-models\/rambo"},{"key":"e_1_2_1_2_30_2","unstructured":"Roohi N Kaur R Weimer J Sokolsky O Lee I (2018) Self-driving vehicle verification towards a benchmark. CoRR arXiv:1806.08810"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Stahl T Eicher M Betz J Diermeyer F (2020) Online verification concept for autonomous vehicles\u2014illustrative study for a trajectory planning module. CoRR arXiv:2005.07740","DOI":"10.1109\/ITSC45102.2020.9294703"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann B Hess D Eilbrecht J Stursberg O K\u00f6ster F Althoff M (2017) Ensuring drivability of planned motions using formal methods. In: 20th IEEE international conference on intelligent transportation systems ITSC 2017 Yokohama Japan October 16\u201319 2017 pp 1\u20138","DOI":"10.1109\/ITSC.2017.8317647"},{"key":"e_1_2_1_2_33_2","unstructured":"Rishi K Samer H Chris R (2015) Using convolutional neural networks for image recognition. Technical report 2015"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Spearman C (1904) The proof and measurement of association between two things. Am J Psychol 72C101","DOI":"10.2307\/1412159"},{"key":"e_1_2_1_2_35_2","unstructured":"Shalev-Shwartz S Shammah S Shashua A (2017) On a formal model of safe and scalable self-driving cars. CoRR arXiv:1708.06374"},{"key":"e_1_2_1_2_36_2","unstructured":"SullyChen. Driving dataset"},{"key":"e_1_2_1_2_37_2","unstructured":"Safety and trustworthiness of deep neural networks: a survey. CoRR arXiv:1812.08342 2018. Withdrawn"},{"key":"e_1_2_1_2_38_2","unstructured":"Szegedy C Zaremba W Sutskever I Bruna J Erhan D Goodfellow IJ Fergus R (2014) Intriguing properties of neural networks. In: 2nd international conference on learning representations ICLR 2014 Banff AB Canada April 14\u201316 2014 conference track proceedings"},{"key":"e_1_2_1_2_39_2","unstructured":"Tesla says vehicle in deadly crash was on autopilot (2018)"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Tian Y Pei K Jana S Ray B (2018) Deeptest: automated testing of deep-neural-network-driven autonomous cars. In: Proceedings of the 40th international conference on software engineering ICSE 2018 Gothenburg Sweden May 27\u2013June 03 2018 pp 303\u2013314","DOI":"10.1145\/3180155.3180220"},{"key":"e_1_2_1_2_41_2","unstructured":"Cheung SC Chen TY Yiu SM (1998) Metamorphic testing: a new approach for generating next test cases. Technical report technical report HKUST-CS98-01 Department of Computer Science Hong Kong University of Science and Technology Hong Kong"},{"key":"e_1_2_1_2_42_2","unstructured":"Fatal car crash involving a self-driving uber shows there are major flaws in the software hardware and testing procedures involving autonomous vehicles (2018)"},{"key":"e_1_2_1_2_43_2","unstructured":"Z3 (2019). http:\/\/rise4fun.com\/z3"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Zhang M Zhang Y Zhang L Liu C Khurshid S (2018) Deeproad: Gan-based metamorphic testing and input validation framework for autonomous driving systems. In: Proceedings of the 33rd ACM\/IEEE international conference on automated software engineering ASE 2018 Montpellier France September 3\u20137 2018 pp 132\u2013142","DOI":"10.1145\/3238147.3238187"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00539-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00539-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00539-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00539-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T11:20:43Z","timestamp":1697973643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00539-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["10.1007\/s00165-021-00539-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00539-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"10 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 January 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}