Formal Analysis of Steady State Error in Feedback Control Systems

Abstract

The meticulousness of safety critical control system design has always been of vital signi cance as even a tri ing glitch in the design analysis may result in grievous penalties, even in the loss of human life. To ensure the correctness of the system, traditionally it based on paper and pencil proofs. With the beginning of the modern age, simulations and computer algebra systems were employed to ensure the correctness of design. However, the said techniques compromise the accuracy of the analysis and thus are not a viable option for the analysis of safety critical systems. Over the years Formal Veri cation has emerged as one of the most viable option for the veri cation of hardware and software systems. It combines the strong paper and pencil mathematics along with modern computer aided tool to ensure correctness. Since the new formal model must satisfy the existing mathematical reasoning, therefore the chance to catch critical design errors increases which are often ignored otherwise. This thesis makes use of formal methods to establish a higher- order logic based framework to reason about the correctness of safety critical control systems. In particular, we rst provide a generic platform to express a wide variety of control systems in terms of their formal model. We identi ed the least basic blocks which can be arranged in various topologies to express a wide range of systems. We then provide theorems which can be used to reason v vi various properties of these systems. Moreover, a generic expression for the steady-state error of unity-feedback control systems using the multivariate analysis theories of HOL-Light has been veri ed. The unique feature of this expression is that it can be used to reason about the steady-state error of any system type and input. Moreover, it facilitates reusability when reasoning about the state-state error of the same system while considering di erent inputs. The quest for minimizing the user interaction in the higher-order- logic theorem-proving based analysis for steady-state errors led us to develop this useful relationship, which to the best of our knowledge has not been reported in the control systems literature before. In order to illustrate the utilization and practical e ectiveness of the formalization for verifying real- world control systems, two case studied have been conducted. The steady- state error analysis of the Pulse Width Modulation (PWM) push-pull DC- DC converters, which is used in power electronics and many safety-critical aerospace applications and the steady-state error analysis of a Solar Tacking control systems developed for aerospace applications.