Abstract
As autonomy becomes prevalent in many applications, ranging from recommendation systems to fully autonomous vehicles, there is an increased need to provide safety guarantees for such systems. The problem is difficult, as these are large, complex systems which operate in uncertain environments, requiring data-driven machine-learning components. However, learning techniques such as Deep Neural Networks, widely used today, are inherently unpredictable and lack the theoretical foundations to provide strong assurance guarantees. We present a compositional approach for the scalable, formal verification of autonomous systems that contain Deep Neural Network components. The approach uses assume-guarantee reasoning whereby contracts, encoding the input–output behavior of individual components, allow the designer to model and incorporate the behavior of the learning-enabled components working side-by-side with the other components. We illustrate the approach on an example taken from the autonomous vehicles domain.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
S. Bak, S. Chaki, Verifying cyber-physical systems by combining software model checking with hybrid systems reachability, in 2016 International Conference on Embedded Software, EMSOFT 2016, Pittsburgh, Pennsylvania, USA, October 1–7, 2016 (2016), pp. 10:1–10:10
S. Bogomolov, G. Frehse, M. Greitschus, R. Grosu, C.S. Pasareanu, A. Podelski, T. Strump, Assume-guarantee abstraction refinement meets hybrid systems, in Proceedings of Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18–20, 2014 (2014), pp. 116–131
N. Carlini, D. Wagner, Towards evaluating the robustness of neural networks, in Proceedings of 38th IEEE Symposium on Security and Privacy (2017)
C. Chilton, B. Jonsson, M.Z. Kwiatkowska, An algebraic theory of interface automata. Theor. Comput. Sci. 549, 146–174 (2014)
C. Chilton, B. Jonsson, M.Z. Kwiatkowska, Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program. 91, 115–137 (2014)
T. Dreossi, A. Donzé, S.A. Seshia, Compositional falsification of cyber-physical systems with machine learning components, in Proceedings of NASA Formal Methods - 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16–18, 2017 (2017), pp. 357–372
R. Feinman, R.R. Curtin, S. Shintre, A.B. Gardner, Detecting adversarial samples from artifacts. Technical Report (2017). http://arxiv.org/abs/1703.00410
I.J. Goodfellow, J. Shlens, C. Szegedy, Explaining and harnessing adversarial examples. Technical Report (2014). http://arxiv.org/abs/1412.6572
D. Gopinath, G. Katz, C.S. Pasareanu, C. Barrett, Deepsafe: a data-driven approach for checking adversarial robustness in neural networks, in Proc. ATVA’18 (2017). https://arxiv.org/abs/1710.00486
X. Huang, M. Kwiatkowska, S. Wang, M. Wu, Safety verification of deep neural networks, in Proceedings of 29th International Conference on Computer Aided Verification (CAV) (2017), pp. 3–29
K. Julian, J. Lopez, J. Brush, M. Owen, M. Kochenderfer, Policy compression for aircraft collision avoidance systems, in Digital Avionics Systems Conference (DASC) (2016), pp. 1–10
T. Kanungo, D.M. Mount, N.S. Netanyahu, C.D. Piatko, R. Silverman, A.Y. Wu, An efficient k-means clustering algorithm: analysis and implementation. IEEE Trans. Pattern Anal. Mach. Intell. 24(7), 881–892 (2002)
G. Katz, C. Barrett, D. Dill, K. Julian, M. Kochenderfer, Reluplex: an efficient SMT solver for verifying deep neural networks, in Proceedings of the 29th International Conference on Computer Aided Verification (CAV) (2017), pp. 97–117
A. Komuravelli, C.S. Pasareanu, E.M. Clarke, Assume-guarantee abstraction refinement for probabilistic systems, in Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7–13, 2012 (2012), pp. 310–326
A. Kurakin, I. Goodfellow, S. Bengio, Adversarial examples in the physical world, 2016. Technical Report. http://arxiv.org/abs/1607.02533
Y. LeCun, C. Cortes, C.J.C. Burges, The MNIST database of handwritten digits. http://yann.lecun.com/exdb/mnist/
Y. Li, Y. Gal, Dropout inference in Bayesian neural networks with alpha-divergences, in International Conference on Machine Learning (2017), pp. 2052–2061
J. Li, P. Nuzzo, A.L. Sangiovanni-Vincentelli, Y. Xi, D. Li, Stochastic assume-guarantee contracts for cyber-physical system design under probabilistic requirements. CoRR (2017). http://arxiv.org/abs/1705.09316
C.S. Pasareanu, D. Giannakopoulou, M.G. Bobaru, J.M. Cobleigh, H. Barringer, Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des. 32(3), 175–205 (2008)
C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, 2013. Technical Report. http://arxiv.org/abs/1312.6199
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Păsăreanu, C.S., Gopinath, D., Yu, H. (2019). Compositional Verification for Autonomous Systems with Deep Learning Components. In: Yu, H., Li, X., Murray, R., Ramesh, S., Tomlin, C. (eds) Safe, Autonomous and Intelligent Vehicles. Unmanned System Technologies. Springer, Cham. https://doi.org/10.1007/978-3-319-97301-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-97301-2_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97300-5
Online ISBN: 978-3-319-97301-2
eBook Packages: EngineeringEngineering (R0)