Formal Stability Analysis of Control Systems

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, paperand- 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-orderlogic 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.