Détermination des pire-temps d’exécution (WCET) pour des plateformes embarquées par analyse statique

Nowadays real-time systems are omnipresent and embedded systems thrive in a variety of application fields. When they are integrated into safety-critical systems, the verification of their properties becomes a crucial part. Dependability is a primary design goal in environments that use hard real-time systems, whereas general-use microprocessors were designed with a high performance goal. The average-throughput maximization design choice is intrinsically opposed to design goals such as dependability that benefit mostly from highly deterministic architectures without local optimizations. Besides the growth in complexity of the embedded systems, platforms are getting more and more heterogeneous. With regard to the respect of the timing constraints, real-time systems are classified in two categories: hard real-time systems (the non respect of a deadline can lead to catastrophic consequences) and soft real-time systems (missing a deadline can cause performance degradation and material loss). We analyze hard real-time systems that need precise and safe determination of the worst-case execution time bounds in order to be certified.The validation of their non-functional properties is a complex and resource consuming task. One of the main reasons is that currently available solutions focus on delivering precise estimations through tools that are highly dependent on the underlying platform (in order to provide precise and safe results, the architecture of the system must be taken into account).In this thesis we address the above issues by introducing a timing analysis method that maintains a good level of precision while being applicable to a variety of platforms. This adaptability is achieved through separating as much as possible the worst-case execution time (WCET) estimation from the model of the hardware. Our approach consists in the introduction of a new formal modeling language that captures the complex behaviour of modern hardware and is guided by the timing analysis in order to achieve the needed precision to scalability tradeoff. The analysis drives a conjoint symbolic execution of the program's binary and the processor model using a dynamic prediction module that decides what states to merge in order to limit the state space explosion. Several state merging algorithms are introduced and applied that can also give an estimation of the introduced precision loss.La détermination précise de pires temps d’exécution (WCET) est un sujet de grand intérêt pour les systèmes embarqués critiques. Le sujet de la Thèse adresse des problèmes qui ne sont pas résolus dans la littérature notamment l’inertie notable dans le changement de plateformes cibles des analyseurs existants et la perte de précision lors du passage à l’échelle. Nos travaux se concentrent justement sur une souplesse au changement du processeur à analyser et la maitrise de la perte de précision à l’aide d’un nouvel langage de modélisation du matériel qui se trouve en étroit lien avec l’analyseur même.Une estimation sûre du WCET nécessite la prise en compte du matériel sur lequel le programme est exécuté. Les processeurs embarqués dans les systèmes critiques présentent des composants qui ont été conçus non pas pour faciliter leur analyse mais pour maximiser les performances moyennes, introduisant une variabilité temporelle significative. Le temps d'exécution est donc dépendent, entre autres des valeurs effectives de données mais aussi de l'historique d'exécution. Le but étant d'estimer le pire temps d'exécution, l'option de supposer qu'à chaque fois l'optimisation ne se produit pas et que le pire temps possible est nécessaire conduit à une surestimation trop importante. A ce problème se rajoute aussi le fait que nous ne pouvons pas supposer qu'un pire temps local (par exemple le nombre de cycles pendant une micro-opération du pipeline) contribuera au vrai pire temps global à cause des anomalies temporelles des processeurs. Tous les chemins d'exécution, engendrés par la totalité des entrées possibles doivent donc être analysés. Le fait de devoir gérer cette explosion combinatoire, nous a guidé dans les choix de conception du modèle utilisé pour simuler le processeur. Nous avons conçu une méthode de spécification et d'analyse de systèmes, basée sur la méthode des abstract state machines (ASM). L'extension HiTAsm consiste en l'incorporation des notions de hiérarchie et de temporalité, pour pouvoir gérer l'explosion combinatoire en choisissant une définition d'un composant parmi plusieurs niveaux d'abstraction possibles et pour pouvoir estimer le temps écoulé entre chaque transition des états du système. Cela permet l'estimation de la consommation temporelle et la variation dynamique du niveau d'abstraction du système analysé, afin d'analyser un grand nombre d'états, tout en minimisant la perte de précision. Le modèle du processeur et l'analyseur sont complètement séparés, ce qui est nécessaire pour rendre l'outil adaptable aux changements de plateforme. L'analyseur est basé sur une exécution symbolique conjointe du binaire et du modèle de processeur spécifié avec HiTAsm. En partant des valeurs symboliques, toutes les entrées possibles du binaire sont analysées, en utilisant des sur-approximations uniquement quand c'est nécessaire de manière à minimiser la perte de précision et fournir le pire-temps d’exécution du programme le plus proche de la valeur théorique