CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper)
For control engineers using MPC, CODEV offers the first automated safety verification, addressing a critical gap in ensuring rigorous guarantees for constrained and optimal control systems.
CODEV is a Matlab-based tool that automatically designs and verifies Model Predictive Control (MPC) systems, providing the first automated approach to guarantee safety by verifying that the system robustly maintains constraints. It successfully applied to benchmark examples, demonstrating potential for complex MPC problems.
We present CODEV, a Matlab-based tool for verifying systems employing Model Predictive Control (MPC). The MPC solution is computed offline and modeled together with the physical system as a hybrid automaton, whose continuous dynamics may be nonlinear with a control solution that remains affine. While MPC is a widely used synthesis technique for constrained and optimal control in industry, our tool provides the first automated approach of analyzing these systems for rigorous guarantees of safety. This is achieved by implementing a simulation-based verification algorithm for nonlinear hybrid models, with extensions tailored to the structure of the MPC solution. Given a physical model and parameters for desired system behavior (i.e. performance and constraints), CODEV generates a control law and verifies the resulting system will robustly maintain constraints. We have applied CODEV successfully to a set of benchmark examples, which illuminates its potential to tackle more complex problems for which MPC is used.