nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Verifying Band Convergence for Sampled Control Systems

verfasst von : P. Ezudheen, Zahra Rahimi Afzal, Pavithra Prabhakar, Deepak D’Souza, Meenakshi D’Souza

Erschienen in: NASA Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We present a method to verify transient and settling time properties, called band convergence properties, of digitally controlled continuous systems, wherein we consider a linear dynamical system model for a plant and a PID controller. We consider the discrete-time sampled behavior of the closed loop system, and verify band convergence for the discrete-time behavior. The basic idea is to look for a box-shaped invariant for the system which is adequate to ensure that the system stays within the given band. We first give a technique to handle a general discrete-time system, but with determinate matrix entries. We then give a technique to handle discrete-time systems with matrices that lie in a range which over-approximate the matrix exponentials (which arise when we consider the discrete-time version of a continuous system), using the notion of an abstract discrete-time system. We have implemented the verification approach, and evaluate its efficacy on some popular Simulink models.

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

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

Vorheriges Kapitel Model Checking Timed Hyperproperties in Discrete-Time Systems

Nächstes Kapitel Heterogeneous Verification of an Autonomous Curiosity Rover

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12CrossRefMATH

Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 92–106. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33386-6_9CrossRefMATH

Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRef

Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Meth. Syst. Des. 51(1), 5–30 (2017). https://doi.org/10.1007/s10703-017-0286-7CrossRefMATH

Prabhakar, P., Lal, R., Kapinski, J.: Automatic trace generation for signal temporal logic. In: Proceedings of the IEEE Real-Time Systems Symposium (RTSS), Nashville, USA, December 2018, pp. 208–217. IEEE Computer Society (2018)

Roehm, H., Oehlerking, J., Heinz, T., Althoff, M.: STL model checking of continuous and hybrid systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 412–427. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_26CrossRefMATH

Moler, C., Van Loan, C.: Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM Rev. 45(1), 3–49 (2003)MathSciNetCrossRef

Control Tutorials for MATLAB and Simulink. http://ctms.engin.umich.edu/CTMS/

Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Automat. Contr. 55(12), 2834–2840 (2010)MathSciNetCrossRef

10.

Yordanov, B., Tumova, J., Cerna, I., Barnat, J., Belta, C.: Temporal logic control of discrete-time piecewise affine systems. IEEE Trans. Automat. Contr. 57(6), 1491–1504 (2012)MathSciNetCrossRef

11.

Blondel, V.D., Tsitsiklis, J.N.: Complexity of stability and controllability of elementary hybrid systems. Automatica 35(3), 479–489 (1999)MathSciNetCrossRef

12.

Blondel, V.D., Bournez, O., Koiran, P., Tsitsiklis, J.N.: The stability of saturated linear dynamical systems is undecidable. J. Comput. Syst. Sci. 62(3), 442–462 (2001)MathSciNetCrossRef

13.

Branicky, M.S.: Multiple Lyapunov functions and other analysis tools for switched and hybrid systems. IEEE Trans. Automat. Contr. 43(4), 3–17 (1998)MathSciNetCrossRef

14.

Davrazos, G., Koussoulas, N.T.: A review of stability results for switched and hybrid systems. In: Proceedings of the Mediterranean Conference on Control (2001)

15.

Lin, H., Antsaklis, P.J.: Stability and stabilizability of switched linear systems: a survey of recent results. IEEE Trans. Automat. Contr. 54(2), 308–322 (2009)MathSciNetCrossRef

16.

Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: Proceedings of the IEEE/ACM Conference on Cyber-Physical Systems (ICCPS), Chicago, USA, April 2011, pp. 22–31. IEEE Computer Society (2011)

17.

Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Proceedings of the 15th Conference on Hybrid Systems: Computation and Control (HSCC), Beijing, China, April 2012, pp. 115–124. ACM (2012)

18.

Prabhakar, P., Garcia Soto, M.: Abstraction based model-checking of stability of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 280–295. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_20CrossRef

19.

Prabhakar, P., Soto, M.G.: Counterexample guided abstraction refinement for stability analysis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 495–512. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_27CrossRef

20.

Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 507–521. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_38CrossRefMATH

21.

Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 320–335. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75454-1_23CrossRefMATH

22.

Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 750–753. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71493-4_76CrossRef

23.

Zutshi, A., Sankaranarayanan, S., Tiwari, A.: Timed relational abstractions for sampled data control systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 343–361. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_27CrossRef

24.

Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686–702. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_56CrossRef

25.

Rushby, J., Lincoln, P., Owre, S., Shankar, N., Tiwari, A.: Symbolic Analysis Laboratory (SAL), SRI, California. http://www.csl.sri.com/projects/sal/

26.

Bessa, I., Ismail, H., Palhares, R.M., Cordeiro, L.C., Filho, J.E.C.: Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Trans. Comput. 66(3), 545–552 (2017)MathSciNetCrossRef

27.

Lal, R., Prabhakar, P.: Bounded error flowpipe computation of parameterized linear systems. In: 13th International Conference on Embedded Software (EMSOFT) (2015)

28.

Lal, R., Prabhakar, P.: Safety analysis using compositional bounded error approximations of communicating hybrid systems. In: Proceedings of the 56th IEEE Conference on Decision and Control (CDC) (2017)

29.

Lal, R., Prabhakar, P.: Compositional construction of bounded error over-approximations of acyclic interconnected continuous dynamical systems. In: Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2019, La Jolla, CA, USA, 9–11 October 2019, pp. 12:1–12:5 (2019)

30.

Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15CrossRef

31.

Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14CrossRef

Titel: Verifying Band Convergence for Sampled Control Systems
verfasst von: P. Ezudheen
Zahra Rahimi Afzal
Pavithra Prabhakar
Deepak D’Souza
Meenakshi D’Souza
Verlag: Springer International Publishing
Buch: NASA Formal Methods
Print ISBN: 978-3-030-55753-9

Electronic ISBN: 978-3-030-55754-6

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-55754-6_19

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"