Un système temps réel est un système informatique soumis à des contraintes de temps, et en particulier à des échéances. Les systèmes temps réels critiques sont une sous-classe de ces systèmes qui doivent impérativement respecter leurs échéances. Dans ce genre de systèmes, manquer une échéance peut avoir des conséquences catastrophiques pouvant aller jusqu'à la perte de vies humaines. Pour s'assurer que ces systèmes ne manquent jamais leurs échéances, l'analyse de pire temps d'exécution (PTE, ou WCET en anglais) calcule une limite supérieure au temps d'exécution des programmes qui doivent être exécutés. Traditionnellement, l'analyse statique du PTE produit un entier qui représente une borne supérieure au nombre de cycles du processeur nécessaires à l'exécution de ce programme. Cependant, le temps d'exécution d'un programme peut dépendre de paramètres matériels, l'état du cache notamment, ou de paramètres logiciels, comme les paramètres d'entrée du programme. Calculer un seul PTE sous la forme d'un entier, peu importe la valeur des paramètres, est donc souvent pessimiste. Pour résoudre ce problème, l'analyse paramétrique du PTE produit une formule arithmétique qui dépend de différents paramètres choisis. Instancier cette formule avec des valeurs pour chaque paramètre permet d'obtenir un PTE plus précis qui prend en compte la valeur de ces paramètres. Parmi les différentes analyses paramétriques, les techniques à base d'arbres montrent une complexité faible. En effet, elles utilisent une structure arborescente qui peut facilement être transformée en une formule arithmétique, ce qui permet de calculer le PTE en incluant des symboles, et donc des paramètres, de manière efficace. Néanmoins, ces approches ont aussi des inconvénients. Tout d'abord, ces méthodes sont connues pour leurs difficultés à tenir compte des effets des composants matériels sur le PTE. Ensuite, elles montrent également des difficultés à prendre en compte certains aspects sémantiques du programme, qui peuvent avoir un impact conséquent sur le PTE. Finalement, tout comme les autres analyses paramétriques, les paramètres proposés doivent être déterminés par l'utilisateur. Dans cette thèse, nous étendons une technique de calcul symbolique du PTE pour aborder trois problèmes liés à des techniques de calcul de PTE paramétrique: - nous avons développé une technique qui élimine les chemins sémantiquement infaisables de la représentation du programme utilisée pour calculer le PTE; - nous avons adapté une technique existante d'analyse de pipeline, qui fonctionne avec les techniques non paramétriques de calcul du PTE à base de graphes, afin de l'utiliser dans une technique d'analyse paramétrique du PTE utilisant des arbres; - nous avons développé une technique paramétrique qui prend automatiquement en compte les effets des paramètres d'entrée du programme sur le PTE. Cette technique produit une formule dont les paramètres sont les paramètres d'entrée du programme et ne requiert aucune connaissance du programme de la part de l'utilisateur.
M. Giuseppe LIPARI Université de Lille Directeur de thèse. M. Matthieu MOY Université Claude Bernard Lyon 1 Rapporteur. Mme Isabelle PUAUT Université de Rennes 1 Rapporteure. M. Emmanuel GROLLEAU ENSMA Examinateur. M. Julien FORGET Université de Lille Co-directeur de thèse. M. Clément BALLABRIGA Université de Lille Examinateur.
Thèse de l'équipe SyCoMoRES soutenue le 07/11/2023
français
English