Vérification des Optimisations Rapides Appliquées à la Commande Embarquée – VORACE

Les algorithmes d'optimisation, lorsqu'ils sont utilisés dans un
contexte temps-réel embarqué critique, permettent d'augmenter de façon
significative les capacités d'autonomie d'un système robotique ou d'un système
embarqué. Leur mise en œuvre permet en effet de prévoir, de planifier et de
réaliser des missions critiques. Ils peuvent ainsi réaliser ce qu'ils font déjà
sur les applications non embarquées utilisant ces algorithmes avancés
d'optimisation. Cependant une limite majeure à leur application dans un tel cadre
embarqué critique et temps réel ne peut et ne pourra se faire sans l'apport de
garantie supplémentaire par rapport à leur utilisation dans un cadre non
critique. Ainsi, il est primordial de pouvoir garantir le respect des délais
(calcul de pire temps d'exécution, WCET), l'absence d'erreur à l'exécution (RTE)
telles que les divisions par zéro ou les dépassements de capacité. Enfin la
sémantique propre de ces algorithmes, ce pourquoi ils ont été conçus, doit être
garantie, c'est à dire formalisée et documentée de la spécification à
l'implémentation. L'expression et la vérification d'une telle sémantique pouvant
faire intervenir des aspects complexes comme la précision flottante.

L'objectif de ce projet est de construire une étude autour de l'utilisation
effective de tels algorithmes d'optimisation dans un contexte embarqué critique
et temps-réel.

Une première étape consistera à étudier la vaste littérature de ce sujet en se
focalisant plus spécifiquement sur les aspects performances des
algorithmes. Cette étude sera effectuée à la lumière des contraintes de
certification des systèmes embarqués critiques temps-réels mentionnés ci-dessus,
ainsi qu'à leur application effective pour des missions autonomes critiques. Un
soin particulier sera apporté sur les aspects temps et respect des délais.

Une seconde étape étudiera comment ces algorithmes et leur implémentation
peuvent être modifiés pour satisfaire ces contraintes temps-réel, en particulier
sur l'aspect imprécision flotaante. L'utilisation des approches de spécification
formelle permettra d'enrichir l'implémentation de l'algorithme pour les
informations, les éléments de preuve permettant de garantir le respect des
propriétés recherchées. En particulier, l'utilisation de sémantique axiomatique
basée sur des triplets de Hoare devra permettre d'exprimer au plus près du code,
les éléments de correction de l'état de l'art.

Nous commencerons notre étude par un classe d'algorithmes bien maîtrisée: les
algorithmes d'optimization convexe en dimension finie. Cette classe d'algorithme
est également pertinente du fait de son utilisation dans un large gamme
d'application comme par exemple la recherche de chemins optimaux.

L'approche proposée sera également outillée par un outil permettant d'obtenir à
partir d'un algorithme prouvé correct, une implémentation enrichie par les
arguments de preuve. Cette documentation automatique de l'implémentation sera
aussi utilisée pour évaluer la pertinence d'outils d'analyses modernes comme
ceux issus de l'interprétation abstraite.