State-Based Hybrid Control and Symbolic Model Checking

Verification Procedure for Generalized Goal-based Control Programs, Julia M.B. Braman, Richard M. Murray and Michel D. Ingham. AIAA Infotech@Aerospace, May 2007.

Control Program Verification for a Sample Titan Aerobot Mission, Julia M B Braman, Richard M Murray. AIAA Infotech@Aerospace Conference and Exhibit, 2009.

Mathematica - symbolic manipulation program
SBT Checker - This design for verification tool allows designers to ensure that the goal network or hybrid system control program has state-based transitions. Mathematica package (zip file), User guide (PDF)
InVeriant - A symbolic model checker that can quickly and efficiently perform reachability analyses on goal networks or hybrid systems with state-based transitions. Mathematica package (zip file), User guide (PDF)
LERExample.zip - zip file with Lunar Electric Rover (LER) example