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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Concept Design: Modeling and Synthesis from Requirements to Functional Models and Simulation Kapitel lesen Erstes Kapitel lesen

2019 | OriginalPaper | Buchkapitel

4. Formal Techniques for Verification and Testing of Cyber-Physical Systems

verfasst von : Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan

Erschienen in: Design Automation of Cyber-Physical Systems

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Modern cyber-physical systems (CPS) are often developed in a model-based development (MBD) paradigm. The MBD paradigm involves the construction of different kinds of models: (1) a plant model that encapsulates the physical components of the system (e.g., mechanical, electrical, chemical components) using representations based on differential and algebraic equations, (2) a controller model that encapsulates the embedded software components of the system, and (3) an environment model that encapsulates physical assumptions on the external environment of the CPS application. In order to reason about the correctness of CPS applications, we typically pose the following question: For all possible environment scenarios, does the closed-loop system consisting of the plant and the controller exhibit the desired behavior? Typically, the desired behavior is expressed in terms of properties that specify unsafe behaviors of the closed-loop system. Often, such behaviors are expressed using variants of real-time temporal logics. In this chapter, we will examine formal methods based on bounded-time reachability analysis, simulation-guided reachability analysis, deductive techniques based on safety invariants, and formal, requirement-driven testing techniques. We will review key results in the literature, and discuss the scalability and applicability of such systems to various academic and industrial contexts. We conclude this chapter by discussing the challenge to formal verification and testing techniques posed by newer CPS applications that use AI-based software components.

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 "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
Vorheriges Kapitel An Hourglass-Shaped Architecture for Model-Based Development of Networked Cyber-Physical Systems
Nächstes Kapitel Data-Driven Safety Verification of Complex Cyber-Physical Systems
Fußnoten
1
Allowing stochasticity in the plant or environment model necessitates treating the closed-loop CPS model as a stochastic dynamical system. The techniques for verification and testing of such systems are quite different. As we wish to focus on techniques that are closer to industrial use of MBD for CPS applications, we refer the reader to [36, 71] for excellent surveys.
 
2
For a set X, let \(\mathcal {P}(X)\) denote its power set.
 
