English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Classical control of cyber-physical systems used to rely on basic linearcontrollers. These controllers provided a safe and robust behavior but lack theability to perform more complex controls such as aggressive maneuvering orperforming fuel-efficient controls. Another approach called optimal control iscapable of computing such difficult trajectories but lacks the ability to adaptto dynamic changes in the environment. In both cases, the control was designedoffline, relying on more or less complex algorithms to find the appropriateparameters. More recent kinds of approaches such as Linear Model-PredictiveControl (MPC) rely on the online use of convex optimization to compute the bestcontrol at each sample time. In these settings, optimization algorithms arespecialized for the specific control problem and embed on the device. Thispaper proposes to revisit the code generation of an interior point method(IPM)algorithm, an efficient family of convex optimization, focusing on theproof of its implementation at code level. Our approach relies on the codespecialization phase to produce additional annotations formalizing the intentedspecification of the algorithm. Deductive methods are then used to proveautomatically the validity of these assertions. Since the algorithm is complex,additional lemmas are also produced, allowing the complete proofto be checkedby SMT solvers only. This work is the first to address the effective formalproof of an IPM algorithm. Theapproach could also be generalized moresystematically to code generation frameworks, producing proof certificate alongthe code, for numerical intensive software.

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm