Automated Testing and Formal Verification of State-Machine Switched Guidance and Control Systems

Posted May 22, 2019

Multi-mode control systems for non-linear dynamical systems that are switched using finite state machines are a class of cyber-physical system that are difficult to develop, verify, and validate. The goal is to show that these systems will always eventually reach a desired state, that mode transitions are smooth, and that continuous time control and state constraints are not violated. This project will develop regression tools that work in the MathWorks tool chain that assist the development and testing of such systems.