CISE-ANR: SHF: Small: CAFEE: Control Algorithms Formal End-to-End Verification

Traditional control theorists are concerned with high-level control algorithms and their high-level properties such as convergence, robustness and performance. Notably, they typically assume all calculations are done with real numbers, and do not pay as much attention to the concrete implementation of their control algorithms, or to errors introduced by machine arithmetic. The project's novelties are to bridge the gap between control theory and low-level implementations, and to provide typical control theory guarantees on the implementation rather than on a high-level algorithm. The project's impacts are a comprehensive framework for end-to-end verification of control systems, and applications to the automotive and aerospace domains. This framework encompasses high-level hybrid models down to the verification of embedded C code. The investigators are working closely with several government agencies and industrial partners for technology transfer. The project is first exploring simple linear discrete-time systems, by designing an end-to-end process achieving verification at all stages, with discrete-time plant semantics. The project is then extending this process to focus on hybrid systems consisting of a continuous-time plant and a discrete-time controller. While typical control engineers work either with pure continuous-time or pure discrete-time models for verification purposes, the actual system combines both paradigms. The project also considers control algorithms that rely on optimization routines, such as model predictive control (MPC). Throughout these tasks, the investigators focus on numerical accuracy using machine arithmetic. One outcome of the project is to provide modular, reusable, open-source formal proofs of end-to-end correctness of common controllers, namely the Proportional–integral–derivative (PID) and MPC controllers. Finally, the project is applying these techniques on three different applications: car collision avoidance, aircraft collision avoidance, and spacecraft docking. The project strives to give research opportunities to students from groups underrepresented in the computing field, through different programs at the University of Michigan and at Ecole Nationale de l'Aviation Civile (ENAC). The project also incorporates findings into control theory and embedded systems college classes, giving students an understanding of the challenges faced when implementing a controller. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.