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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Notes
Udacity’s Self-Driving Car Simulator: https://github.com/udacity/self-driving-car-sim.
Unity: https://unity3d.com/.
Socket.IO protocol: https://github.com/socketio.
References
Imagenet. http://image-net.org/
Udacity self-driving car simulator built with unity. https://github.com/udacity/self-driving-car-sim
Abadi, M. et al.: TensorFlow: Large-scale machine learning on heterogeneous systems (2015). Software available from tensorflow.org
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)
Blum, A.L., Langley, P.: Selection of relevant features and examples in machine learning. Artif. Intell. 97(1), 245–271 (1997)
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
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)
Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 39–57 (2017)
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Computer Aided Verification, CAV, pp. 167–170 (2010)
Donzé, A., Ferrere, T., Maler, O.: Efficient robust monitoring for STL. In: Computer Aided Verification, CAV, pp. 264–279. Springer, Berlin (2013)
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)
Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: NASA Formal Methods Conference (NFM) (2017)
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
Dreossi, T., Jha, S., Seshia, S.A.: Semantic adversarial deep learning. In: 30th International Conference on Computer Aided Verification (CAV) (2018)
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)
Fawzi, A., Fawzi, O., Frossard, P.: Analysis of classifiers’ robustness to adversarial perturbations (2015). arXiv preprint arXiv:1502.02590
Hannaford, B.: Resolution-first scanning of multidimensional spaces. CVGIP Graph. Models Image Process. 55(5), 359–369 (1993)
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)
Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks (2016). CoRR arXiv:1610.06940
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
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)
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)
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)
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)
Matousek, J.: Geometric Discrepancy: An Illustrated Guide, vol. 18. Springer, Berlin (2009)
Michalski, R .S., Carbonell, J .G., Mitchell, T .M.: Machine Learning: An Artificial Intelligence Approach. Springer, Berlin (2013)
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)
Morokoff, W.J., Caflisch, R.E.: Quasi-random sequences and their discrepancies. SIAM J. Sci. Comput. 15(6), 1251–1279 (1994)
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)
Niederreiter, H.: Low-discrepancy and low-dispersion sequences. J. Number Theory 30(1), 51–70 (1988)
Niederreiter, H.: Random Number Generation and Quasi-Monte Carlo Methods. SIAM, Philadelphia (1992)
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)
Rosenblatt, J., Wierdl, M.: Pointwise ergodic theorems via harmonic analysis. In: Conference on Ergodic Theory, No. 205, pp. 3–151 (1995)
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)
Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence (2016). CoRR arXiv:1606.08514
Shirley, P. et al.: Discrepancy as a quality measure for sample distributions. In: Proceedings of Eurographics, vol. 91, pp. 183–194 (1991)
Sloan, I .H., Joe, S.: Lattice Methods for Multiple Integration. Oxford University Press, Oxford (1994)
Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (2013). arXiv:1312.6199
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)
Trandafir, Aurel., Weisstein, Eric, W.: Quasirandom sequence. From MathWorld—A Wolfram Web Resource
Vapnik, V.: Principles of risk minimization for learning theory. In: NIPS, pp. 831–838 (1991)
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)
Weyl, H.: Über die gleichverteilung von zahlen mod. eins. Math. Ann. 77(3), 313–352 (1916)
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)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This work is funded in part by the DARPA BRASS program under Agreement Number FA8750-16-C-0043, NSF Grants CNS-1646208, CNS-1545126, CCF-1837132, and CCF-1139138, the DARPA Assured Autonomy program, Toyota under the iCyPhy center, Berkeley Deep Drive, and by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA. All the contributions of the second author with the exception of those to Sect. 5.2 occurred while he was affiliated with UC Berkeley. We gratefully acknowledge the support of NVIDIA Corporation with the donation of the Titan Xp GPU used for this research.
Rights and permissions
About this article
Cite this article
Dreossi, T., Donzé, A. & Seshia, S.A. Compositional Falsification of Cyber-Physical Systems with Machine Learning Components. J Autom Reasoning 63, 1031–1053 (2019). https://doi.org/10.1007/s10817-018-09509-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-018-09509-5