Flow fact automata for the expression and the integration of properties in WCET analysis

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.In the domain of critical systems, the analysis of execution times of programs is needed to schedule various task at best and by extension to dimension the whole system. The execution time of a program depends on multiple factors such as entries of the program or the targeted hardware. Yet this time variation is an issue in real-time systems where the duration is required to allow correct processor time to each task, and in this purpose, we need to know their worst-case execution time. In the TRACES team at IRIT, we try to compute a safe upper bound of this worst-case execution time that would be as precise as possible. In order to do so, we work on the control flow graph of a program that represents an over-set of its possible executions and we combine this structure with annotations on specific behaviours of the program that might reduce the over-approximation of our estimation. Tools designed to compute worst-case execution times of programmes usually support the expression and the integration of annotations thanks to specific annotation languages. Our proposal is to replace these languages with a type of automata named flow fact automata so that not only the expression but also the integration of annotations in the analysis inherit from the formal basis of automata. Based on these automata enriched with constraints, variables and a hierarchy, we show how they support the various annotation types used in the worst-case execution time domain. Additionally, the integration of annotations in an analysis usually lead to associate numerical constraint to the control flow graph. The automata presented here support this method but their expressiveness offers new integration possibilities based on the partial unfolding of control flow graph. We present experimental results from the comparison of these two methods that show how the graph unfolding can improve the analysis precision. In the end, this precision gain in the worst-case execution time will ensure a better usage of the hardware as well as the absence of risks for the user or the system itself