Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


thesis.pdf (810.54 KB)

ETD Abstract Container

Abstract Header

Provable Run Time Safety Assurance for a Non-Linear System

Snyder, Cory Firmin
http://rave.ohiolink.edu/etdc/view?acc_num=wright1369443661

Abstract Details

2013, Master of Science in Engineering (MSEgr), Wright State University, Electrical Engineering.
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.
Kuldip Rattan, Ph.D. (Advisor)
Matthew Clark, M.S.Egr. (Committee Member)
Xiaodong Zhang, Ph.D. (Committee Member)
94 p.
Computer Science; Electrical Engineering; Engineering
reachable sets; non-linear system; hybrid automata; PHAVer; SpaceEx; safety assurance; verification; run time assurance

Recommended Citations

Citations

  • Snyder, C. F. (2013). Provable Run Time Safety Assurance for a Non-Linear System [Master's thesis, Wright State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=wright1369443661

    APA Style (7th edition)

  • Snyder, Cory. Provable Run Time Safety Assurance for a Non-Linear System. 2013. Wright State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=wright1369443661.

    MLA Style (8th edition)

  • Snyder, Cory. "Provable Run Time Safety Assurance for a Non-Linear System." Master's thesis, Wright State University, 2013. http://rave.ohiolink.edu/etdc/view?acc_num=wright1369443661

    Chicago Manual of Style (17th edition)

wright1369443661
423
© 2013, some rights reserved.Creative Commons License Provable Run Time Safety Assurance for a Non-Linear System by Cory Firmin Snyder is licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License. Based on a work at etd.ohiolink.edu.
This open access ETD is published by Wright State University and OhioLINK.