Literatur
1.
Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivancic, F., & Gupta, A. (2013). Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions on Embedded Computing Systems, 12, 95.CrossRef
2.
Abbas, H., Hoxha, B., Fainekos, G., & Ueda, K. (2014). Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In 2014 IEEE 4th Annual International Conference on Cyber Technology in Automation, Control, and Intelligent Systems (CYBER) (pp. 1–6). Piscataway: IEEE.
3.
Abbas, H., O’Kelly, M., Rodionova, A., & Mangharam, R. (2017). Safe at any speed: A simulation-based test harness for autonomous vehicles. In 7th Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy’17).
4.
Abbas, H., Rodionova, A., Bartocci, E., Smolka, S. A., & Grosu, R. (2017). Quantitative regular expressions for arrhythmia detection algorithms. In Proceedings of the International Conference on Computational Methods in Systems Biology (pp. 23–39). Berlin: Springer.CrossRef
5.
Adimoolam, A., Dang, T., Donzé, A., Kapinski, J., & Jin, X. (2017). Classification and coverage-based falsification for embedded control systems. In International Conference on Computer Aided Verification (pp. 483–503). Berlin: Springer.CrossRef
6.
Akazaki, T., Liu, S., Yamagata, Y., Duan, Y., & Hao, J. (2018). Falsification of cyber-physical systems using deep reinforcement learning. arXiv preprint arXiv:1805.00200.
7.
Althoff, M. (2015). An introduction to CORA 2015. In Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (pp. 120–151).
8.
Althoff, M., & Grebenyuk, D. (2016). Implementation of interval arithmetic in CORA 2016. In Proceedings of the 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems (pp. 91–105).
9.
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P. H., Nicollin, X., et al. (1995). The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1), 3–34.MathSciNetMATHCrossRef
10.
Alur, R., Courcoubetis, C., Henzinger, T. A., & Ho, P. H. (1993). Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Workshop on International Hybrid Systems (pp. 209–229). Berlin: Springer.CrossRef
11.
Alur, R., Dang, T., & Ivančić, F. (2003). Counter-example guided predicate abstraction of hybrid systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science (Vol. 2619, pp. 208–223). Berlin: Springer
12.
13.
Alur, R., Fisman, D., & Raghothaman, M. (2016). Regular programming for quantitative properties of data streams. In Proceedings of the European Symposium on Programming Languages and Systems (pp. 15–40). Berlin: Springer.MATHCrossRef
14.
Alur, R., & Henzinger, T. A. (1989). A really temporal logic. In Proceedings of the Symposium on Foundations of Computer Science (pp. 164–169).
15.
Alur, R., Henzinger, T. A., Lafferriere, G., & Pappas, G.J. (2000). Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88(7), 971–984.CrossRef
16.
Alur, R., Mamouras, K., & Ulus, D. (2017). Derivatives of quantitative regular expressions. In Models, algorithms, logics and tools (pp. 75–95). Cham: Springer.CrossRef
17.
Ames, A. D., Grizzle, J. W., & Tabuada, P. (2014). Control barrier function based quadratic programs with application to adaptive cruise control. In 2014 IEEE 53rd Annual Conference on Decision and Control (CDC) (pp. 6271–6278). Piscataway: IEEE.
18.
Annapureddy, Y. S. R., & Fainekos, G. E. (2010). Ant colonies for temporal logic falsification of hybrid systems. In Proceedings of the 36th Annual Conference of IEEE Industrial Electronics (pp. 91–96). Piscataway: IEEE.
19.
Annpureddy, Y., Liu, C., Fainekos, G. E., & Sankaranarayanan, S. (2011). S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 254–257). Berlin: Springer.MATH
20.
Aréchiga, N., & Krogh, B. (2014). Using verified control envelopes for safe controller design. In 2014 American Control Conference (ACC) (pp. 2918–2923). Piscataway: IEEE.CrossRef
21.
22.
Asarin, E., Dang, T., & Girard, A. (2007). Hybridization methods for the analysis of nonlinear systems. Acta Informatica, 43(7), 451–476.MathSciNetMATHCrossRef
23.
Asarin, E., Maler, O., & Pnueli, A. (1995). Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science, 138, 35–65.MathSciNetMATHCrossRef
24.
Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: MIT Press.MATH
25.
Bak, S., & Duggirala, P. S. (2017). HyLAA: A tool for computing simulation-equivalent reachability for linear systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (pp. 173–178). New York: ACM.
26.
Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., & Criminisi, A. (2016). Measuring neural net robustness with constraints. In Advances in Neural Information Processing Systems (pp. 2613–2621).
27.
Berz, M. (1999). Modern map methods in particle beam physics. Advances in Imaging and Electron Physics (Vol. 108). London: Academic.
28.
Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., et al. (2016) End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316.
29.
Bonakdarpour, B., & Finkbeiner, B. (2016). Runtime verification for HyperLTL. In International Conference on Runtime Verification (pp. 41–45). Cham: Springer.CrossRef
30.
Bonakdarpour, B., Sanchez, C., & Schneider, G. (2018). Monitoring hyperproperties by combining static analysis and runtime verification. In International Symposium on Leveraging Applications of Formal Methods (pp. 8–27). Berlin: Springer.
31.
Bournez, O., Maler, O., & Pnueli, A. (1999). Orthogonal polyhedra: Representation and computation. In Hybrid systems: Computation and control. Lecture Notes in Computer Science (Vol. 1569, pp. 46–60). Berlin: Springer.
32.
Box, G. E. P. (1979). Robustness in the strategy of scientific model building. In Robustness in Statistics (pp. 201–236). London: Academic.CrossRef
33.
Brockett, R. (1993). Hybrid models for motion control systems. In Essays on control: Perspectives in the theory and its applications (pp. 29 –53). Boston: Birkhäuser.CrossRef
34.
Cameron, F., Fainekos, G., Maahs, D. M., & Sankaranarayanan, S. (2015). Towards a verified artificial pancreas: Challenges and solutions for runtime verification. In Proceedings of Runtime Verification (RV’15). Lecture Notes in Computer Science (Vol. 9333, pp. 3–17). Cham: Springer.
35.
Cameron, F., Wilson, D. M., Buckingham, B. A., Arzumanyan, H., Clinton, P., Chase, H. P., et al. (2012). Inpatient studies of a Kalman-filter-based predictive pump shutoff algorithm. Journal of Diabetes Science and Technology, 6(5), 1142–1147.CrossRef
36.
Cassandras, C. G., & Lygeros, J. (2006). Stochastic hybrid systems. Boca Raton: CRC Press.MATHCrossRef
37.
Chaochen, Z., Hoare, C. A. R., & Ravn, A. P. (1991). A calculus of durations. Information Processing Letters, 40(5), 269–276.MathSciNetMATHCrossRef
38.
Chee, F., & Fernando, T. (2007). Closed-loop control of blood glucose. Berlin: Springer.MATH
39.
Chen, S., O’Kelly, M., Weimer, J., Sokolsky, O., & Lee, I. (2015). An intraoperative glucose control benchmark for formal verification. In 5th IFAC conference on Analysis and Design of Hybrid Systems (ADHS) (2015)
40.
Chen, X., Ábrahám, E., & Sankaranarayanan, S. (2012). Taylor model flowpipe construction for non-linear hybrid systems. In Proceedings of the 2012 IEEE 33rd Real-Time Systems Symposium (RTSS’12) (pp. 183–192). Piscataway: IEEE.CrossRef
41.
Chen, X., Ábrahám, E., & Sankaranarayanan, S. (2013). Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification. Lecture Notes in Computer Science (Vol. 8044, pp. 258–263). Berlin: Springer.
42.
Chen, X., Mover, S., & Sankaranarayanan, S. (2017). Compositional relational abstraction for nonlinear systems. ACM Transactions on Embedded Computing Systems, 16(5s), 187.
43.
Chen, X., & Sankaranarayanan, S. (2016). Decomposed reachability analysis for nonlinear systems. In 2016 IEEE Real-Time Systems Symposium (RTSS) (pp. 13–24). Piscataway: IEEE.CrossRef
44.
Chonev, V., Ouaknine, J., & Worrell, J. (2016). On the Skolem problem for continuous linear dynamical systems. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (Vol. 55, pp. 100:1–100:13). Wadern: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
45.
Chutinan, A., & Krogh, B. (1998). Computing polyhedral approximations to flow pipes for dynamic systems. In Proceedings of the 37th IEEE Conference on Decision and Control. Piscataway: IEEE.
46.
47.
Clarkson, M. R., & Schneider, F. B. (2010). Hyperproperties. Journal of Computer Security, 18(6), 1157–1210.CrossRef
48.
Cobelli, C., Man, C. D., Sparacino, G., Magni, L., Nicolao, G. D., & Kovatchev, B. P. (2009). Diabetes: Models, signals and control (methodological review). IEEE Reviews in Biomedical Engineering, 2, 54–95.CrossRef
49.
Dang, T., & Maler, O. (1998). Reachability via face lifting. In Hybrid Systems: Computation and Control. Lecture Notes in Computer Science (Vol. 1386, pp. 96–109). Berlin: Springer
50.
Dang, T., Maler, O., & Testylier, R. (2010). Accurate hybridization of nonlinear systems. In Hybrid Systems: Computation and Control (HSCC ’10) (pp. 11–20). New York: ACM.MATH
51.
Deshmukh, J., Horvat, M., Jin, X., Majumdar, R., & Prabhu, V. S. (2017). Testing cyber-physical systems through Bayesian optimization. ACM Transactions on Embedded Computing Systems, 16(5s), 170.CrossRef
52.
Deshmukh, J., Jin, X., Kapinski, J., & Maler, O. (2015). Stochastic local earch for falsification of hybrid ystems. In International Symposium on Automated Technology for Verification and Analysis (pp. 500–517). Berlin: Springer.MATHCrossRef
53.
Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M. N., & Seidl, H. (2012). Model checking information flow in reactive systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation (pp. 169–185). Berlin: Springer.MATHCrossRef
54.
Dokhanchi, A., Zutshi, A., Srinivas, R. T., Sankaranarayanan, S., & Fainekos, G. E. (2015). Requirements driven falsification with coverage metrics. In 2015 International Conference on Embedded Software (EMSOFT’15) (pp. 31–40). Piscataway: IEEE.CrossRef
55.
Donzé, A. (2010). Breach, a toolbox for verification and parameter synthesis of hybrid systems. In International Conference on Computer Aided Verification (pp. 167–170). Berlin: Springer.CrossRef
56.
Donzé, A., Ferrère, T., & Maler, O. (2013). Efficient robust monitoring for STL. In Computer Aided Verification (pp. 264–279). Berlin: Springer.CrossRef
57.
Donzé, A., & Maler, O. (2007). Systematic simulation using sensitivity analysis. In International Workshop on Hybrid Systems: Computation and Control (pp. 174–189). Berlin: Springer.CrossRef
58.
Donzé, A., & Maler, O. (2010). Robust satisfaction of temporal logic over real-valued signals. In Formal Modeling and Analysis of Timed Systems (pp. 92–106). Berlin: Springer.MATHCrossRef
59.
Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Deshmukh, J., & Jin, X. (2015). Efficient guiding strategies for testing of temporal properties of hybrid systems. In NASA Formal Methods Symposium (pp. 127–142). Berlin: Springer.
60.
Dreossi, T., Donzé, A., & Seshia, S. A. (2017). Compositional falsification of cyber-physical systems with machine learning components. In NASA Formal Methods. Lecture Notes in Computer Science (Vol. 10227). Berlin: Springer.
61.
62.
Duggirala, P. S., Fan, C., Mitra, S., & Viswanathan, M. (2015). Meeting a powertrain verification challenge. In Proceedings of the 27th International Conference on Computer Aided Verification. Part I (pp. 536–543). Cham: Springer.
63.
Duggirala, P. S., Potok, M., Mitra, S., & Viswanathan, M. (2015). C2E2: A tool for verifying annotated hybrid systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC’15) (pp. 307–308). New York: ACM.
64.
Dutta, S., Jha, S., Sankaranarayanan, S., & Tiwari, A. (2018). Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine, 51(16), 151–156.CrossRef
65.
Dutta, S., Jha, S., Sankaranarayanan, S., & Tiwari, A. (2018). Output range analysis for deep feedforward neural networks. In Proceedings of NASA Formal Methods Symposium (NFM). Lecture Notes in Computer Science (Vol. 10811, pp. 121–138). Berlin: Springer.
66.
Dutta, S., Kushner, T., & Sankaranarayanan, S. (2018). Robust data-driven control of artificial pancreas systems using neural networks. In M. Češka, & D. Šafránek (Eds.), Computational methods in systems biology (pp. 183–202). Cham: Springer.MATHCrossRef
67.
Ehlers, R. (2017). Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science (Vol. 10482, pp. 269–286). Berlin: Springer.CrossRef
68.
Fainekos, G. E., & Pappas, G. J. (2009). Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42), 4262–4291.MathSciNetMATHCrossRef
69.
Fan, C., Kapinski, J., Jin, X., & Mitra, S. (2018). Simulation-driven reachability using matrix measures. ACM Transactions on Embedded Computing Systems, 17(1), 21:1–21:28.
70.
Finkbeiner, B., Rabe, M. N., & Sánchez, C. (2015). Algorithms for model checking HyperLTL and HyperCTL*. In International Conference on Computer Aided Verification (pp. 30–48). Berlin: Springer.CrossRef
71.
Forejt, V., Kwiatkowska, M., Norman, G., & Parker, D. (2011). Automated verification techniques for probabilistic systems. In International School on Formal Methods for the Design of Computer, Communication and Software Systems (pp. 53–113). Berlin: Springer.
72.
Fränzle, M., Herde, C., Ratschan, S., Schubert, T., & Teige, T. (2007). Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1, 209–236.MATH
73.
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., et al. (2011). SpaceEx: Scalable verification of hybrid systems. In International Conference on Computer Aided Verification (CAV’11). Lecture Notes in Computer Science (Vol. 6806, pp. 379–395). Berlin: Springer.CrossRef
74.
75.
Gadkari, A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., & Shashidhar, K. (2008). Automotgen: Automatic model oriented test generator for embedded control systems. In A. Gupta & S. Malik (Eds.), Computer aided verification. Lecture Notes in Computer Science (Vol. 5123, pp. 204–208). Berlin: Springer.
76.
Gao, S., Kong, S., & Clarke, E. M. (2013). dReal: An SMT solver for nonlinear theories over the reals. In International Conference on Automated Deduction (CADE’13). Lecture Notes in Computer Science (Vol. 7898, pp. 208–214). Berlin: Springer.
77.
Geiger, A., Lenz, P., & Urtasun, R. (2012) Are we ready for autonomous driving? The Kitti vision benchmark suite. In 2012 IEEE Conference on Computer Vision and Pattern Recognition (CVPR) (pp. 3354–3361). Piscataway: IEEE.CrossRef
78.
Girard, A. (2005). Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science (Vol. 3414, pp. 291–305). Berlin: Springer.MATHCrossRef
79.
Girard, A., & Pappas, G. J. (2005). Approximate bisimulations for nonlinear dynamical systems. In Proceedings of the 44th IEEE Conference on Decision and Control (pp. 684–689). Piscataway: IEEE.CrossRef
80.
81.
Goubault, E., Jourdan, J. H., Putot, S., & Sankaranarayanan, S. (2014). Finding non-polynomial positive invariants and lyapunov functions for polynomial systems through darboux polynomials. In Proceedings of the American Control Conference (ACC) (pp. 3571–3578). New York: IEEE Press.
82.
Hainry, E. (2008). Reachability in linear dynamical systems. In Logic and theory of algorithms (pp. 241–250). Berlin: Springer.CrossRef
83.
Henzinger, T. A. (1996). The theory of hybrid automata. In Proceedings of the Logic in Computer Science (pp. 278–292). Piscataway: IEEE.
84.
Henzinger, T. A., Kopke, P. W., Puri, A., & Varaiya, P. (1998). What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1), 94–124.MathSciNetMATHCrossRef
85.
Herde, C., Eggers, A., Franzle M., & Teige, T. (2008). Analysis of hybrid systems using HySAT. In Third International Conference on Systems, 2008 (pp. 13–18). Piscataway: IEEE.
86.
Hovorka, R. (2005). Continuous glucose monitoring and closed-loop systems. Diabetic Medicine, 23(1), 1–12.CrossRef
87.
Huang, X., Kwiatkowska, M., Wang, S., & Wu, M. (2017). Safety verification of deep neural networks. In Proceedings of the Computer Aided Verification (pp. 3–29). Cham: Springer.CrossRef
88.
Jiang, Z., Pajic, M., Moarref, S., Alur, R., & Mangharam, R. (2012). Modeling and verification of a dual chamber implantable pacemaker. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science (Vol. 7214, pp. 188–203). Berlin: Springer.
89.
Junghanns, A., Mauss, J., & Tatar, M. (2008). Tatar: Testweaver—a tool for simulation-based test of mechatronic designs. In 6th International Modelica Conference, Bielefeld, March 3. Citeseer
90.
Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., & Aréchiga, N. (2014). Simulation-guided lyapunov analysis for hybrid dynamical systems. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (pp. 133–142 ). New York: ACM.MATH
91.
Kapinski, J., Krogh, B. H., Maler, O., & Stursberg, O. (2003). On systematic simulation of open continuous systems. In International Workshop on Hybrid Systems: Computation and Control (pp. 283–297). Berlin: Springer.MATHCrossRef
92.
Kato, K., Ishikawa, F., & Honiden, S. (2018). Falsification of cyber-physical systems with reinforcement learning. In 2018 IEEE Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS) (pp. 5–6). Piscataway: IEEE.CrossRef
93.
Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification (pp. 97–117). Berlin: Springer.CrossRef
94.
Koymans, R. (1990). Specifying real-time properties with metric temporal logic. Real-Time System, 2(4), 255–299.CrossRef
95.
Kurzhanski, A. B., & Varaiya, P. (2000). Ellipsoidal techniques for reachability analysis. In International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science (Vol. 1790, pp. 202–214). Berlin: Springer.
96.
Kushner, T., Bortz, D., Maahs, D., & Sankaranarayanan, S. (2018). A data-driven approach to artificial pancreas verification and synthesis. In International Conference on Cyber-Physical Systems (ICCPS’18). New York: IEEE Press.
97.
Labinaz, G., Bayoumi, M. M., & Rudie, K. (1997). A survey of modeling and control of hybrid systems. Annual Reviews in Control, 21, 79–92.CrossRef
98.
Lafferriere, G., Pappas, G. J., & Sastry, S. (2000). O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1), 1–21.MathSciNetMATHCrossRef
99.
Leitner, F., & Leue, S. (2008). Simulink design verifier vs. SPIN a comparative case study. In Proceedings of the 13th International Workshop on Formal Methods for Industrial Critical Systems.
100.
Levinson, J., Askeland, J., Becker, J., Dolson, J., Held, D., Kammel, S., et al. (2011). Towards fully autonomous driving: Systems and algorithms. In 2011 IEEE Intelligent Vehicles Symposium (IV) (pp. 163–168). Piscataway: IEEE.CrossRef
101.
102.
Loos, S. M., Platzer, A., & Nistor, L. (2011). Adaptive cruise control: Hybrid, distributed, and now formally verified. In International Symposium on Formal Methods (pp. 42–56). Berlin: Springer.
103.
Maahs, D. M., Calhoun, P., Buckingham, B. A., Chase, H. P., Hramiak, I., Lum, J., et al. (2014). A randomized trial of a home system to reduce nocturnal hypoglycemia in type 1 diabetes. Diabetes Care, 37(7), 1885–1891.CrossRef
104.
Magdici, S., & Althoff, M. (2017). Adaptive cruise control with safety guarantees for autonomous vehicles. IFAC-PapersOnLine, 50(1), 5774–5781.CrossRef
105.
Makino, K., & Berz, M. (2003). Taylor models and other validated functional inclusion methods. Journal of Pure and Applied Mathematics, 4(4), 379–456.MathSciNetMATH
106.
Maler, O., & Nickovic, D. (2004). Monitoring temporal properties of continuous signals. In Proceedings of Formal Modeling and Analysis of Timed Systems (pp. 152–166). Berlin: Springer.MATH
107.
108.
Mitchell, I., & Tomlin, C. (2000). Level set methods for computation in hybrid systems. In International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science (Vol. 1790, pp. 310–323). Berlin: Springer.
109.
Mover, S., Cimatti, A., Tiwari, A., & Tonetta, S. (2013). Time-aware relational abstractions for hybrid systems. In Proceedings of the Eleventh ACM International Conference on Embedded Software (EMSOFT ’13) (pp. 14:1–14:10). Piscataway: IEEE Press.
110.
111.
Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., & Pappas, G.J. (2010). Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In Proceedings of Hybrid Systems: Computation and Control (pp. 211–220). New York: ACM.MATH
112.
Nguyen, L. V., Kapinski, J., Jin, X., Deshmukh, J. V., & Johnson, T. T. (2017). Hyperproperties of real-valued signals. In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (pp. 104–113). New York: ACM.
113.
Nicolescu, G., & Mosterman, P. J. (2009). Model-based design for embedded systems (1st ed.). Boca Raton: CRC Press.CrossRef
114.
Nilsson, P., Hussien, O., Chen, Y., Balkan, A., Rungger, M., Ames, A., et al. (2014). Preliminary results on correct-by-construction control software synthesis for adaptive cruise control. In 2014 IEEE 53rd Annual Conference on Decision and Control (CDC) (pp. 816–823). Piscataway: IEEE.
115.
Norris, J. (1998). Markov chains. Cambridge: Cambridge University Press.MATH
116.
Øksendal, B. K. (2000). Stochastic differential equations: An introduction. Berlin: Springer.MATH
117.
Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J., & Lee, I. (2014). Model-driven safety analysis of closed-loop medical systems. IEEE Transactions on Industrial Informatics, 10(1), 3–16.CrossRef
118.
Papachristodoulou, A., & Prajna, S. (2005). Analysis of non-polynomial systems using the sum of squares decomposition. In Positive Polynomials in Control (pp. 23–43). Berlin: Springer.CrossRef
119.
Pei, Y., Entcheva, E., Grosu, R., & Smolka, S. (2005) Efficient modeling of excitable cells using hybrid automata. In Proceedings of the Computational Methods in Systems Biology (pp. 216–227).
120.
121.
Platzer, A. (2010). Logical analysis of hybrid systems: Proving theorems for complex dynamics. Heidelberg: Springer. https://​doi.​org/​10.​1007/​978-3-642-14509-4MATHCrossRef
122.
Platzer, A., & Clarke, E. M. (2008). Computing differential invariants of hybrid systems as fixedpoints. In A. Gupta & S. Malik (Eds.), Proceedings of computer aided verification. Lecture Notes in Computer Science (Vol. 5123, pp. 176–189). Berlin: Springer.
123.
Pnueli, A. (1977). The temporal logic of programs. In Proceedings of Symposium on Foundations of Computer Science (pp. 46–57). Piscataway: IEEE.
124.
Podelski, A., & Wagner, S. (2007). Region stability proofs for hybrid systems (pp. 320–335). Berlin: Springer.MATH
125.
Prabhakar, P., Duggirala, P. S., Mitra, S., & Viswanathan, M. (2013). Hybrid automata-based CEGAR for rectangular hybrid systems. In R. Giacobazzi, J. Berdine, I. Mastroeni (Eds.), Verification, model checking, and abstract interpretation (pp. 48–67). Berlin: Springer.CrossRef
126.
Prajna, S. (2005). Optimization-based methods for nonlinear and hybrid systems verification. Ph.D. thesis, California Institute of Technology, Caltech, Pasadena, CA, USA.
127.
Prajna, S., & Jadbabaie, A. (2004). Safety verification of hybrid systems using barrier certificates. In Hybrid Systems: Computation and Control (pp. 477–492). Berlin: Springer.MATHCrossRef
128.
Pulina, L., & Tacchella, A. (2012). Challenging smt solvers to verify neural networks. AI Communications, 25(2), 117–135.MathSciNetMATH
129.
Ratschan, S., & She, Z. (2005). Safety verification of hybrid systems by constraint propagation based abstraction refinement. In International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science (Vol. 3414, pp. 573–589). Berlin: Springer.
130.
131.
132.
Roohi, N., Prabhakar, P., & Viswanathan, M. (2016). Hybridization based CEGAR for hybrid automata with affine dynamics. In M. Chechik, & J. F. Raskin (Eds.), Tools and algorithms for the construction and analysis of systems (pp. 752–769). Berlin: Springer.CrossRef
133.
134.
Sankaranarayanan, S., & Fainekos, G. E. (2012). Falsification of temporal properties of hybrid systems using the cross-entropy method. In ACM International Conference on Hybrid Systems: Computation and Control (pp. 125–134 ). New York: ACM.MATH
135.
Sankaranarayanan, S., Kumar, S. A., Cameron, F., Bequette, B. W., Fainekos, G., & Maahs, D. M. (2017). Model-based falsification of an artificial pancreas control system. ACM SIGBED Review, 14(2), 24–33.CrossRef
136.
Sankaranarayanan, S., & Tiwari, A. (2011). Relational abstractions for continuous and hybrid systems. In International Conference on Computer Aided Verification. Lecture Notes in Computer Science (Vol. 6806, pp. 686–702). Berlin: Springer.
137.
Siper, M. J. (2005). An Introduction to mathematical theory of computation (2nd ed.). Toronto: Thompson Publishing (Course Technology)
138.
Skyler, J. S. (Ed.). (2012). Atlas of diabetes (4th ed.). Berlin: Springer.
139.
Sontag, E. D. (1981). Nonlinear regulation: The piecewise linear approach. IEEE Transactions on Automatic Control, 26(2), 346–358.MathSciNetMATHCrossRef
140.
Steil, G., Panteleon, A., & Rebrin, K. (2004). Closed-sloop insulin delivery—the path to physiological glucose control. Advanced Drug Delivery Reviews, 56(2), 125–144.CrossRef
141.
Steil, G. M. (2013). Algorithms for a closed-loop artificial pancreas: The case for proportional-integral-derivative control. Journal of Diabetes Science and Technology, 7, 1621–1631.CrossRef
142.
Sutton, R. S., & Barto, A. G. (1998). Reinforcement learning: An introduction (Vol. 1). Cambridge: MIT Press.MATH
143.
Teixeira, R. E., & Malin, S. (2008). The next generation of artificial pancreas control algorithms. Journal of Diabetes Science and Technology, 2, 105–112.CrossRef
144.
145.
Topcu, U., & Packard, A. (2009). Stability region analysis for uncertain nonlinear systems. IEEE Transactions on Automatic Control, 54, 1042–1047.MathSciNetMATHCrossRef
146.
Topcu, U., Seiler, P., & Packard, A. (2008). Local stability analysis using simulations and sum-of-squares programming. Automatica, 44, 2669–2675.MathSciNetMATHCrossRef
147.
Tuncali, C. E., Fainekos, G., Ito, H., & Kapinski, J. (2018). Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In Proceedings of IEEE Intelligent Vehicles Symposium (IV)
148.
Tuncali, C. E., Kapinski, J., Ito, H., & Deshmukh, J. V. (2018). Reasoning about safety of learning-enabled components in autonomous cyber-physical systems. In Proceedings of the 55th Annual Design Automation Conference, DAC 2018 (pp. 30:1–30:6). New York: ACM.
149.
Ulus, D. (2017). Montre: A tool for monitoring timed regular expressions. In Proceedings of the International Conference on Computer Aided Verification (pp. 329–335). Berlin: Springer.CrossRef
150.
Ulus, D., Ferrère, T., Asarin, E., & Maler, O. (2014). Timed pattern matching. In Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems (pp. 222–236). Berlin: Springer.MATH
151.
Zutshi, A., Sankaranarayanan, S., Deshmukh, J., & Jin, X. (2016). Symbolic-numeric reachability analysis of closed-loop control software. In Hybrid Systems: Computation and Control (HSCC) (pp. 135–144). New York: ACM Press.MATH
152.
Zutshi, A., Sankaranarayanan, S., Deshmukh, J., & Kapinski, J. (2013). A trajectory splicing approach to concretizing counterexamples for hybrid systems. In IEEE Conference on Decision and Control (CDC) (pp. 3918–3925). New York: IEEE Press.CrossRef
153.
Zutshi, A., Sankaranarayanan, S., Deshmukh, J., & Kapinski, J. (2014). Multiple-shooting CEGAR-based falsification for hybrid systems. In International Conference on Embedded Software (EMSOFT) (pp. 5:1–5:10). New York: ACM Press.
154.
Zutshi A., Sankaranarayanan S., & Tiwari A. (2012). Timed relational abstractions for sampled data control systems. In P. Madhusudan & S. A. Seshia (Eds.), Computer Aided Verification. Lecture Notes in Computer Science (Vol. 7358). Berlin: Springer.
Metadaten
Titel
Formal Techniques for Verification and Testing of Cyber-Physical Systems
verfasst von
Jyotirmoy V. Deshmukh
Sriram Sankaranarayanan
Copyright-Jahr
2019
Buch
Design Automation of Cyber-Physical Systems

Print ISBN: 978-3-030-13049-7

Electronic ISBN: 978-3-030-13050-3

Copyright-Jahr: 2019

DOI
https://doi.org/10.1007/978-3-030-13050-3_4

Neuer Inhalt

    Bildnachweise