LogoLogo

Ballabriga, Clément. Vérification de contraintes temporelles strictes sur des programmes par composition d'analyses partielles

Ballabriga, Clément (2010) Vérification de contraintes temporelles strictes sur des programmes par composition d'analyses partielles.

[img]
Preview
PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
2794Kb

Résumé en francais

Les systèmes temps-réel critiques doivent impérativement obéir à des contraintes temporelles strictes. Le respect de ces contraintes doit donc être prouvé, et le calcul de pire temps d'exécution (WCET ou Worst Case Execution Time) joue un rôle important dans cette preuve. Le calcul de WCET par analyse statique est généralement réalisé sur un programme entier. Ceci présente deux inconvénients : la plupart de ces méthodes de calcul voient leur temps d'exécution augmenter de manière non linéaire par rapport à la taille de la tâche à analyser, et un problème se pose lorsque cette tâche est constituée de plusieurs composants (dont certains ne sont pas disponibles au moment de l'analyse). Il est donc nécessaire d'introduire une approche d'analyse partielle, permettant d'analyser séparément les composants d'un programme, produisant un résultat de WCET partiel pour chaque composant. Ces résultats partiels peuvent ensuite être composés pour obtenir le WCET du programme. Le calcul de WCET comporte plusieurs analyses dont les résultats sont exprimés sous forme d'un système ILP, qui doit ensuite être résolu pour obtenir le WCET. Chaque analyse doit être adaptée pour faire de l'analyse partielle. Cette adaptation sera illustrée à l'aide de diverses analyses existantes, et une formulation générale pour l'analyse partielle sera donnée. Il sera ensuite montré qu'il est possible d'utiliser l'analyse partielle afin d'accélérer la résolution ILP. L'expérimentation montre que l'analyse partielle permet de réduire le temps de calcul et de traiter le cas des programmes avec composants, sans rajouter trop de pessimisme.

Sous la direction du :
Directeur de thèse
Sainrat, Pascal
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :WCET - Temps-réel strict - Analyse statique - Analyse partielle
Sujets :Informatique
Déposé le :27 May 2011 12:23