Control Program Verification for a Sample Titan Aerobot Mission
Julia M. B. Braman, Richard M. Murray · AIAA Infotech@Aerospace Conference · 2009
The success of complex autonomous robotic systems depends on the quality and correctness of their fault tolerant control systems. A goal-based control approach is used to design an example control program for a proposed mission to Titan, a moon of Saturn. The state space of the example exceeds the capability of existing symbolic model checkers for hybrid automata, so a novel verication method is developed. An original design for verication software tool called SBT Checker that aids in the design of modular, state-based goal trees for the control of separate tasks in the overall mission, is discussed. The combination of the individual goal trees constitute a goal network control program that can be veried against unsafe conditions using the novel InVeriant software. InVeriant converts goal networks to hybrid systems whose special structure is exploited to quickly nd the reachable unsafe states. The Titan aerobot mission example is then veried using this new method.