Formal analysis of steady state errors in feedback control systems using HOL-light

The accuracy of control systems analysis is of paramount importance as even minor design flaws can lead to disastrous consequences in this domain. This paper provides a higher-order-logic theorem proving based framework for the formal analysis of steady state errors in feedback control systems. In particular, we present the formalization of control system foundations, like transfer functions, summing junctions, feedback loops and pickoff points, and steady state error models for the step, ramp and parabola cases. These foundations can be built upon to formally specify a wide range of feedback control systems in higher-order logic and reason about their steady state errors within the sound core of a theorem prover. The proposed formalization is based on the complex number theory of the HOL-Light theorem prover. For illustration purposes, we present the steady state error analysis of a solar tracking control system.