VORACE - Verified fast optimization for embedded control
French Government Defense Agency (DGA) and National Research Agency (ANR)

Scope

The project VORACE (Vérification des Optimisations Rapides Appliquée à la Commande Embarquée - Verification of fast optimization algorithms applied in critical embedded control) is funded by the ASTRID programme of the DGA (Direction Generale de l'Armement - French Government Defense Agency) and managed by ANR (Agence Nationale de la Recherche - French National Research Agency).

Project summary

Optimization algorithms, when they are used in a real-time and safety-critical context, offer the potential for considerably advancing robotic and autonomous systems by enabling significant improvements in their ability to initiate, plan, and execute complex missions. In that regard, they are likely to realize the same promise as that delivered long ago by the desktop application of optimization algorithms. However, this promise cannot happen without proper attention to the considerably stronger operational constraints that real-time, safety- critical application must meet, unlike their non real-time, desktop counterparts. In particular, safety-critical real-time optimization algorithms must be equipped with deterministic bounds on their worst-case execution time (WCET). Absence of run-time errors, such as variable range overflows and divide-by zero errors, must be systematically analyzed and eliminated. Finally, the semantics of optimization algorithms, that is, what they actually do, must be systematically documented and accessible at all implementation levels, ranging from specification documents to binary executables. Such semantics may be complex to obtain when the original purpose of the optimization algorithms is combined with real-world computational imperfections, such as floating-point number approximation and computation.

We therefore propose a comprehensive study aimed at defining the suitability of optimization algorithms to meet the stringent constraints that must be met by real-time safety critical software.

Period

March 2013 - March 2017

Participants

  • Michael Dierkes (Rockwell-Collins)
  • Eric Feron (ENAC/INP and Georgia Tech)
  • Pierre-Loic Garoche (ONERA)
  • Didier Henrion (LAAS-CNRS and Czech Tech Univ Prague)
  • Mioara Joldes (LAAS-CNRS)
  • Jean-Bernard Lasserre (LAAS-CNRS)
  • Marc Pantel (IRIT/ENSEEIHT) - project leader
  • Xavier Thirioux (IRIT/ENSEEIHT).

    Events

  • 22 March 2013. Kick-off meeting at ENSEEIHT/INP Toulouse.

  • 2 October 2013. Meeting at LAAS-CNRS Toulouse. Presentations by Raphael Cohen (ENSMA and Georgia Tech) and Mioara Joldes (LAAS-CNRS Toulouse).

  • 20 January 2014. Meeting at LAAS-CNRS Toulouse. Presentations by Victor Magron (LAAS-CNRS Toulouse) and Assale Adjé (ONERA Toulouse).

  • 12-14 May 2014. First VORACE workshop in Toulouse. As a follow-up of this workshop, the USA National Science Foundation (NSF) awarded a Cyber Physical Systems (CPS) Collaborative Research Award of USD910000 for the period 2015-2017 to Eric Feron (ENAC/INP and Georgia Tech), Behcet Acikmese (Univ. Texas Austin) and John Hauser (Univ. Colorado Boulder), entitled SORTIES (Semantics of Optimization for Real Time Intelligent Embedded Systems).

  • 12 May 2014. SPOT seminar focused on computer science and optimization.

  • 3-7 November 2014. Kick-off meeting of the related FastRelax ANR project focusing on computer-aided proofs for global optimization, amongst many other topics.

  • Winter 2015. Visit of Tim Wang (Georgia Tech) at IRIT/ENSEEIHT.

  • 28 Feb-1 Mar 2015. Pierre-Loic Garoche (ONERA) attends the workshop "Real-time optimization in systems control and autonomy" in Silverthorne, Colorado.

  • 23-24 April 2015. Visit and seminar of David Monniaux, Alexandre Marechal and Tim King (VERIMAG) at LAAS-CNRS.

  • 11-13 May 2015. Visit and seminar of Jean-Michel Muller (INRIA and ENS Lyon) at LAAS-CNRS.

  • 12-13 May 2015. Visit and seminar of Anders Rantzer (Lund Univ.) at LAAS-CNRS and ONERA.

  • 11-12 June 2015. Second VORACE workshop in Toulouse.

  • 1 November - 18 December 2015. Visit and seminar of Milan Korda (EPFL) at LAAS-CNRS.

  • 18 December 2015. Meeting at ONERA. Talks by Guillaume Davy (PhD student of Pierre-Loic Garoche and Didier Henrion), Pierre-Loic Garoche (joint work with Assale Adje and Victor Magron) and Didier Henrion (joint work with Pierre-Loic Garoche, Xavier Thirioux, Assale Adje, Victor Magron, Pierre Roux and Milan Korda).

  • 20-22 September 2016. Third VORACE workshop in Toulouse.

  • 20 February 2017. Last VORACE workshop in Prague.

    Scientific productions

  • T. Wang, R. Jobredeaux, M. Pantel, P.-L. Garoche, E. Feron, D. Henrion. Credible autocoding of convex optimization algorithms. hal-00961133 and arXiv:1403.1861, March 2014.

  • A. Adjé, P.-L. Garoche. Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. hal-01064408 and arXiv:1409.5089, September 2014. Appeared in pp. 99-116 of Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science Volume 8931, Springer, 2015.

  • A. Adjé, P.-L. Garoche, A. Werey. Quadratic Zonotopes:An extension of Zonotopes to Quadratic Arithmetics arXiv:1411.5847, November 2014.

  • V. Magron, D. Henrion, J. B. Lasserre. Semidefinite approximations of projections and polynomial images of semialgebraic sets. hal-01075343, December 2014.

  • A. Adjé, P.-L. Garoche, V. Magron. Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization. hal-01134816 and arXiv:1503.07025, March 2015.

  • A. Adjé, P.-L. Garoche, V. Magron. A Sums-of-Squares Extension of Policy Iterations. arXiv:1503.08090, March 2015.

  • P.-L. Garoche, D. Henrion, V. Magron, X. Thirioux. Semidefinite Approximations of Reachability Sets for Discrete-time Polynomial Systems. Talk to be given by V. Magron at the SMAI-MODE conference, Toulouse, March 23-25, 2016.