La vérification formelle de systèmes concurrents temps réels se heurte au problème de l'explosion du nombre d'états à explorer. Ce problème connu sous le nom ``d'explosion combinatoire'' à plusieurs causes. Cette thèse s'intéresse à deux d'entre-elles. · Pour lutter contre l'explosion due à la représentation du parallélisme par l'entrelacement d'actions, cette thèse propose des techniques basées sur l'approche des ordres-partiels pour construire un graphe réduit. Pour exploiter les ordres-partiels, les techniques proposées utilisent la construction de « pas de transitions » afin de limiter le nombre d'états explorés. Différentes constructions des « pas de transitions » sont proposées en fonction de la classe de propriétés que l'on souhaite préserver (Blocages, Équivalence de traces, LTL). · Pour lutter contre l'explosion due aux contraintes temporelles, cette thèse propose une approche par sur-approximation du comportement. L'objectif est d'avoir un graphe abstrait du comportement de la sur-approximation plus petit que celui du système. Comme classiquement, les techniques d'abstractions permettent d'obtenir une procédure de décision semi-effective. Lorsque l'analyse de la sur-approximation ne permet pas de conclure, la thèse propose une méthode effective permettant de conclure pour les formules de LTL: le système est analysé, guidé par les résultats obtenus sur la sur-approximation. Cette thèse présente les algorithmes de ces différentes techniques de réduction et l'outil tina (http://www.laas.fr/tina) dans lequel ils ont été implémentés.

Le processus de développement des systèmes avioniques suit des réglementations de sûreté de fonctionnement très strictes, incluant l'analyse du déterminisme et de la prédictibilité temporelle des systèmes. L'approche est basée sur la séparation des étapes de conception et d'implémentation. Une des plus grandes difficultés dans l'approche actuelle se trouve dans la détermination du WCET, qui est nécessaire pour prouver la satisfaction des contraintes de temps-réel dur du système. Dans cette thèse, une méthodologie de relâchement de contraintes temps-réels pour les systèmes de commandes digital est proposé. L'objectif est de réduire le conservatisme des approches traditionnelles basés sur le pire temps d'exécution, tout en préservant la stabilité et les performances de commandes. L'approche a été appliqué au système de commande de tangage d'un avion, ce qui a permi de montrer que le relâchement des contraintes temps réels améliore l'utilisation de la puissance de calcul disponible tout en préservant la stabilité et la qualité de commande du système.

Afin de garantir qu'un programme respectera toutes ses contraintes temporelles, nous devons être capable de calculer une estimation fiable de son temps d'exécution au pire cas (WCET: worst case execution time). Cependant, identifier une borne précise du pire temps d'exécution devient une tâche très complexe du fait de la sophistication croissante des processeurs. Ainsi, l'objectif de nos travaux de recherche a été de définir une méthode formelle qui puisse s'adapter aux évolutions du matériel. Cette méthode consiste à développer un modèle du processeur cible, puis à l'exécuter symboliquement afin d'associer à chaque trace d'exécution un temps d'exécution au pire cas. Une méthode de fusionnement est également prévue afin d'éviter une possible explosion combinatoire. Cette méthode a pour principale contrainte de ne pas introduire trop d'imprécision sur les temps calculés.

Le processus de développement des systèmes avioniques suit des réglementations de sûreté de fonctionnement très strictes, incluant l'analyse du déterminisme et de la prédictibilité temporelle des systèmes. L'approche est basée sur la séparation des étapes de conception et d'implémentation. Une des plus grandes difficultés dans l'approche actuelle se trouve dans la détermination du WCET, qui est nécessaire pour prouver la satisfaction des contraintes de temps-réel dur du système. Dans cette thèse, une méthodologie de relâchement de contraintes temps-réels pour les systèmes de commandes digital est proposé. L'objectif est de réduire le conservatisme des approches traditionnelles basés sur le pire temps d'exécution, tout en préservant la stabilité et les performances de commandes. L'approche a été appliqué au système de commande de tangage d'un avion, ce qui a permi de montrer que le relâchement des contraintes temps réels améliore l'utilisation de la puissance de calcul disponible tout en préservant la stabilité et la qualité de commande du système. / The development process of critical avionics products are done under strict safety regulations. These regulations include determinism and predictability of the systems' timing. The overall approach is based on a separation of concerns between control design and implementation. One of the toughest challenges in the current approach is the determination of the WCET, in order to correctly size the system. In this thesis, a weakened implementation scheme for real-time feedback controllers is proposed to reduce the conservatism due to traditional worst-case considerations, while preserving the stability and control performance. The methodology is tested to the pitch control of an aircraft, showing that weakening the real-time constraints allows for saving computing power while preserving the system's stability and quality of control.

Afin de garantir qu'un programme respectera toutes ses contraintes temporelles, nous devons être capable de calculer une estimation fiable de son temps d'exécution au pire cas (WCET: worst case execution time). Cependant, identifier une borne précise du pire temps d'exécution devient une tâche très complexe du fait de la sophistication croissante des processeurs. Ainsi, l'objectif de nos travaux de recherche a été de définir une méthode formelle qui puisse s'adapter aux évolutions du matériel. Cette méthode consiste à développer un modèle du processeur cible, puis à l'exécuter symboliquement afin d'associer à chaque trace d'exécution un temps d'exécution au pire cas. Une méthode de fusionnement est également prévue afin d'éviter une possible explosion combinatoire. Cette méthode a pour principale contrainte de ne pas introduire trop d'imprécision sur les temps calculés. / To ensure that a program will respect all its timing constraints we must be able to compute a safe estimation of its worst case execution time (WCET). However with the increasing sophistication of the processors, computing a precise estimation of the WCET becomes very difficult. In this report, we propose a novel formal method to compute a precise estimation of the WCET that can be easily parameterized by the hardware architecture. Assuming that we developed an executable timed model of the hardware, we use symbolic execution to precisely infer the execution time for a given instruction flow. We also merge the states relying on the loss of precision we are ready to accept, in order to avoid a possible states explosion.

Ce mémoire présente une nouvelle approche pour le calcul de temps d'exécution au pire (WCET) de tâche temps-réel critique, en particulier en ce qui concerne les aléas dus aux caches mémoire. Le point général est fait sur la problématique et l'état de l'art en la matière, mais l'accent est mis sur la théorie elle-même et son formalisme, d'abord dans le cadre monotâche puis dans le cadre multitâche. La méthode utilisée repose sur une technique d'interprétation abstraite, comme la plupart des autres méthodes de calcul de WCET, mais le formalisme est dans une approche probabiliste (bien que déterministe dans le cadre monotâche) de par l'utilisation de chaînes de Markov. La généralisation au cadre multitâche utilise les propriétés proba- bilistes pour faire une évaluation pessimiste d'un WCET et d'un écart type au pire, grâce à une modification astucieuse du propagateur dans ce cadre. Des premières évaluations du modèle, codées à la main à partir des résultats de compilation d'applications assez simples montrent des résultats promet- teurs quant à l'application du modèle sur des programmes réels en vraie grandeur.