ASTRID - Accompagnement spécifique des travaux de recherches et d’innovation Défense

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

Résumé de soumission

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.

Coordinateur du projet

Institut de Recherche en Informatique de Toulouse (Laboratoire public)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Laboratoire d’Analyse et d’Architecture des Systèmes
Rockwell collins France
Institut de Recherche en Informatique de Toulouse
ONERA DTIM

Aide de l'ANR 291 392 euros
Début et durée du projet scientifique : mars 2013 - 36 Mois

Liens utiles