Verification Procedure for Generalized Goal-based Control Programs

Safety verification of fault-tolerant control systems is essential for the success of autonomous robotic systems. A control architecture called Mission Data System, developed at the Jet Propulsion Laboratory, takes a goal-based control approach. In this paper, the development of a method for converting a goal network control program into a hybrid system is given and a process for converting logic associated with the goal network into transition conditions for the hybrid automata is developed. The resulting hybrid system can then be verified for safety in the presence or failures using existing symbolic model checkers. An example task and goal network is designed, converted to hybrid automata, and verified using symbolic model checking software for hybrid systems.