Bisimulation conversion and verification procedure for goal-based control systems
- Creators
- Braman, Julia M. B.
-
Murray, Richard M.
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, addresses these needs with a goal-based control approach. In this paper, a software algorithm for converting goal network control systems 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 example goal network control system is converted to a linear hybrid system using the automatic conversion software that is based on the bisimulation and then is verified.
Additional Information
© 2010 Springer Science, LLC. Published online: 22 December 2010. The authors would like to gratefully acknowledge Kenneth Meyer, Michel Ingham, David Wagner, Robert Rasmussen, Kirk Reinholtz, and the rest of the MDS team at JPL for feedback, suggestions, answered questions, and MDS and State Analysis instruction. This work was funded in part by the Air Force Office of Scientific Research (AFOSR) and The Boeing Company.Additional details
- Eprint ID
- 22716
- Resolver ID
- CaltechAUTHORS:20110308-123056956
- Air Force Office of Scientific Research (AFOSR)
- Boeing Company
- Created
-
2011-03-09Created from EPrint's datestamp field
- Updated
-
2021-11-09Created from EPrint's last_modified field