Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints

Elias Khalife, Pierre-Loic Garoche, Mazen Farhood

TL;DR

The paper develops a formal framework to verify invariant properties of uncertain discrete-time control systems modeled via linear fractional transformations and pointwise IQCs. It integrates IQC-based model analysis with deductive code verification, using ghost code to represent plant dynamics while preserving executable controller code, and addresses both real and floating-point arithmetic through Hoare logic and ACSL annotations. The authors provide practical verification strategies for LTI and affine LPV controllers, including templates and tool-supported workflows (Frama-C, ACSL, WP, Alt-Ergo) and demonstrate their approach on four diverse examples (UAS, AUV, hovercraft, two-mass). The work advances rigorous, code-level guarantees for closed-loop invariants under uncertainty, with potential impact on safety-critical control software by enabling sound operating envelopes despite modeling errors and finite precision. Future work aims to extend to reachability analyses and improve numerical property revalidation in practice.

Abstract

This paper focuses on formally verifying invariant properties of control programs both at the model and code levels. The physical process is described by an uncertain discrete-time state-space system, where the dependence of the state-space matrix-valued functions defining the system on the uncertainties can be rational. The proposed approaches make use of pointwise integral quadratic constraints (IQCs) to characterize the uncertainties affecting the behavior of the system. Various uncertainties can be characterized by pointwise IQCs, including static linear time-varying perturbations and sector-bounded nonlinearities. Using the IQC framework, a sound overapproximation of the uncertain system, which is expressible at the code level, is constructed. Tools such as Frama-C, ACSL, WP, and an Alt-Ergo plugin are employed to ensure the validity of the state and output invariant properties across both real and float models. The first proposed approach can be used to formally verify (local) invariant properties of the control code. This capability is demonstrated in a couple of examples involving gain-scheduled path-following controllers designed for an uncrewed aircraft system and an autonomous underwater vehicle. The second approach enables the verification of closed-loop invariant properties, i.e., invariant properties of the controlled system as a whole, in both real and float models, while preserving the integrity of the executable controller code. This is achieved by using ghost code attached to the control code for all elements related to the plant model with uncertainties, as the ghost code does not interfere with the executable code. The effectiveness of this approach is demonstrated in two examples on the control of a four-thruster hovercraft and the control of a two-mass rotational system.

Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints

TL;DR

The paper develops a formal framework to verify invariant properties of uncertain discrete-time control systems modeled via linear fractional transformations and pointwise IQCs. It integrates IQC-based model analysis with deductive code verification, using ghost code to represent plant dynamics while preserving executable controller code, and addresses both real and floating-point arithmetic through Hoare logic and ACSL annotations. The authors provide practical verification strategies for LTI and affine LPV controllers, including templates and tool-supported workflows (Frama-C, ACSL, WP, Alt-Ergo) and demonstrate their approach on four diverse examples (UAS, AUV, hovercraft, two-mass). The work advances rigorous, code-level guarantees for closed-loop invariants under uncertainty, with potential impact on safety-critical control software by enabling sound operating envelopes despite modeling errors and finite precision. Future work aims to extend to reachability analyses and improve numerical property revalidation in practice.

Abstract

This paper focuses on formally verifying invariant properties of control programs both at the model and code levels. The physical process is described by an uncertain discrete-time state-space system, where the dependence of the state-space matrix-valued functions defining the system on the uncertainties can be rational. The proposed approaches make use of pointwise integral quadratic constraints (IQCs) to characterize the uncertainties affecting the behavior of the system. Various uncertainties can be characterized by pointwise IQCs, including static linear time-varying perturbations and sector-bounded nonlinearities. Using the IQC framework, a sound overapproximation of the uncertain system, which is expressible at the code level, is constructed. Tools such as Frama-C, ACSL, WP, and an Alt-Ergo plugin are employed to ensure the validity of the state and output invariant properties across both real and float models. The first proposed approach can be used to formally verify (local) invariant properties of the control code. This capability is demonstrated in a couple of examples involving gain-scheduled path-following controllers designed for an uncrewed aircraft system and an autonomous underwater vehicle. The second approach enables the verification of closed-loop invariant properties, i.e., invariant properties of the controlled system as a whole, in both real and float models, while preserving the integrity of the executable controller code. This is achieved by using ghost code attached to the control code for all elements related to the plant model with uncertainties, as the ghost code does not interfere with the executable code. The effectiveness of this approach is demonstrated in two examples on the control of a four-thruster hovercraft and the control of a two-mass rotational system.

Paper Structure

This paper contains 28 sections, 2 theorems, 33 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. IQC Framework
  4. Uncertainty Sets.
  5. IQCs.
  6. Uncertain System Modeling
  7. Preliminary Results
  8. Model-Level Verification of Invariants of Dynamical Systems with Floating-Point Arithmetic
  9. Expressing Invariant Properties in Hoare Logic
  10. State Invariant Property.
  11. Output Invariant Property.
  12. Incremental Verification Process: From Real to Floating-Point Arithmetic Verification
  13. Verification in the Float Model
  14. Stateful Contracts: Verification of Invariant Systemic Properties Using Ghost Code
  15. LTI Controllers
  16. ...and 13 more sections

Key Result

theorem thmcountertheorem

If there exist $P\in\mathbb{S}_{++}^{n_H}$, $\tau_1\geq0$, and $\tau_2\geq0$ such that for $i=1,\ldots,t$, and $B_{H_2}^\top P B_{H_2}+\tau_2 D_{H_{12}}^\top S_x D_{H_{12}}\succeq 0$, then $x_H(k)\in\mathcal{E}_P$ implies that $x_H(k+1)\in\mathcal{E}_P$ for any $k\geq 0$, i.e., $\mathcal{E}_P$ is a state-invariant ellipsoid for $H$.

Figures (3)

  • Figure 1: LFT system $(G,\Delta)$.
  • Figure 3: Schematic of the verification process using ghost annotations, excluding exogenous inputs and uncertainties. The orange box represents the executable controller code; the dashed box corresponds to ghost code for the plant; dashed arrows indicate ghost variables; and variables with apostrophes are the updated states.
  • Figure 4: Sketch of the annotations used to attach closed-loop contracts to a controller code. The presented pseudo-code is a sketch that outlines the key elements of the contract. We refer the reader to the examples to see the valid syntax. Predicate is called using the definition of the augmented system . Similarly, and should define the dynamics of the augmented system. The presented contract requires to add an extra set of ghost variables (here ) to the function prototype but does not modify the content of the controller function itself. only appears in the and .

Theorems & Definitions (3)

  • theorem thmcountertheorem: AboujaoudeGarocheFarhood21
  • theorem thmcountertheorem: invariantpwIQC
  • remark thmcounterremark