Fault tolerance and safety verification of controludsystems are essential for the success of autonomous roboticudsystems. A control architecture called Mission Data Systemud(MDS), developed at the Jet Propulsion Laboratory, takesuda goal-based control approach. In this paper, a method forudconverting goal network control programs into linear hybridudsystems is developed. The linear hybrid system can then beudverified for safety in the presence of failures using existingudsymbolic model checkers. An example task is simulated inudMDS and successfully verified using HyTech, a symbolic modeludchecking software for linear hybrid systems.ud
展开▼
