Compositional falsification of cyber-physical systems with machine learning components. (English) Zbl 1468.68126
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T05 | Learning and adaptive systems in artificial intelligence |
| 68T07 | Artificial neural networks and deep learning |
| 93C83 | Control/observation systems involving computers (process control, etc.) |
Keywords:
cyber-physical systems; machine learning; falsification; temporal logic; deep learning; neural networks; autonomous drivingSoftware:
C2e2; TensorFlow; DeepFool; ImageNet; DeepXplore; Caffe; SqueezeNet; self-driving-car-sim; AlexNet; GitHub; Breach; S-TaLiRoReferences:
| [1] | Imagenet. http://image-net.org/ |
| [2] | Udacity self-driving car simulator built with unity. https://github.com/udacity/self-driving-car-sim |
| [3] | Abadi, M. et al.: TensorFlow: Large-scale machine learning on heterogeneous systems (2015). Software available from tensorflow.org |
| [4] | Annpureddy, Yashwanth; Liu, Che; Fainekos, Georgios; Sankaranarayanan, Sriram, S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems, 254-257 (2011), Berlin, Heidelberg · Zbl 1316.68069 · doi:10.1007/978-3-642-19835-9_21 |
| [5] | Blum, A.L., Langley, P.: Selection of relevant features and examples in machine learning. Artif. Intell. 97(1), 245-271 (1997) · Zbl 0904.68142 · doi:10.1016/S0004-3702(97)00063-5 |
| [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] | 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) |
| [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) |
| [9] | Donzé, Alexandre, Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems, 167-170 (2010), Berlin, Heidelberg · doi:10.1007/978-3-642-14295-6_17 |
| [10] | Donzé, Alexandre; Ferrère, Thomas; Maler, Oded, Efficient Robust Monitoring for STL, 264-279 (2013), Berlin, Heidelberg · doi:10.1007/978-3-642-39799-8_19 |
| [11] | Dreossi, Tommaso; Dang, Thao; Donzé, Alexandre; Kapinski, James; Jin, Xiaoqing; Deshmukh, Jyotirmoy V., Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems, 127-142 (2015), Cham |
| [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) · Zbl 1468.68126 |
| [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] | Dreossi, Tommaso; Jha, Somesh; Seshia, Sanjit A., Semantic Adversarial Deep Learning, 3-26 (2018), Cham · doi:10.1007/978-3-319-96145-3_1 |
| [15] | Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh; Potok, Matthew, C2E2: A Verification Tool for Stateflow Models, 68-82 (2015), Berlin, Heidelberg · doi:10.1007/978-3-662-46681-0_5 |
| [16] | Fawzi, A., Fawzi, O., Frossard, P.: Analysis of classifiers’ robustness to adversarial perturbations (2015). arXiv preprint arXiv:1502.02590 · Zbl 1462.62383 |
| [17] | Hannaford, B.: Resolution-first scanning of multidimensional spaces. CVGIP Graph. Models Image Process. 55(5), 359-369 (1993) · doi:10.1006/cgip.1993.1027 |
| [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) · doi:10.1109/MSP.2012.2205597 |
| [19] | Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks (2016). CoRR arXiv:1610.06940 · Zbl 1494.68166 |
| [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] | 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) |
| [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) · doi:10.1109/TCAD.2015.2421907 |
| [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) |
| [24] | Maler, Oded; Nickovic, Dejan, Monitoring Temporal Properties of Continuous Signals, 152-166 (2004), Berlin, Heidelberg · Zbl 1109.68518 · doi:10.1007/978-3-540-30206-3_12 |
| [25] | Matousek, J.: Geometric Discrepancy: An Illustrated Guide, vol. 18. Springer, Berlin (2009) · Zbl 0930.11060 |
| [26] | Michalski, R .S., Carbonell, J .G., Mitchell, T .M.: Machine Learning: An Artificial Intelligence Approach. Springer, Berlin (2013) · Zbl 0593.68060 |
| [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) |
| [28] | Morokoff, W.J., Caflisch, R.E.: Quasi-random sequences and their discrepancies. SIAM J. Sci. Comput. 15(6), 1251-1279 (1994) · Zbl 0815.65002 · doi:10.1137/0915077 |
| [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) |
| [30] | Niederreiter, H.: Low-discrepancy and low-dispersion sequences. J. Number Theory 30(1), 51-70 (1988) · Zbl 0651.10034 · doi:10.1016/0022-314X(88)90025-X |
| [31] | Niederreiter, H.: Random Number Generation and Quasi-Monte Carlo Methods. SIAM, Philadelphia (1992) · Zbl 0761.65002 · doi:10.1137/1.9781611970081 |
| [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) |
| [33] | Rosenblatt, J., Wierdl, M.: Pointwise ergodic theorems via harmonic analysis. In: Conference on Ergodic Theory, No. 205, pp. 3-151 (1995) · Zbl 0848.28008 |
| [34] | Seshia, Sanjit A.; Desai, Ankush; Dreossi, Tommaso; Fremont, Daniel J.; Ghosh, Shromona; Kim, Edward; Shivakumar, Sumukh; Vazquez-Chanlatte, Marcell; Yue, Xiangyu, Formal Specification for Deep Neural Networks, 20-34 (2018), Cham · Zbl 1517.68345 · doi:10.1007/978-3-030-01090-4_2 |
| [35] | Seshia, S.A., Sadigh, D., Sastry, S.S.: Towards verified artificial intelligence (2016). CoRR arXiv:1606.08514 |
| [36] | Shirley, P. et al.: Discrepancy as a quality measure for sample distributions. In: Proceedings of Eurographics, vol. 91, pp. 183-194 (1991) |
| [37] | Sloan, I .H., Joe, S.: Lattice Methods for Multiple Integration. Oxford University Press, Oxford (1994) · Zbl 0855.65013 |
| [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] | 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) |
| [40] | Trandafir, Aurel., Weisstein, Eric, W.: Quasirandom sequence. From MathWorld—A Wolfram Web Resource |
| [41] | Vapnik, V.: Principles of risk minimization for learning theory. In: NIPS, pp. 831-838 (1991) |
| [42] | Vazquez-Chanlatte, Marcell; Deshmukh, Jyotirmoy V.; Jin, Xiaoqing; Seshia, Sanjit A., Logical Clustering and Learning for Time-Series Data, 305-325 (2017), Cham · Zbl 1494.68232 · doi:10.1007/978-3-319-63387-9_15 |
| [43] | Weyl, H.: Über die gleichverteilung von zahlen mod. eins. Math. Ann. 77(3), 313-352 (1916) · JFM 46.0278.06 · doi:10.1007/BF01475864 |
| [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) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
