Verification of Digital Controller Verifications Verification of Digital Controller Verifications

by Wang, Xuan 1967-

This thesis presents an analysis framework to verify the stablility property of a closed-loop control system with a software controller implementation. The usual approach to verifying stability for software uses experiments which are costly and can be dangerous. More recently, mathematical models of software have been proposed which can be used to reason about the correctness of controllers. However, these mathematical models ignore computational details that may be important in verification. We propose a method to determine the instability of a closed-loop system with a software controller implementation under l2 inputs using simulation. This method avoids the cost of experimentation and the loss of precision inherent in mathematical modeling. The method uses the small gain theorem to compute a lower bound on the 2-induced norm of the uncertainty in the software implementation; if the lower bound is greater than 1/(2-induced norm of G), where G is the feedback system consisting of the mathematical model of the plant and the mathematical model of the controller, the closed-loop system is unsafe in a certain sense. The resulting method can not determine if the closed-loop system is stable, but can only suggest instability.