[M2R-2013-2014] Analyse sémantique des programmes pour l’évaluation de leur pire temps d’exécution

L’évaluation du pire temps d’exécution des programmes ("worst case execution time" ou WCET) est un objectif très important dans la conception des systèmes temps-réel critiques (avionique, automobile, spatial,...).. Ce pire temps dépend évidemment des caractéristiques de l’architecture sur laquelle le programme est exécuté, mais il dépend également finement de la sémantique du programme, et en particulier des chemins d’exécution réalisables dans le code. L’objectif de ce projet est d’appliquer les techniques modernes d’analyse sémantique des programmes pour détecter des chemins impossibles, ou pour borner le nombre d’exécutions de fragments de code. Il s’agira en particulier d’étudier l’expression des propriétés importantes pour le temps d’exécution, en termes de propriétés analysables par les outils d’analyse existants. Dans un deuxième temps il se peut que les outils doivent être adaptés ou améliorés pour rendre les résultats attendus. Le candidat acquerra des compétences en analyse statique de programmes et en compilation. Le sujet est susceptible d’être prolongé par un sujet de thèse.

Contexte : projet W-SEPT (financé par l’Agence National pour la Recherche)

Encadrants : Nicolas Halbwachs, Claire Maiza (prenom.nom@imag.fr)