CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper)

TL;DR

CODEV is a Matlab tool that automates the verification of safety guarantees in systems controlled by Model Predictive Control, combining hybrid automaton modeling with simulation-based analysis.

Contribution

It introduces the first automated method for verifying safety in MPC-controlled systems using hybrid automaton models and simulation-based algorithms.

Findings

Successfully applied to benchmark examples

Provides rigorous safety guarantees for MPC systems

Demonstrates potential for complex real-world problems

Abstract

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.