Advertisement

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

  • Tommaso DreossiEmail author
  • Alexandre Donzé
  • Sanjit A. Seshia
Article
First Online:
  • 11 Downloads

Abstract

Cyber-physical systems (CPS), such as automotive systems, are starting to include sophisticated machine learning (ML) components. Their correctness, therefore, depends on properties of the inner ML modules. While learning algorithms aim to generalize from examples, they are only as good as the examples provided, and recent efforts have shown that they can produce inconsistent output under small adversarial perturbations. This raises the question: can the output from learning components lead to a failure of the entire CPS? In this work, we address this question by formulating it as a problem of falsifying signal temporal logic specifications for CPS with ML components. We propose a compositional falsification framework where a temporal logic falsifier and a machine learning analyzer cooperate with the aim of finding falsifying executions of the considered model. The efficacy of the proposed technique is shown on an automatic emergency braking system model with a perception component based on deep neural networks.

Keywords

Cyber-physical systems Machine learning Falsification Temporal logic Deep learning Neural networks Autonomous driving 
This is a preview of subscription content, log in to check access.

Notes

References

  1. 1.
  2. 2.
    Udacity self-driving car simulator built with unity. https://github.com/udacity/self-driving-car-sim
  3. 3.
    Abadi, M. et al.: TensorFlow: Large-scale machine learning on heterogeneous systems (2015). Software available from tensorflow.orgGoogle Scholar
  4. 4.
    Annpureddy, Y., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: a tool for temporal logic falsification for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pp. 254–257 (2011)Google Scholar
  5. 5.
    Blum, A.L., Langley, P.: Selection of relevant features and examples in machine learning. Artif. Intell. 97(1), 245–271 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L.D., Monfort, M., Muller, U., Zhang, J., et al.: End to end learning for self-driving cars (2016). arXiv preprint arXiv:1604.07316
  7. 7.
    Branicky, M.S., LaValle, S.M., Olson, K., Yang, L.: Quasi-randomized path planning. In: IEEE International Conference on Robotics and Automation, 2001. Proceedings 2001 ICRA, vol. 2, pp. 1481–1487. IEEE (2001)Google Scholar
  8. 8.
    Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 39–57 (2017)Google Scholar
  9. 9.
    Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Computer Aided Verification, CAV, pp. 167–170 (2010)Google Scholar
  10. 10.
    Donzé, A., Ferrere, T., Maler, O.: Efficient robust monitoring for STL. In: Computer Aided Verification, CAV, pp. 264–279. Springer, Berlin (2013)Google Scholar
  11. 11.
    Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: NASA Formal Methods, NFM, pp. 127–142 (2015)Google Scholar
  12. 12.
    Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: NASA Formal Methods Conference (NFM) (2017)Google Scholar
  13. 13.
    Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Systematic testing of convolutional neural networks for autonomous driving. In: ICML Workshop on Reliable Machine Learning in the Wild (RMLW) (2017). arXiv:1708.03309
  14. 14.
    Dreossi, T., Jha, S., Seshia, S.A.: Semantic adversarial deep learning. In: 30th International Conference on Computer Aided Verification (CAV) (2018)Google Scholar
  15. 15.
    Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 68–82. Springer, Berlin (2015)Google Scholar
  16. 16.
    Fawzi, A., Fawzi, O., Frossard, P.: Analysis of classifiers’ robustness to adversarial perturbations (2015). arXiv preprint arXiv:1502.02590
  17. 17.
    Hannaford, B.: Resolution-first scanning of multidimensional spaces. CVGIP Graph. Models Image Process. 55(5), 359–369 (1993)CrossRefGoogle Scholar
  18. 18.
    Hinton, G., et al.: Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Signal Process. Mag. 29(6), 82–97 (2012)CrossRefGoogle Scholar
  19. 19.
    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks (2016). CoRR arXiv:1610.06940
  20. 20.
    Iandola, F.N., Han, S., Moskewicz, M.W., Ashraf, K., Dally, W.J., Keutzer, K.: Squeezenet: Alexnet-level accuracy with 50x fewer parameters and \(<\) 0.5 mb model size (2016). arXiv preprint arXiv:1602.07360
  21. 21.
    Jia, Y., Shelhamer, E., Donahue, J., Karayev, S., Long, J., Girshick, R., Guadarrama, S., Darrell, T.: Caffe: convolutional architecture for fast feature embedding. In: ACM Multimedia Conference, ACMMM, pp. 675–678 (2014)Google Scholar
  22. 22.
    Jin, X., Donzé, A., Deshmukh, J., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE Trans. Comput.-Aided Des. Circuits Syst. 34(11), 1704–1717 (2015)CrossRefzbMATHGoogle Scholar
  23. 23.
    Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097–1105 (2012)Google Scholar
  24. 24.
    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152–166. Springer, Berlin (2004)Google Scholar
  25. 25.
    Matousek, J.: Geometric Discrepancy: An Illustrated Guide, vol. 18. Springer, Berlin (2009)zbMATHGoogle Scholar
  26. 26.
    Michalski, R .S., Carbonell, J .G., Mitchell, T .M.: Machine Learning: An Artificial Intelligence Approach. Springer, Berlin (2013)zbMATHGoogle Scholar
  27. 27.
    Moosavi-Dezfooli, S.-M., Fawzi, A., Frossard, P.: DeepFool: a simple and accurate method to fool deep neural networks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 2574–2582 (2016)Google Scholar
  28. 28.
    Morokoff, W.J., Caflisch, R.E.: Quasi-random sequences and their discrepancies. SIAM J. Sci. Comput. 15(6), 1251–1279 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Nguyen, A., Yosinski, J., Clune, J.: Deep neural networks are easily fooled: high confidence predictions for unrecognizable images. In: Computer Vision and Pattern Recognition, CVPR, pp. 427–436. IEEE (2015)Google Scholar
  30. 30.
    Niederreiter, H.: Low-discrepancy and low-dispersion sequences. J. Number Theory 30(1), 51–70 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Niederreiter, H.: Random Number Generation and Quasi-Monte Carlo Methods. SIAM, Philadelphia (1992)CrossRefzbMATHGoogle Scholar
  32. 32.
    Pei, K., Cao, Y., Yang, J., Jana, S.: DeepXplore: automated whitebox testing of deep learning systems. In: Proceedings of the 26th Symposium on Operating Systems Principles (SOSP), pp. 1–18 (2017)Google Scholar
  33. 33.
    Rosenblatt, J., Wierdl, M.: Pointwise ergodic theorems via harmonic analysis. In: Conference on Ergodic Theory, No. 205, pp. 3–151 (1995)Google Scholar
  34. 34.
    Seshia, S.A., Desai, A., Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Shivakumar, S., Vazquez-Chanlatte, M., Yue, X.: Formal specification for deep neural networks. In: 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 20–34 (2018)Google Scholar
  35. 35.
    Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence (2016). CoRR arXiv:1606.08514
  36. 36.
    Shirley, P. et al.: Discrepancy as a quality measure for sample distributions. In: Proceedings of Eurographics, vol. 91, pp. 183–194 (1991)Google Scholar
  37. 37.
    Sloan, I .H., Joe, S.: Lattice Methods for Multiple Integration. Oxford University Press, Oxford (1994)zbMATHGoogle Scholar
  38. 38.
    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (2013). arXiv:1312.6199
  39. 39.
    Taeyoung, L., Kyongsu, Y., Jangseop, K., Jaewan, L.: Development and evaluations of advanced emergency braking system algorithm for the commercial vehicle. In: Enhanced Safety of Vehicles Conference, ESV, pp. 11–0290 (2011)Google Scholar
  40. 40.
    Trandafir, Aurel., Weisstein, Eric, W.: Quasirandom sequence. From MathWorld—A Wolfram Web ResourceGoogle Scholar
  41. 41.
    Vapnik, V.: Principles of risk minimization for learning theory. In: NIPS, pp. 831–838 (1991)Google Scholar
  42. 42.
    Vazquez-Chanlatte, M., Deshmukh, J.V., Jin, X., Seshia, S.A.: Logical clustering and learning for time-series data. In: Computer Aided Verification—29th International Conference (CAV), pp. 305–325 (2017)Google Scholar
  43. 43.
    Weyl, H.: Über die gleichverteilung von zahlen mod. eins. Math. Ann. 77(3), 313–352 (1916)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 44.
    Yamaguchi, T., Kaga, T., Donzé, A., Seshia, S.A.: Combining requirement mining, software model checking, and simulation-based verification for industrial automotive systems. In: Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD) (2016)Google Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  • Tommaso Dreossi
    • 1
    Email author
  • Alexandre Donzé
    • 2
  • Sanjit A. Seshia
    • 1
  1. 1.University of California, BerkeleyBerkeleyUSA
  2. 2.Decyphir SASMoiransFrance

Personalised recommendations

Cite article

Buy options