Safety Verification and Failure Analysis of Goal-Based Hybrid Control Systems

• Main Author: Braman, Julia Marie Badger
• Format: Others
• Published: 2009
• Online Access: https://thesis.library.caltech.edu/2271/11/thesis.pdf; https://thesis.library.caltech.edu/2271/1/01FrontMatter.pdf; https://thesis.library.caltech.edu/2271/2/02Intro.pdf; https://thesis.library.caltech.edu/2271/3/03Background.pdf; https://thesis.library.caltech.edu/2271/4/04ConvProc.pdf; https://thesis.library.caltech.edu/2271/5/05SBTInV.pdf; https://thesis.library.caltech.edu/2271/6/06FailProb.pdf; https://thesis.library.caltech.edu/2271/7/07Examples.pdf; https://thesis.library.caltech.edu/2271/8/08Conclusions.pdf; https://thesis.library.caltech.edu/2271/9/09Appendices.pdf; https://thesis.library.caltech.edu/2271/10/10Bibliography.pdf; 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 <https://resolver.caltech.edu/CaltechETD:etd-05292009-111937>

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.