maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2021-4-326-336mais-1563Research ArticleTheory of ComputingЗамечания о последних достижениях в доказательстве устойчивости с использованием KeYmaeraXNotes on Recent Achievements in Proving Stability using KeYmaeraXhttps://orcid.org/0000-0002-8443-1558БаарТомасBaarThomasthomas.baar@htw-berlin.dehttps://orcid.org/0000-0001-5851-3616ШультеХорстSchulteHorsthorst.schulte@htw-berlin.deУниверситет прикладных технических и экономических наук г. БерлинаГерманияHTW BerlinGermany202118122021284326336Copyright © Баар Т., Шульте Х., 20212021Баар Т., Шульте Х.Baar T., Schulte H.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1563

KeYmaeraX -- это доказательство теорем в стиле Хоара для гибридных систем. Гибридную систему можно рассматривать как совокупность дискретных, так и непрерывных переменных, значения которых могут изменяться резко или непрерывно соответственно. KeYmaeraX поддерживает только переменные, имеющие примитивный тип bool или real. Благодаря сочетанию дискретных и непрерывных элементов системы, одной из перспективных областей применения KeYmaeraX являются системы управления с замкнутым контуром. Система управления с замкнутым контуром состоит из установки и контроллера. В то время как установка в основном представляет собой совокупность непрерывных переменных, значения которых меняются со временем в соответствии с физическими законами, контроллер можно рассматривать как алгоритм, сформулированный на классическом языке программирования. В этой статье мы рассмотрим некоторые недавние расширения исчисления доказательств, применяемые KeY\\-maeraX, которые делают формальные доказательства устойчивости динамических систем более выполнимыми. Основываясь на примере, мы сначала познакомимся с темой и докажем асимптотическую устойчивость данной системы.

KeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability.

