Ricardo Sanfelice receives Phase I funding from the Air Force SBIR Program
GN&C systems that involve mode-switching logic or gain-scheduling are both examples of a hybrid system, where the dynamics of a finite-state machine (e.g., the mode-logic or the gain-schedule) interact with the dynamics of a continuous-valued system (e.g., the attitude control system & attitude dynamics). State-of-practice for such systems involves rigorous analysis of both the continuous-valued system and the finite-state machine individually via standard techniques. But analysis of the coupled system comprised of the connected mode-logic and control systems is beyond current analysis approaches - regression testing via Monte-Carlo (MC) analysis is the only option, and does not provide rigorous guarantees. Recently, techniques have been published in the literature that allow rigorous analysis of these coupled system behaviors, and in some cases can design coupled mode-logic/control systems with rigorous guarantees for stability and robustness. This SBIR will apply these techniques to missions of AF interest and demonstrate the utility of the resulting set calculations. Techniques of interest include but are not limited to analysis approaches (e.g., linear-temporal logic specification verification via system approximation, bisimulation, model-checking) as well as synthesis approaches (e.g., guaranteed performance via composition or other proofs).