LogoLogo

Mussot, Vincent. Automates d'annotation de flot pour l'expression et l'intégration de propriétés dans l'analyse de WCET

Mussot, Vincent (2016). Automates d'annotation de flot pour l'expression et l'intégration de propriétés dans l'analyse de WCET.

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

Résumé en francais

Dans le domaine des systèmes critiques, l'analyse des temps d'exécution des programmes est nécessaire pour planifier et ordonnancer au mieux différentes tâches et par extension pour dimensionner les systèmes. La durée d'exécution d'un programme dépend de divers facteurs comme ses entrées ou le matériel utilisé. Or cette variation temporelle pose problème dans les systèmes temps-réel dans lesquels il est nécessaire de dimensionner précisément les temps processeur alloués à chaque tâche, et pour cela, connaître leur temps d'exécution au pire cas. Au sein de l'équipe TRACES à l'IRIT, nous cherchons à calculer une borne supérieure à ce temps d'exécution au pire cas qui soit la plus précise possible. Pour cela, nous travaillons sur le graphe de flot de contrôle d'un programme qui représente un sur-ensemble des ses exécutions possibles, que nous accompagnons d'annotations sur des comportements spécifiques du programme susceptibles de réduire la sur-approximation de notre estimation. Dans les outils destinés au calcul du temps d'exécution au pire cas des programmes, les annotations sont habituellement exprimées et intégrées grâce à des langages d'annotation spécifiques. Nous proposons d'utiliser des automates appelés automates d'annotation de flot en lieu et place de ces langages, afin de fonder non seulement l'expression, mais également l'intégration d'annotations dans l'analyse sur des bases formelles. Nous présentons ces automates enrichis de contraintes, de variables et d'une hiérarchie et nous montrons comment ils supportent les divers types d'annotations utilisés dans le domaine de l'analyse du temps d'exécution au pire cas. Par ailleurs, l'intégration des annotations dans une analyse se fait habituellement par l'association de contraintes numériques au graphe de flot de contrôle. Les automates que nous présentons supportent cette méthode mais leur expressivité offre également de nouvelles possibilités d'intégration basées sur le dépliage du graphe de flot de contrôle. Nous présentons des résultats expérimentaux issus de la comparaison de ces deux méthodes qui montrent comment le dépliage de graphe peut améliorer la précision de l'analyse. A terme, ce gain de précision dans l'estimation du temps d'exécution au pire cas permettra de mieux exploiter le matériel sans faire courir de risques à l'utilisateur ou au système.

Sous la direction du :
Directeur de thèse
Cassé, Hugues
Sotin, 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 - Systèmes temps-réel - Analyse statique - IPET - Automates hiérarchiques - Langage d'annotation
Sujets :Informatique
Déposé le :14 Apr 2017 15:23