Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] PhD defense Guillaume Davy - 12/6/2018 - Generation of codes and provable annotations of interior-point algorithms for critical embedded systems

  • Subject: [Frama-c-discuss] PhD defense Guillaume Davy - 12/6/2018 - Generation of codes and provable annotations of interior-point algorithms for critical embedded systems
  • From: davyg2 at gmail.com (Guillaume DAVY)
  • Date: Fri, 30 Nov 2018 17:27:45 +0100
Hi,

It is my pleasure to invite you to my PhD thesis defense : « Generation of
codes and provable annotations of interior-point algorithms for critical
embedded systems ». The defense will be in French.

Defense date :
  December 6th, 2018 at 10:00

Location :
  Auditorium de l'ONERA
  2 Avenue Edouard Belin
  31000 Toulouse

The building is in a protected area so you have to send an email to
Guillaume.DAVY at isae.fr if you want to be added to the guest list.
Moreover, you will have to bring an ID.

In case of success, you are all invited to the "pot" at 16h.

PHD committee:
  - M. Didier HENRION
  - M. Pierre-Loïc GAROCHE
  - Mme Sylvie PUTOT
  - M. Yves BERTOT
  - Mme Sylvie BOLDO
  - M. Eric FERON

Summary: (Version française en dessous)
The use of convex optimization within aeronautics critical systems has
emerged for the
last years. The benefits of optimization can range from reducing the
consumption of fuel
oil to new control techniques. For example, the rocket landing done by
SpaceX is based on
the online solving of convex optimization problem thanks to interior point
algorithms. Howe-
ver, these algorithms are expensive in computing time, but the growing
power of computer
systems allows, nowadays, their use online. Moreover, in order to reduce
computing times,
manufacturers choose to develop specific implementations for the problems
to be solved.
Optimization, however, remains limited to secondary computations, or
uncritical systems.
In order to generalize their use, manufacturers will have to guarantee the
implementations of
these algorithms. This consists in checking : 1. no runtime error, 2. that
it answers in a finite
time, ideally bounded, 3. the correction of the returned solution.
Regarding the last point, for an optimization algorithm, the solution must
satisfy the
constraint and be optimal.
In this work, we developed tools and methods that allow to formally
guarantee an interior
point algorithm generated code. We used methods and tools from the formal
program veri-
fication to generate a code embeddable, but also provable from a given
convex optimization
problem. The main contributions made by this manuscript are : 1. the
creation of a language,
pySil, which allows to express simple algorithms with matrix computation,
as well as their
specifications. 2. the writing, in pySil, of an interior point algorithm.
3. the development
of a pySil compiler to the C / ACSL language to obtain a code executable
online, but also
provable by Frama-C. 4. the enrichment of the specification of the
algorithm written in pySil
so that Frama-C can prove the correction of the C/ACSL compiled files.
This approach was evaluated on examples, in particular of predictive
control. On the other
hand, we conducted this work with the aim of clearly explaining and
minimizing software and
assumptions on which the proof of correction is based.
Keywords: Verification, Control, Formal method, Optimization, Hoare logic,
MPC


Résumé : (English version below)
L’aéronautique a vu émerger ces dernières années l’utilisation
d’optimisation convexe au sein de ses systèmes critiques. Les avantages
apportés par l’optimisation peuvent aller de la réduction de la
consommation de fioul à de nouvelles techniques de contrôle. Par exemple,
l’atterrissage de fusée comme pratiqué par SpaceX se base sur la résolution
en ligne de problème d’optimisation convexe grâce à des algorithmes de
point intérieur. Toutefois, ceux-ci sont couteux en temps de calcul, mais
la puissance grandissante des systèmes informatiques permet, désormais,
leur utilisation en ligne. De plus, afin de réduire les temps de calcul au
maximum, les industriels choisissent de développer des implémentations
spécifiques aux problèmes à résoudre. L’optimisation reste cependant
aujourd’hui limitée à des calculs secondaires, ou à des systèmes peu
critiques. Pour généraliser leur utilisation, au sein de systèmes grand
public, les industriels devront pouvoir certifier les implémentations de
ces algorithmes. Cela consiste à vérifier : 1. l’absence d’erreur à
l’exécution, 2. qu’eles répondent en temps fini, idéalement borné 3. la
correction de la solution retournée. Dans le cas de l’optimisation, ce
dernier point correspond à vérifier que la solution respecte les
contraintes et est optimale. Ce travail a consisté à développer des outils
et des méthodes qui permettent de certifier formel- lement un code généré
d’algorithme de point intérieur. Pour cela, nous avons utilisé des méthodes
et outils issus de la vérification formelle de programmes afin de générer
un code embarquable, mais aussi prouvable à partir de la donnée d’un
problème d’optimisation convexe. Les principales contributions apportées
par ce manuscrit sont : 1. La création d’un langage, pySil, qui permet
d’exprimer simplement des algorithmes numériques matriciels, ainsi que
leurs spécifications. 2. L’écriture, en pySil, d’un algorithme de point
intérieur. 3. Le développement d’un compilateur de pySil vers le langage
C/ACSL afin d’obtenir un code à la fois exécutable en ligne, mais aussi
prouvable par Frama-C. 4. L’enrichissement de la spécification de
l’algorithme écrit en pySil afin que Frama-C puisse prouver la correction
de sa compilation en C/ACSL. L’approche a pu être évaluée sur des exemples,
en particulier de commande prédictive. D’autre part, nous avons mené ce
travail avec le souci d’expliciter clairement et réduire au maximum les
logiciels et hypothèses sur lesquels repose la preuve de correction.
Mots-clés : Vérification, Contrôle, Méthode formelle, Optimisation, Logique
de Hoare, Commande prédictive

Regards,

Guillaume DAVY
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181130/f5f4dcea/attachment.html>