OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method algorithm

Davy, Guillaume and Feron, Eric and Garoche, Pierre-Loïc and Henrion, Didier Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method algorithm. (2018) In: LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 16 November 2018 - 21 November 2018 (Awasa, Ethiopia).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.29007/qt5j


Classical control of cyber-physical systems used to rely on basic linear controllers. These controllers provided a safe and robust behavior but lack the ability to perform more complex controls such as aggressive maneuvering or performing fuel-efficient controls. Another approach called optimal control is capable of computing such difficult trajectories but lacks the ability to adapt to dynamic changes in the environment. In both cases, the control was designed offline, relying on more or less complex algorithms to find the appropriate parameters. More recent kinds of approaches such as Linear Model-Predictive Control (MPC) rely on the online use of convex optimization to compute the best control at each sample time. In these settings optimization algorithms are specialized for the specific control problem and embed on the device. This paper proposes to revisit the code generation of an interior point method (IPM) algorithm, an efficient family of convex optimization, focusing on the proof of its implementation at code level. Our approach relies on the code specialization phase to produce additional annotations formalizing the intended specification of the algorithm. Deductive methods are then used to prove automatically the validity of these assertions. Since the algorithm is complex, additional lemmas are also produced, allowing the complete proof to be checked by SMT solvers only. This work is the first to address the effective formal proof of an IPM algorithm. The approach could also be generalized more systematically to code generation frameworks, producing proof certificate along the code, for numerical intensive software.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-02384908
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National des Sciences Appliquées de Toulouse - INSA (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Georgia Institute of Technology (USA)
Laboratory name:
Deposited On:28 Nov 2019 14:38

Repository Staff Only: item control page