Laboratoire: Verimag (http://www-verimag.imag.fr/)
Équipe: SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE)
Encadrants: David Monniaux <David.Monniaux@imag.fr>, Claire Maïza <Claire.Maiza@imag.fr>.
Contexte Scientifique
Dans les parties critiques des avions et des voitures, les programmes ne doivent pas seulement s’exécuter sans bug mais ils doivent aussi terminer leur exécution dans un temps imparti. Imaginez, par exemple, les dégâts causés si l’ABS ne réagissait pas à temps, ou si la sortie du train d’atterrissage n’était pas garantie avant l’atterrissage. Pour pouvoir garantir que les programmes s’exécutent suffisamment vite, il est primordial d’estimer une borne supérieure du temps d’exécution de ces programmes. Cette estimation du pire cas , worst case execution time (WCET) en anglais, doit être garantie supérieure ou égale à la borne supérieure réelle du temps d’exécution. Malheureusement, il n’est pas possible de mesurer cette borne car le nombre de cas à tester est bien trop important. Pour cette raison, l’estimation du temps d’exécution pire cas se fait de manière statique (sans exécuter le code).
La dernière phase de cette estimation du temps d’exécution pire-cas consiste à maximiser une fonction exprimant le temps d’exécution du programme. De manière générale, ceci s’effectue en utilisant des bornes de boucles pré-calculées. Nous avons conçu une méthode permettant de borner le temps de calcul, même dans le cas de programmes comportant des boucles sans bornes apparentes. Ces travaux sont toutefois très préliminaires et demandent de grandes améliorations.
Sujet
La première étape sera de comprendre notre technique d’analyse statique et les autres méthodes existantes. Ensuite, il s’agira d’améliorer notre technique d’analyse statique pour le WCET, tant en précision qu’en efficacité.
Compétences Attendues
- De bonnes bases en algorithmique, logique et recherche opérationnelle
- C++ ou Caml
Contexte de Travail
Le stagiaire sera encadré par David Monniaux et Claire Maïza (permanents du laboratoire). Ce sujet est lié à deux projets de recherche : le projet européen STATOR (ERC, David Monniaux) et le projet ANR W-7.
