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 l^2 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.
","abstract_html":"<p>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 l^2 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.</p>","abstract_has_math":false,"creators":["Wang, Xuan"],"institution":"Brigham Young University - Provo","degree_name":"MS","degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T01:28:12Z","subjects":["small gain theorem","digital controller implementation","software verification","controller uncertainty","Computer Sciences"],"languages":["English"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://scholarsarchive.byu.edu/etd/681","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Wang, Xuan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2005-11-10T08:00:00Z"]},{"key":"dc:publisher","label":"Institution","values":["Brigham Young University - Provo"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["MS"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["small gain theorem","digital controller implementation","software verification","controller uncertainty","Computer Sciences"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://scholarsarchive.byu.edu/etd/681","https://scholarsarchive.byu.edu/context/etd/article/1680/viewcontent/ETD_CISOPTR_501.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Physical and Mathematical Sciences; Computer Science"]},{"key":"dc:description.abstract","label":"Abstract","values":["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 l^2 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.
"]},{"key":"dc:format","label":"Dc Format","values":["application:pdf"]},{"key":"dc:source","label":"Dc Source","values":["Brigham Young University - Provo"]},{"key":"dc:title","label":"Title","values":["Verification of Digital Controller Verifications"]}]}],"canonical_facts":{"dc:creator":["Wang, Xuan"],"dc:date":["2005-11-10T08:00:00Z"],"dc:description":["Physical and Mathematical Sciences; Computer Science"],"dc:description.abstract":["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 l^2 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.
"],"dc:format":["application:pdf"],"dc:identifier":["https://scholarsarchive.byu.edu/etd/681","https://scholarsarchive.byu.edu/context/etd/article/1680/viewcontent/ETD_CISOPTR_501.pdf"],"dc:language":["English"],"dc:publisher":["Brigham Young University - Provo"],"dc:source":["Brigham Young University - Provo"],"dc:subject":["small gain theorem","digital controller implementation","software verification","controller uncertainty","Computer Sciences"],"dc:title":["Verification of Digital Controller Verifications"],"dc:type":["Thesis"],"thesis:degree_name":["MS"]},"updated_at":"2026-07-24T01:28:12Z"}