Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 4/2019

19.01.2019

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

verfasst von: Tommaso Dreossi, Alexandre Donzé, Sanjit A. Seshia

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
Nächster Artikel Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
3
Udacity’s Self-Driving Car Simulator: https://​github.​com/​udacity/​self-driving-car-sim.
 
Literatur
1.
2.
3.
Abadi, M. et al.: TensorFlow: Large-scale machine learning on heterogeneous systems (2015). Software available from tensorflow.org
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)CrossRef
5.
Blum, A.L., Langley, P.: Selection of relevant features and examples in machine learning. Artif. Intell. 97(1), 245–271 (1997)MathSciNetCrossRef
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é, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Computer Aided Verification, CAV, pp. 167–170 (2010)CrossRef
10.
Donzé, A., Ferrere, T., Maler, O.: Efficient robust monitoring for STL. In: Computer Aided Verification, CAV, pp. 264–279. Springer, Berlin (2013)CrossRef
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)
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)
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, T., Jha, S., Seshia, S.A.: Semantic adversarial deep learning. In: 30th International Conference on Computer Aided Verification (CAV) (2018)CrossRef
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)CrossRef
16.
Fawzi, A., Fawzi, O., Frossard, P.: Analysis of classifiers’ robustness to adversarial perturbations (2015). arXiv preprint arXiv:​1502.​02590
17.
Hannaford, B.: Resolution-first scanning of multidimensional spaces. CVGIP Graph. Models Image Process. 55(5), 359–369 (1993)CrossRef
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)CrossRef
19.
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)CrossRef
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, 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)CrossRef
25.
Matousek, J.: Geometric Discrepancy: An Illustrated Guide, vol. 18. Springer, Berlin (2009)MATH
26.
Michalski, R .S., Carbonell, J .G., Mitchell, T .M.: Machine Learning: An Artificial Intelligence Approach. Springer, Berlin (2013)MATH
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)MathSciNetCrossRef
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.
31.
Niederreiter, H.: Random Number Generation and Quasi-Monte Carlo Methods. SIAM, Philadelphia (1992)CrossRef
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)
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)CrossRef
35.
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)MATH
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, 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)CrossRef
43.
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)
Metadaten
Titel
Compositional Falsification of Cyber-Physical Systems with Machine Learning Components
verfasst von
Tommaso Dreossi
Alexandre Donzé
Sanjit A. Seshia
Publikationsdatum
19.01.2019
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-09509-5

Weitere Artikel der Ausgabe 4/2019

Journal of Automated Reasoning 4/2019 Zur Ausgabe

EditorialNotes

Selected Extended Papers of NFM 2017: Preface

OriginalPaper

QPCF: Higher-Order Languages and Quantum Circuits

OriginalPaper

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

OriginalPaper

Efficient Active Automata Learning via Mutation Testing

OriginalPaper

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants

OriginalPaper

An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains

Premium Partner

    Bildnachweise