Abstract
Stability of a control system ensures that its output is under control and thus is the most important characteristic of control systems. Stability is characterized by the roots of the characteristic equation of the given control system in the complex-domain. Traditionally, paper-and-pencil proof methods and computer-based tools are used to analyze the stability of control systems. However, paper-and-pencil proof methods are error prone due to the human involvement. Whereas, computer based tools cannot model the continuous behavior in its true form due to the involvement of computer arithmetic and the associated truncation errors. Therefore, these techniques do not provide an accurate and complete analysis, which is unfortunate given the safety-critical nature of control system applications. In this paper, we propose to overcome these limitations by using higher-order-logic theorem proving for the stability analysis of control systems. For this purpose, we present a higher-order-logic based formalization of stability and the roots of the quadratic, cubic and quartic complex polynomials. The proposed formalization is based on the complex number theory of the HOL-Light theorem prover. A distinguishing feature of this work is the automatic nature of the formal stability analysis, which makes it quite useful for the control engineers working in the industry who have very little expertise about formal methods. For illustration purposes, we present the stability analysis of power converter controllers used in smart grids.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ahmad, M., Hasan, O.: Formal verification of steady-state errors in unity-feedback control systems. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 1–15. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10702-8_1
Ahmed, A.: System Analysis and Verification (SAVe) Lab. http://save.seecs.nust.edu.pk/projects/fsacs/. Accessed 12 Sept 2018
Amin, S.M., Wollenberg, B.F.: Toward a smart grid: power delivery for the 21st century. IEEE Power Energ. Mag. 3(5), 34–41 (2005)
Dyke, P.: An Introduction to Laplace Transforms and Fourier Series. SUMS. Springer, London (2014). https://doi.org/10.1007/978-1-4471-6395-4
Ekanayake, J., Jenkins, N.: Comparison of the response of doubly fed and fixed-speed induction generator wind turbines to changes in network frequency. IEEE Trans. Energy Convers. 19(4), 800–802 (2004)
Giordano, V., et al.: Smart grid projects in Europe. JRC Ref Rep Sy 8. Publications Office of the European Union, Luxembourg (2011). https://doi.org/10.2790/32946
Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4
Harrison, J.: Theorem Proving with the Real Numbers. Springer, London (2012)
Hasan, O., Ahmad, M.: Formal analysis of steady state errors in feedback control systems using HOL-Light. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 1423–1426. EDA Consortium, San Jose (2013)
Heck, A., Heck, A.: Introduction to MAPLE. Springer, New York (1993). https://doi.org/10.1007/978-1-4684-0519-4
Hornik, T., Zhong, Q.C.: A current-control strategy for voltage-source inverters in microgrids based on H\(^\infty \) and repetitive control. IEEE Trans. Power Electron. 26(3), 943–952 (2011)
MathWorks: Control System Toolbox. https://ch.mathworks.com/products/control.html. Accessed 12 Sept 2018
MathWorks: Simulink. https://www.mathworks.com/products/simulink.html. Accessed 12 Sept 2018
Momoh, J.A.: Smart Grid: Fundamentals of Design and Analysis, vol. 63. Wiley, Hoboken (2012)
Nise, N.S.: Control Systems Engineering. Wiley, Hoboken (2007)
Rashid, A., Hasan, O.: Formal analysis of linear control systems using theorem proving. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 345–361. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_21
Rashid, A., Siddique, U., Hasan, O.: Formal verification of platoon control strategies. In: Johnsen, E.B., Schaefer, I. (eds.) SEFM 2018. LNCS, vol. 10886, pp. 223–238. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92970-5_14
Sanwal, M.U., Hasan, O.: Formally analyzing continuous aspects of cyber-physical systems modeled by homogeneous linear differential equations. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 132–146. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25141-7_10
Siddique, U., Aravantinos, V., Tahar, S.: Formal stability analysis of optical resonators. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 368–382. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_25
Skogestad, S., Postlethwaite, I.: Multivariable Feedback Control: Analysis and Design, vol. 2. Wiley, New York (2007)
Sourceforge: Maxima. http://maxima.sourceforge.net/. Accessed 12 Sept 2018
Spong, M.W., Hutchinson, S., Vidyasagar, M., et al.: Robot Modeling and Control, vol. 3. Wiley, New York (2006)
Stoorvogel, A.A.: The H\(^\infty \) Control Problem: A State Space Approach. Citeseer (1992)
Taqdees, S.H., Hasan, O.: Formalization of Laplace transform using the multivariable calculus theory of HOL-light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 744–758. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_50
Varaiya, P.: Smart cars on smart roads: problems of control. IEEE Trans. Autom. Control 38(2), 195–207 (1993)
Wellin, P.R., Gaylord, R.J., Kamin, S.N.: An Introduction to Programming with Mathematica®. Cambridge University Press, Cambridge (2005)
Zhong, Q.C., Hornik, T.: Control of Power Inverters in Renewable Energy and Smart Grid Integration, vol. 97. Wiley, Hoboken (2012)
Acknowledgments
This work is supported by ICT Fund UAE, fund number 21N206 at UAE University, Al Ain, United Arab Emirates.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ahmed, A., Hasan, O., Awwad, F. (2019). Formal Stability Analysis of Control Systems. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2018. Communications in Computer and Information Science, vol 1008. Springer, Cham. https://doi.org/10.1007/978-3-030-12988-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-12988-0_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12987-3
Online ISBN: 978-3-030-12988-0
eBook Packages: Computer ScienceComputer Science (R0)