ssr: Proposition de thèse
Posté le vendredi 17 février 2006 par Fabrice Kordon

Bonjour,

Voici une proposition de thèse que j’ai reçue par email. Je vous la livre tel que sachant que vous pouevz déjà prendre contact. C’est fortement orienté SRETR bien sûr.

Nous recherchons un ingénieur ou un doctorant pour travailler sur le sujet décrit-ci-dessous.

Vérification de contraintes temporelles strictes sur des programmes binaires par composition d’analyses partielles

contact : H. Cassé

laboratoire : Institut de Recherche en Informatique de Toulouse

équipe : TRACES

Le numérique est de plus en plus utilisé dans des applications obéissant à des contraintes strictes de temps réel. Alors que le dysfonctionnement de certaines de ces applications peut avoir des conséquences critiques, du point économique, environnemental ou humain, il est nécessaire de prouver qu’elles satisfont les contraintes temporelles. Le calcul de pire temps d’exécution ou Worst Case Execution Time est une composante des vérifications réalisées : elle consiste à calculer le temps d’exécution maximal d’une tâche d’un programme en prenant en compte les caractéristiques matérielles de la plate-forme hôte. Dans ce sujet, nous nous intéressons principalement au calcul de WCET par analyse statique. On procède en général en trois phases : la première consiste à calculer les informations d’exécution à effet global, comme la modélisation du cache ou du flot de contrôle du programme ; la seconde prend en compte les effets locaux comme le pipeline et la dernière utilise les résultats des deux phases précédentes pour obtenir le WCET final. Actuellement, le calcul de WCET est uniquement réalisé de manière monolithique sur un programme complet. Avec l’évolution actuelle des applications temps réel et du logiciel embarqué, cette approche risque de ne pas être suffisante. Tout d’abord, la taille des programmes est en constante augmentation alors que les méthodes de calcul de WCET ont un temps de calcul exponentiel sur la taille du code à traiter. D’autre part, l’utilisation de plus en plus fréquente de composants standards, Component-Off-The-Shelf, et de système d’exploitation temps-réel ne permet pas d’avoir une connaissance complète des instructions exécutées sur le processeur. Enfin, les méthodes de développement actuelles, approche incrémentale ou multi-programmation, peuvent nécessiter de traiter des parties de code non encore développées sous forme de bouchon : il faudra prendre en compte les caractéristiques temporelles prévisionnelles du code manquant. Toutes ces contraintes amènent à réviser l’approche actuelle du calcul du WCET : il n’est plus possible de réaliser une analyse uniforme s’étendant sur tout le programme. Il devient nécessaire de partitionner le programme, de réaliser une analyse locale, quand le code est disponible, puis de composer les résultats partiels pour calculer le WCET total de la tâche. Les parties manquantes, COTS ou code bouchon, seront seulement décrites grâce à un ensemble d’informations suffisantes pour réaliser le calcul du WCET.

Objectif

L’objectif de cette travail est de mettre en oeuvre la stratégie décrite dans le sujet. Cette stratégie inclut l’étude de plusieurs domaines encore largement inexplorés :
- partitionnement utile du programme,
- définition des informations partielles nécessaires au calcul du WCET (état utile du processeur),
- méthode de composition des informations partielles pour obtenir le WCET. Cette étude devrait s’inscrire, mais n’est pas limitée à, l’approche Implicit Path Enumeration Technique qui réalise sa modélisation du comportement temporel du programme sous forme de programmation linéaire entière ou Implicit Path Enumeration. Il reste à démontrer qu’IPET peut effectivement supporter notre stratégie par partitionnement et recomposition.

Finalement, l’étude devra donner lieu à un développement au sein d’OTAWA, un framework dédié au calcul de WCET par analyse statique.

logo-spip E. Saint-James & F. Kordon - Master Informatique - UPMC Valid XHTML 1.0!
Calculé le 7 avril 2020 à 11h41min