CaltechTHESIS
  A Caltech Library Service

Safety verification and failure analysis of goal-based hybrid control systems

Citation

Braman, Julia Marie Badger (2009) Safety verification and failure analysis of goal-based hybrid control systems. Dissertation (Ph.D.), California Institute of Technology. http://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
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Murray, Richard M.
Thesis Committee:
  • Murray, Richard M. (chair)
  • Beck, James L.
  • Burdick, Joel Wakeman
  • Chandy, K. Mani
Defense Date:27 May 2009
Author Email:jmbraman (AT) yahoo.com
Record Number:CaltechETD:etd-05292009-111937
Persistent URL:http://resolver.caltech.edu/CaltechETD:etd-05292009-111937
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 Dec 2012 02:49

Thesis Files

[img]
Preview
PDF (01FrontMatter.pdf) - Final Version
See Usage Policy.

83Kb
[img]
Preview
PDF (02Intro.pdf) - Final Version
See Usage Policy.

147Kb
[img]
Preview
PDF (03Background.pdf) - Final Version
See Usage Policy.

680Kb
[img]
Preview
PDF (04ConvProc.pdf) - Final Version
See Usage Policy.

1079Kb
[img]
Preview
PDF (05SBTInV.pdf) - Final Version
See Usage Policy.

791Kb
[img]
Preview
PDF (06FailProb.pdf) - Final Version
See Usage Policy.

718Kb
[img]
Preview
PDF (07Examples.pdf) - Final Version
See Usage Policy.

2636Kb
[img]
Preview
PDF (08Conclusions.pdf) - Final Version
See Usage Policy.

50Kb
[img]
Preview
PDF (09Appendices.pdf) - Final Version
See Usage Policy.

62Kb
[img]
Preview
PDF (10Bibliography.pdf) - Final Version
See Usage Policy.

86Kb
[img]
Preview
PDF (thesis.pdf) - Final Version
See Usage Policy.

5Mb

Repository Staff Only: item control page