View source for Automatic Conversion Software for the Safety Verification of Goal-Based Control Programs

{{HTDB paper
| authors = Julia M B Braman, Richard M Murray
| title = Automatic Conversion Software for the Safety Verification of Goal-Based Control Programs 
| source = International Conference on Software Engineering, 2009 (submitted)
| year = 2008
| type = Preprint
| funding = 
| url = http://www.cds.caltech.edu/~murray/preprints/bm09-icse_s.pdf
| abstract = 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, a software algorithm for converting goal network control programs into linear hybrid systems is described. The conversion process is a bisimulation; the resulting linear hybrid system can be verified for safety in the presence of failures using existing symbolic model checkers, and thus the original goal network is verified. A moderately complex goal network control program is converted to a linear hybrid system using the automatic conversion software and then verified. 
| flags = 
| tag = bm09-icse
| id = 2008t
}}