Automatic Conversion Software for the Safety Verification of Goal-based Control Programs

Julia M B Braman, Richard M Murray
Proceedings of the International Conference on Intelligent Robots and Systems, 2008 (submitted)

Fault tolerance and safety verification of control systems are essential for the success of autonomous robotic systems. A control architecture called Mission Data System (MDS), developed at the Jet Propulsion Laboratory, takes a goal-based control approach. In this paper, an automatic software algorithm for converting goal network control programs into linear hybrid systems is described. The linear hybrid system can then be verified for safety in the presence of failures using existing symbolic model checkers. Several benchmark problems are converted from goal networks to linear hybrid automata, illustrating that complex goal networks can be converted and verified using this method.

Preprint
Downloading and printing FAQ