киберфизическая систематеория управленияфункция Ляпуноваимперативный язык программированияcyber physical systemcontrol theorylyapunov functionimperative programming languageReferencesP. Baudin et al., “The dogged pursuit of bug-free C programs: the Frama-C software analysis platform,” Communications of the ACM (CACM), vol. 64, no. 8, pp. 56-68, Aug. 2021.P. Baudin et al., “The dogged pursuit of bug-free C programs: the Frama-C software analysis platform,” Communications of the ACM (CACM), vol. 64, no. 8, pp. 56-68, Aug. 2021.C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Commun. ACM, vol. 12, no. 10, pp. 576-580, 1969.C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Commun. ACM, vol. 12, no. 10, pp. 576-580, 1969.A. Platzer, Logical Foundations of Cyber-Physical Systems. Springer, 2018.A. Platzer, Logical Foundations of Cyber-Physical Systems. Springer, 2018.J.-D. Quesel, S. Mitsch, S. Loos, N. Ar'echiga, and A. Platzer, “How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety,” STTT, vol. 18, no. 1, pp. 67-91, 2016, doi: 10.1007/s10009-015-0367-0.J.-D. Quesel, S. Mitsch, S. Loos, N. Ar'echiga, and A. Platzer, “How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety,” STTT, vol. 18, no. 1, pp. 67-91, 2016, doi: 10.1007/s10009-015-0367-0.T. Baar and S. Staroletov, “A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier,” Modeling and Analysis of Information Systems. 2018;25(5), pp. 465-480, 2018.T. Baar and S. Staroletov, “A Control Flow Graph Based Approach to Make the Verification of Cyber-Physical Systems Using KeYmaera Easier,” Modeling and Analysis of Information Systems. 2018;25(5), pp. 465-480, 2018.T. Baar, “A Metamodel-Based Approach for Adding Modularization to KeYmaera's Input Syntax,” in PSI, Novosibirsk, 2019, pp. 125-139, doi: 10.1007/978-3-030-37487-7_11.T. Baar, “A Metamodel-Based Approach for Adding Modularization to KeYmaera's Input Syntax,” in PSI, Novosibirsk, 2019, pp. 125-139, doi: 10.1007/978-3-030-37487-7_11.A. Liapounoff, “Problème général de la stabilité du mouvement,” Annales de la faculté des sciences de Toulouse, vol. 9, no. 2, pp. 203-474, 1907, [Online]. Available: http://www.numdam.org/item?id=AFST_1907_2_9__203_0.A. Liapounoff, “Problème général de la stabilité du mouvement,” Annales de la faculté des sciences de Toulouse, vol. 9, no. 2, pp. 203-474, 1907, [Online]. Available: http://www.numdam.org/item?id=AFST_1907_2_9__203_0.A. M. Lyapunov, “The general problem of the stability of motion,” International Journal of Control, vol. 55, no. 3, pp. 531-773, 1992.A. M. Lyapunov, “The general problem of the stability of motion,” International Journal of Control, vol. 55, no. 3, pp. 531-773, 1992.D. Liberzon, Switching in Systems and Control. Birkh"auser, 2003.D. Liberzon, Switching in Systems and Control. Birkh"auser, 2003.R. E. Kalman, “On the general theory of control systems,” in Proc. 1st World Congress of the International Federation of Automatic Control, 1960, pp. 481-493.R. E. Kalman, “On the general theory of control systems,” in Proc. 1st World Congress of the International Federation of Automatic Control, 1960, pp. 481-493.V. I. Arnol'd, Gew"ohnliche Differentialgleichungen. Springer-Verlag, 1979.V. I. Arnol'd, Gew"ohnliche Differentialgleichungen. Springer-Verlag, 1979.J. L. Salle and S. Lefschetz, Die Stabilit"atstheorie von Ljapunov. Mannheim: BI Hochschultaschenb"ucher, 1974.J. L. Salle and S. Lefschetz, Die Stabilit"atstheorie von Ljapunov. Mannheim: BI Hochschultaschenb"ucher, 1974.Y. K. Tan and A. Platzer, “Deductive Stability Proofs for Ordinary Differential Equations,” in Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, 2021, vol. 12652, pp. 181-199, doi: 10.1007/978-3-030-72013-1_10.Y. K. Tan and A. Platzer, “Deductive Stability Proofs for Ordinary Differential Equations,” in Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, 2021, vol. 12652, pp. 181-199, doi: 10.1007/978-3-030-72013-1_10.Y. K. Tan and A. Platzer, “Switched Systems as Hybrid Programs,” in 7th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2021, Brussels, Belgium, July 7-9, 2021, 2021, vol. 54, no. 5, pp. 247-252, doi: 10.1016/j.ifacol.2021.08.506.Y. K. Tan and A. Platzer, “Switched Systems as Hybrid Programs,” in 7th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2021, Brussels, Belgium, July 7-9, 2021, 2021, vol. 54, no. 5, pp. 247-252, doi: 10.1016/j.ifacol.2021.08.506.U. Topcu, A. K. Packard, and P. J. Seiler, “Local stability analysis using simulations and sum-of-squares programming,” Autom., vol. 44, no. 10, pp. 2669-2675, 2008, doi: 10.1016/j.automatica.2008.03.010.U. Topcu, A. K. Packard, and P. J. Seiler, “Local stability analysis using simulations and sum-of-squares programming,” Autom., vol. 44, no. 10, pp. 2669-2675, 2008, doi: 10.1016/j.automatica.2008.03.010.M. Anghel, F. Milano, and A. Papachristodoulou, “Algorithmic Construction of Lyapunov Functions for Power System Stability Analysis,” IEEE Trans. Circuits Syst. I Regul. Pap., vol. 60-I, no. 9, pp. 2533-2546, 2013, doi: 10.1109/TCSI.2013.2246233.M. Anghel, F. Milano, and A. Papachristodoulou, “Algorithmic Construction of Lyapunov Functions for Power System Stability Analysis,” IEEE Trans. Circuits Syst. I Regul. Pap., vol. 60-I, no. 9, pp. 2533-2546, 2013, doi: 10.1109/TCSI.2013.2246233.K. Forsman, “Construction of Lyapunov functions using Grobner bases,” in Proceedings of the 30th IEEE Conference on Decision and Control, 1991, pp. 798-799, doi: 10.1109/CDC.1991.261424.K. Forsman, “Construction of Lyapunov functions using Grobner bases,” in Proceedings of the 30th IEEE Conference on Decision and Control, 1991, pp. 798-799, doi: 10.1109/CDC.1991.261424.J. Liu, N. Zhan, and H. Zhao, “Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems,” Math. Comput. Sci., vol. 6, no. 4, pp. 395-408, 2012, doi: 10.1007/s11786-012-0133-6.J. Liu, N. Zhan, and H. Zhao, “Automatically Discovering Relaxed Lyapunov Functions for Polynomial Dynamical Systems,” Math. Comput. Sci., vol. 6, no. 4, pp. 395-408, 2012, doi: 10.1007/s11786-012-0133-6.S. Sankaranarayanan, H. B. Sipma, and Z. Manna, “Constructing invariants for hybrid systems,” in International Workshop on Hybrid Systems: Computation and Control, 2004, pp. 539-554.S. Sankaranarayanan, H. B. Sipma, and Z. Manna, “Constructing invariants for hybrid systems,” in International Workshop on Hybrid Systems: Computation and Control, 2004, pp. 539-554.M. S. Branicky, “Multiple Lyapunov functions and other analysis tools for switched and hybrid systems,” IEEE Trans. Autom. Control., vol. 43, no. 4, pp. 475-482, 1998, doi: 10.1109/9.664150.M. S. Branicky, “Multiple Lyapunov functions and other analysis tools for switched and hybrid systems,” IEEE Trans. Autom. Control., vol. 43, no. 4, pp. 475-482, 1998, doi: 10.1109/9.664150.Z. Sun and S. S. Ge, Stability Theory of Switched Dynamical Systems. Springer, Communications and Control Engineering, 2011.Z. Sun and S. S. Ge, Stability Theory of Switched Dynamical Systems. Springer, Communications and Control Engineering, 2011.A. Podelski and S. Wagner, “Model Checking of Hybrid Systems: From Reachability Towards Stability,” in Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, 2006, vol. 3927, pp. 507-521, doi: 10.1007/11730637_38.A. Podelski and S. Wagner, “Model Checking of Hybrid Systems: From Reachability Towards Stability,” in Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, 2006, vol. 3927, pp. 507-521, doi: 10.1007/11730637_38.

The authors declare that there are no conflicts of interest present.