Publication Date
2013
Document Type
Thesis
Committee Members
Matthew Clark (Committee Member), Kuldip Rattan (Advisor), Xiaodong Zhang (Committee Member)
Degree Name
Master of Science in Engineering (MSEgr)
Abstract
Systems that are modeled by non-linear continuous-time differential equations with uncertain parameters have proven to be exceptionally difficult to formally verify. The past few decades have produced a number of useful verification tools which can be applied to such systems but each is applicable to only a subset of possible verification scenarios. The Level Sets Toolbox (LST) is one such tool which is directly applicable to non-linear systems, however, it is limited to systems of relatively small continuous state space dimension. Other tools such as PHAVer and the SpaceEx invariant of the Le Guernic-Girard (LGG) support function algorithm are specifically designed for hybrid systems with linear dynamics and linear constraints but can accommodate hundreds of continuous states. The application of these linear reachability tools to non-linear models has been achieved by approximating non-linear systems as linear hybrid automata (LHA). Unfortunately, the practical applicability and limitations of this approach are not yet well documented. The purpose of this thesis is to evaluate the performance and dimensionality limitations of PHAVer and the LGG support function algorithm when applied to a LHA approximation of a particular non-linear system. A collision avoidance scenario with autonomous differential drive robots is used as a case study to demonstrate that an over-approximated reachable set boundary can be generated and implemented as a run time safety assurance mechanism.
Page Count
94
Department or Program
Department of Electrical Engineering
Year Degree Awarded
2013
Copyright
Copyright 2013, some rights reserved. My ETD may be copied and distributed only for non-commercial purposes and may not be modified. All use must give me credit as the original author.
Creative Commons License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 License.
