Formal Analysis of Power Electronics Circuits using Theorem Proving

Abstract

Power electronics systems are extensively used in many engineering systems, such as hand-held devices, medical equipment, electric vehicles, aerospace artifacts, power grids, nuclear power plants and military equipment. Power

electronics are characterized by the highly-nonlinear behavior due to the in- volvement of semiconductor switches for power conversion. Mathematical

concepts of basic circuit theory, operational calculus, differential theory, in- tegration theory and control theory are involved in modeling their behavior.

Traditionally, paper-and-pencil proof methods and computer-based simula- tions are used to perform the analysis and design of power electronics sys- tems. However, these traditional analysis techniques suffer from several lim- itations, such as human-error, discretization and truncation errors, and thus

cannot guarantee an accurate analysis and verification of power electronics circuits. Whereas, accurate analysis and design of power electronic circuits is mandatory for the safety and mission-critical engineering applications, such as medical equipment, transportation and smart grids. To overcome the

shortcomings of the traditional analysis techniques, we propose a higher- order-logic theorem proving based framework to formally analyze and verify

power electronic systems accurately and exhaustively. Higher-order logic is highly expressive and allows modeling complex system behaviors, whereas, the soundness of theorem provers ensure accurate analysis and verification of the systems.

The proposed framework, mainly, enables time and complex-domain anal- i

ysis and design of power electronics systems within the HOL Light theorem prover. The formalization in the time-domain paradigm allows to perform formal periodic steady-state analysis and design of the ideal and non-ideal equivalent circuits of power electronics circuits. In this regard, we propose: (i) formal modeling of ideal and non-ideal behavior of the circuit elements

(ii) formal modeling of basic circuit theory notions, such as switching func- tion technique (iii) formally verified results for the integration and differen- tiation of piecewise functions (iv) formal modeling of differential equations

(v) formally verified results for the solutions of the differential equations (vi) formal modeling of steady-state characteristics and design parameters. To illustrate the usefulness of the proposed formalizations, they are used to formally analyze the time-domain based periodic steady-state analysis of ideal and non-ideal DC-DC Buck converters.

Formalization in the complex-domain is aimed at formally analyzing sta- bility of the control systems in power electronics systems to control the flow

of energy from input to output. Our main contributions in complex-domain analysis are: (i) formal modeling of stability criterion (ii) formally verified results of factorization of characteristic polynomials upto the fourth-order

(iii) formally verified results for the stability of the characteristic polyno- mials. The proposed formalization allows to formally specify and verify the

stability analysis of control systems based on the characteristic polynomials

which are obtained from the transfer function of the system in complex- domain. To illustrate the practical effectiveness, we formally verify the sta- bility of controllers in smart grids for efficient energy processing from wind

turbines.