Citation
Braman, Julia Marie Badger (2009) Safety Verification and Failure Analysis of Goal-Based Hybrid Control Systems. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/3H42-BF56. https://resolver.caltech.edu/CaltechETD:etd-05292009-111937
Abstract
The success of complex autonomous robotic systems depends on the quality and correctness of their fault tolerant control systems. A goal-based approach to fault tolerant control, which is modeled after a software architecture developed at the Jet Propulsion Laboratory, uses networks of goals to control autonomous systems. The complex conditional branching of the control program makes safety verification necessary. Three novel verification methods are presented. In the first, goal networks are converted to linear hybrid automata via a bisimulation. The converted automata can then be verified against an unsafe set of conditions using an existing symbolic model checker such as PHAVer. Due to the complexity issues that result from this method, a design for verification software tool, the SBT Checker, was developed to create goal networks that have state-based transitions. Goal networks that have state-based transitions can be converted to hybrid automata whose locations' invariants contain all information necessary to determine the transitions between the locations. An original verification software called InVeriant can then be used to find unsafe locations of linear hybrid systems based on the locations’ invariants and rate conditions, which are compared to the unsafe set of conditions. The reachability of the unsafe locations depends only on the reachability of the states of the state variables constrained in the locations' invariants from those state variables' initial conditions. In cases where this reachability condition is not trivially true, the software efficiently searches for a path to the unsafe locations using properties of the system. The third verification method is the calculation of the failure probability of the verified hybrid control system due to state estimation uncertainty, which is extremely important in autonomous systems that rely heavily on the state estimates made from sensor measurements. Finally, two significant example goal network control programs, one for a complex rover and another for a proposed aerobot mission to Titan, a moon of Saturn, are verified using the three techniques presented.
Item Type: | Thesis (Dissertation (Ph.D.)) |
---|---|
Subject Keywords: | bisimulation; hybrid systems; model checking |
Degree Grantor: | California Institute of Technology |
Division: | Engineering and Applied Science |
Major Option: | Mechanical Engineering |
Minor Option: | Planetary Sciences |
Awards: | Centennial Prize for the Best Thesis in Mechanical Engineering, 2009. |
Thesis Availability: | Public (worldwide access) |
Research Advisor(s): |
|
Thesis Committee: |
|
Defense Date: | 27 May 2009 |
Non-Caltech Author Email: | jmbraman (AT) yahoo.com |
Record Number: | CaltechETD:etd-05292009-111937 |
Persistent URL: | https://resolver.caltech.edu/CaltechETD:etd-05292009-111937 |
DOI: | 10.7907/3H42-BF56 |
Default Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. |
ID Code: | 2271 |
Collection: | CaltechTHESIS |
Deposited By: | Imported from ETD-db |
Deposited On: | 29 May 2009 |
Last Modified: | 26 Nov 2019 19:13 |
Thesis Files
|
PDF (Full Thesis)
- Final Version
See Usage Policy. 5MB | |
|
PDF (01FrontMatter.pdf)
- Final Version
See Usage Policy. 85kB | |
|
PDF (02Intro.pdf)
- Final Version
See Usage Policy. 151kB | |
|
PDF (03Background.pdf)
- Final Version
See Usage Policy. 697kB | |
|
PDF (04ConvProc.pdf)
- Final Version
See Usage Policy. 1MB | |
|
PDF (05SBTInV.pdf)
- Final Version
See Usage Policy. 810kB | |
|
PDF (06FailProb.pdf)
- Final Version
See Usage Policy. 736kB | |
|
PDF (07Examples.pdf)
- Final Version
See Usage Policy. 2MB | |
|
PDF (08Conclusions.pdf)
- Final Version
See Usage Policy. 51kB | |
|
PDF (09Appendices.pdf)
- Final Version
See Usage Policy. 63kB | |
|
PDF (10Bibliography.pdf)
- Final Version
See Usage Policy. 88kB |
Repository Staff Only: item control page