Compositional Verification for Autonomous Systems with Deep Learning Components

White Paper
  • Corina S. PăsăreanuEmail author
  • Divya Gopinath
  • Huafeng Yu
Part of the Unmanned System Technologies book series (UST)


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.


  1. 1.
    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:10Google Scholar
  2. 2.
    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–131Google Scholar
  3. 3.
    N. Carlini, D. Wagner, Towards evaluating the robustness of neural networks, in Proceedings of 38th IEEE Symposium on Security and Privacy (2017)Google Scholar
  4. 4.
    C. Chilton, B. Jonsson, M.Z. Kwiatkowska, An algebraic theory of interface automata. Theor. Comput. Sci. 549, 146–174 (2014)MathSciNetCrossRefGoogle Scholar
  5. 5.
    C. Chilton, B. Jonsson, M.Z. Kwiatkowska, Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program. 91, 115–137 (2014)CrossRefGoogle Scholar
  6. 6.
    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–372Google Scholar
  7. 7.
    R. Feinman, R.R. Curtin, S. Shintre, A.B. Gardner, Detecting adversarial samples from artifacts. Technical Report (2017).
  8. 8.
    I.J. Goodfellow, J. Shlens, C. Szegedy, Explaining and harnessing adversarial examples. Technical Report (2014).
  9. 9.
    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).
  10. 10.
    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–29Google Scholar
  11. 11.
    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–10Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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–117Google Scholar
  14. 14.
    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–326Google Scholar
  15. 15.
    A. Kurakin, I. Goodfellow, S. Bengio, Adversarial examples in the physical world, 2016. Technical Report.
  16. 16.
    Y. LeCun, C. Cortes, C.J.C. Burges, The MNIST database of handwritten digits.
  17. 17.
    Y. Li, Y. Gal, Dropout inference in Bayesian neural networks with alpha-divergences, in International Conference on Machine Learning (2017), pp. 2052–2061Google Scholar
  18. 18.
    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).
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, 2013. Technical Report.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Corina S. Păsăreanu
    • 1
    Email author
  • Divya Gopinath
    • 1
  • Huafeng Yu
    • 2
  1. 1.Carnegie Mellon University and NASA AmesMoffett FieldUSA
  2. 2.BoeingChicagoUSA

Personalised recommendations