Towards Formally Verified Invariant Properties of Control Code Using Robustness Analysis Results

Abstract

Safety-critical aerospace systems rely on digital feedback controllers designed to satisfy stability, performance, and safety requirements despite uncertainties and disturbances. These guarantees are typically established through robust control analysis performed at the model level, under the assumption of exact, infinite-precision arithmetic. However, such guarantees do not automatically extend to the executable code, as floating-point computation and roundoff errors can compromise model-level properties. This dissertation addresses this gap by establishing and connecting robust control analysis results for discrete-time uncertain systems with the deductive formal verification of the corresponding executable code. Robust control analysis results, however, can be conservative. One way to assess this conservatism is to examine how a system behaves under worst-case conditions. To this end, this dissertation develops methods for constructing input signals that drive asymptotically stable, discrete-time linear time-varying systems toward their worst-case behavior, providing a means of evaluating the tightness of established performance results. Beyond this assessment, the dissertation advances the underlying analysis frameworks, including methods for computing invariant and bounding ellipsoids for systems with uncertainties characterized using pointwise integral quadratic constraints. It also establishes stability and performance guarantees for switched linear control laws. To further reduce conservatism in reachability analysis, sum-of-squares programming is used to construct verified quadratic characterizations for smooth nonlinearities and activation functions in feedforward neural networks. Ultimately, these results yield ellipsoidal and quadratic-constraint certificates that establish invariant properties at the model level. On the verification side, this dissertation establishes a deductive workflow that translates these mathematical certificates into code-level contracts, formally verifying the corresponding executable C code while explicitly accounting for floating-point errors. This workflow is then extended from local, single-component properties to systemic, closed-loop properties. By encoding an augmented-system abstraction using ghost code, the approach enables the formal verification of these systemic properties in both the real and float models, without modifying the executable controller code. Collectively, this dissertation establishes a certificate-based pathway from robust control analysis to the formal verification of control programs, while also developing the tools needed to assess and reduce the conservatism of the underlying analysis.