L’augmentation de la densité d’intégration des circuits intégrés nous a amené à étudier, dans le cadre du développement de la technologie CMOS 45 nm, les sources de variabilité inhérentes aux procédés de fabrication utilisés pour ce nœud technologique, et à en déterminer les composantes principales,dans le but ultime de permettre la simulation précise de l’impact de la variabilité technologique à la fois au niveau transistor et circuit. Après un état de l’art des sources de variabilité du transistor MOS et des moyens de simulation associés,ce travail s'est orienté sur les fluctuations d'un facteur technologique difficilement accessible à la mesure statistique qu'est le dopage canal. Ensuite le nœud 45 nm a été étudié expérimentalement via un plan d'expériences.Ceci a permis de connaitre les variations naturelles des facteurs technologiques mais surtout les sensibilités des performances électriques vis-à-vis de ces facteurs.Nous avons pu ainsi identifier les causes prépondérantes de variabilité dues au procédé.Enfin, nous proposons d’améliorer la prise en compte des déviations des facteurs process dans les simulations Monte-Carlo et pire-cas appliquées aux modèles compacts au regard de ces observations expérimentales. / Continuous improvement in integrated circuits density of integration lead us to study process-induced variations in the framework of the 45 nm node, and to determine their principal contributions with the ultimate goal being to allow an accurate simulation of both transistor and circuit level variability. This work starts with a study of the state of the art of variability sources of the MOS transistor and associated simulation means. Then it focuses on the fluctuations of the channel doping, which is a difficult factor to measure statistically.After that we study the 45 nm node through a design of experiment which let us learn about natural variations of process factors but mostly about electrical performances sensitivity to those factors.Thanks to that we could identify major causes of process-induced variability at this stage of this node development. At last, with respect to those experimental results, we propose to enhance the taking in account of process variations in Monte-Carlo and corner simulations applied to compact models.

L’essor des réseaux AFDX comme infrastructure de communication entre les équipements de bord des aéronefs civils motive de nombreux travaux de recherche pour réduire les délais de communication tout en garantissant un haut niveau de déterminisme et de qualité de service. Cette thèse traite de l’effet des accolements de trames sur l’End System de réception, notamment sur le buffer interne afin de garantir une non perte de trames et un dimensionnement mémoire optimal. Une modélisation pire cas du flux de trames est réalisée selon une première méthode pessimiste, basée sur un flux de trames périodiques ; puis une seconde, plus optimiste, basée sur des intervalles de réception et un placement de trames itératif. Une étude probabiliste met en œuvre des distributions gaussiennes pour évaluer les probabilités d’occurrences des pires cas d’accolements et apporte un éclairage qui ouvre une discussion sur la pertinence de ne considérer que la modélisation pire cas pour dimensionner le buffer de réception. Un gain mémoire supplémentaire peut être obtenu par la mise en œuvre de la compression sans perte LZW. / The rise of AFDX networks as a communication infrastructure between on-board equipment of civil aircraft motivates many research projects to reduce communication delays while guaranteeing a high level of determination and quality of service. This thesis deals with the effect of the back-ot-back frame reception on the reception End System, in particular, on the internal buffer, in order to guarantee a non-loss of frames and optimal memory dimensioning. A worst-case modeling of the frame flow is carried out according to a first pessimistic method, based on a periodic frame flow. Then a more optimistic method is presented based on the reception intervals and an iterative frame placement. A probabilistic study implements Gaussian distributions to evaluate the occurrence probabilities of the worst back-to-back frames and provides an illumination that opens a discussion on the relevance of not considering the worst-case modeling to size the reception buffer. Additional memory gain can be achieved by implementing LZW lossless compression.

SpaceWire est un standard de réseau embarqué promu par l'Agence Spatiale Européenne qui envisage de l'utiliser comme réseau bord unique dans ses futures satellites. SpaceWire utilise un mécanisme de routage Wormhole pour réduire la consommation mémoire des routeurs et les coûts associés. Cependant,le routage Wormhole peut engendrer des blocages en cascade dans les routeurs et, par conséquent,d'importantes variations des délais de livraison des paquets.Comme le réseau doit être partagé par des flux critiques et non-critiques, les concepteurs réseau ont besoin d'un outil leur permettant de vérifier le respect des contraintes temporelles des messages critiques. Pour réaliser cet outil, nous avons choisi comme métrique une borne supérieure sur le délai pire-cas de bout en bout d'un paquet traversant un réseau SpaceWire. Au cours de la thèse, nous avons proposé trois méthodes permettant de calculer cette borne. Les trois méthodes utilisent des hypothèses différentes et ont chacune des avantages et des inconvénients. D'une part, les deux premières méthodes sont très générales et ne nécessitent pas d'hypothèses restrictives sur le trafic en entrée du réseau. D'autre part, la troisième méthode nécessite des hypothèses plus précises sur le trafic en entrée. Elle est donc moins générale mais donne la plupart du temps des bornes plus serrées que les deux autres méthodes. Dans cette thèse, nous avons appliqué ces différentes méthodes à une architecture de référence fournie par Thales Alenia Space afin d'en comparer les résultats. Nous avons également appliqué ces méthodes à des exemples plus simples afin de déterminer l'influence de différents paramètres sur les bornes fournies par nos méthodes. / The SpaceWire network standard is promoted by the ESA and is scheduled to be used as the sole onboard network for future satellites. SpaceWire uses a wormhole routing mechanism to reduce memoryconsumption and the associated costs. However, wormhole routing can lead to packet blocking in routerswhich creates large variations in end-to-end delays. As the network will be shared by real-time and nonreal-time traffic, network designers require a tool to check that temporal constraints are verified for allthe critical messages. The metric we chose for this tool is an upper-bound on the worst-case end-to-enddelay of a packet traversing a SpaceWire network. This metric is simpler to compute than the exact delayof each packet and provide enough guarantee to the network designers. During the thesis, we designed three methods to compute this upper-bound. The three methods use different assumptions and have different advantages and drawbacks. On the one hand, the first two methods are very general and do not require strong assumptions on the input traffic. On the other hand, the third method requires more specific assumptions on the input traffic. Thus, it is less general but usually gives tighter bounds than the two other methods. In the thesis, we apply those methods to a case study provided by Thales Alenia Space and compare the results. We also compare the three methods on several smaller networks to study the impact of various parameters on their results.

Les codes correcteurs d'erreurs sont utilisés pour reconstituer les données numériques, qui sont sujettes à des altérations lors de leur stockage et de leur transport. Il s'agit là de l'utilisation principale des codes correcteurs mais ils peuvent encore être employés en cryptographie. Ils sont dans ce contexte un outil permettant, entre autres choses, de chiffrer des données et d'authentifier des personnes. Ces différents aspects sont traités dans ce document. Pour commencer, nous étudions la classe de codes cycliques possédant un ensemble de définition de la forme {1, 2^i+1, 2^j+1}, où i et j désignent des entiers positifs distincts. Nous concentrons notre attention sur la caractérisation des codes trois-correcteurs appartenant à cette classe ainsi que sur la distribution de poids de ces codes. Nous améliorons l'algorithme de Schaub, qui donne une minoration de la distance minimale des codes cycliques. Nous mettons en oeuvre cet algorithme pour calculer l'immunité spectrale de fonctions booléennes. Cette quantité est reliée à la distance minimale de codes cycliques et est importante pour garantir la sécurité dans certains cryptosystèmes de chiffrement à flot. Dans un second temps, nous proposons une solution pour accélérer le calcul des racines de polynômes dans des corps finis de caractéristique deux. Ce calcul est la phase la plus lente du déchiffrement des cryptosystèmes de type McEliece basés sur les codes de Goppa binaires classiques. Nous fournissons une analyse de la complexité de l'algorithme sous-jacent baptisé BTZ. Nous achevons nos travaux par une étude des protocoles d'authentification à bas coût, dérivés du protocole HB, en adoptant une approche basée sur le problème du décodage par syndrome, plutôt que par l'approche standard, fondée sur le problème LPN.

Les nouvelles applications sur Internet nécessitent des garanties de qualité de service (QoS) de la part du réseau. Nous nous intéressons à deux paramètres de QoS : le temps de réponse et la gigue de bout-en-bout. Nous proposons un ordonnancement, noté FP/DP, à base de priorités fixes (FP), départageant les paquets ex aequo selon leurs priorités dynamiques (DP). La priorité fixe d'un flux reflète son degré d'importance et sa priorité dynamique est un paramètre temporel. FP/FIFO et FP/EDF sont deux exemples d'ordonnancement FP/DP. Nous déterminons des bornes déterministes sur les paramètres de QoS considérés, en utilisant l'approche par trajectoire. En monoprocesseur, nous améliorons les résultats existants et prouvons que FP/EDF domine FP/FIFO sous certaines conditions. En distribué, nous apportons de nouveaux résultats et montrons que l'approche par trajectoire est beaucoup moins pessimiste que l'approche holistique. Nos résultats sont appliqués dans une architecture DiffServ/MPLS.

Les applications du calcul fractionnaire en automatique se sont considérablement développées ces dernières années, surtout en commande robuste. Ce mémoire est une contribution à la commande robuste des systèmes d'ordre entier à l'aide d'un correcteur PID d'ordre fractionnaire.Le conventionnel régulateur PID, unanimement apprécié pour le contrôle des processus industriels, a été adapté au cas fractionnaire sous la forme PInDf grâce à l'introduction d'un modèle de référence d'ordre non entier, réputé pour sa robustesse vis-à-vis des variations du gain statique.Cette nouvelle structure a été étendue aux systèmes à retard sous la forme d'un Prédicteur de SMITH fractionnaire. Dans leur forme standard, ces correcteurs sont adaptés à la commande des systèmes du premier et du second ordre, avec ou sans retard pur.Pour des systèmes plus complexes, deux méthodologies de synthèse du correcteur ont été proposées, grâce à la méthode des moments et à l'approche retour de sortie.Pour les systèmes dont le modèle est obtenu à partir d'une identification, la boucle fermée doit en outre être robuste aux erreurs d'estimation. Un modèle pire-cas, déduit de la matrice de covariance de l'estimateur et des domaines d'incertitudes fréquentielles, a été proposé pour la synthèse du correcteur.Les différentes simulations numériques montrent l'efficacité de cette méthodologie pour l'obtention d'une boucle fermée robuste aux variations du gain statique et aux incertitudes d'identification. / The application of fractional calculus in automatic control have received much attention these last years, mainly in robust control. This PhD dissertation is a contribution to the control of integer order systems using a fractional order PID controller.The classical PID, well known for its applications to industrial plants, has been adapted to the fractional case as a PInDf controller, thanks to a fractional order reference model, characterized by its robustness to static gain variations.This new controller has been generalized to time delay systems as a fractional SMITH Predictor. In standard case, these controllers are adapted to first and second order systems, with or without a time delay. For more complex systems, two design methodologies have been proposed, based on the method of moments and on output feedback approach.For systems whose model is obtained by an identification procedure, the closed loop has to be robust to estimation errors. So, a worst-case model, derived from the covariance matrix of the estimator and the frequency uncertainty domains, has been proposed for the design of the controller.The different numerical simulations demonstrate that this methodology is able to provide robustness to static gain variations and to identification uncertainties.

Les architectures pluri-coeurs sont plus intéressantes pour concevoir des systèmes en temps réel que les systèmes multi-coeurs car il est possible de les maîtriser plus facilement et d’intégrer un plus grand nombre d’applications, potentiellement de différents niveau de criticité. Dans les systèmes temps réel embarqués, ces architectures peuvent être utilisées comme des éléments de traitement au sein d’un réseau fédérateur car ils fournissent un grand nombre d’interfaces Entrées/Sorties telles que les contrôleurs Ethernet et les interfaces de la mémoire DDR-SDRAM. Aussi, il est possible d’y allouer des applications ayant différents niveaux de criticités. Ces applications communiquent entre elles à travers le réseau sur puce (NoC) du pluri coeur et avec des capteurs et des actionneurs via l’interface Ethernet. Afin de garantir les contraintes temps réel de ces applications, les délais de transmission pire cas (WCTT) doivent être calculés pour les flux entre les coeurs ("inter-core") et les flux entre les coeurs et les interfaces entrées/sorties ("core-to-I/O"). Plusieurs réseaux sur puce (NoCs) ciblant les systèmes en temps réel dur ont été conçus en s’appuyant sur des extensions matérielles spécifiques. Cependant, aucune de ces extensions ne sont actuellement disponibles dans les architectures de réseaux sur puce commercialisés, qui se basent sur la commutation wormhole avec la stratégie d’arbitrage par tourniquet. En utilisant cette stratégie de commutation, différents types d’interférences peuvent se produire sur le réseau sur puce entre les flux. De plus, le placement de tâches des applications critiques et non critiques a un impact sur les contentions que peut subir les flux "core-to-I/O". Ces flux "core-to-I/O" parcourent deux réseaux de vitesses différentes: le NoC et Ethernet. Sur le NoC, la taille des paquets autorisés est beaucoup plus petite que la taille des trames Ethernet. Ainsi, lorsque la trame Ethernet est transmise sur le NoC, elle est divisée en plusieurs paquets. La trame sera supprimée de la mémoire tampon de l’interface Ethernet uniquement lorsque la totalité des données aura été transmise. Malheureusement, la congestion du NoC ajoute des délais supplémentaires à la transmission des paquets et la taille de la mémoire tampon de l’interface Ethernet est limitée. En conséquence, ce comportement peut aboutir au rejet des trames Ethernet. L’idée donc est de pouvoir analyser les délais de transmission pire cas sur les NoC et de réduire leurs délais afin d’éviter ce problème de rejet. Dans cette thèse, nous montrons que le pessimisme de méthodes existantes de calcul de WCTT et les stratégies de placements existantes conduisent à rejeter des trames Ethernet en raison d’une congestion interne sur le NoC. Des propriétés des réseaux utilisant la commutation "wormhole" ont été définies et validées afin de mieux prendre en compte les conflits entre les flux. Une stratégie de placement de tâches qui prend en compte les communications avec les I/O a été ensuite proposée. Cette stratégie vise à diminuer les contentions des flux qui proviennent de l’I/O et donc de réduire leurs WCTTs. Les résultats obtenus par la méthode de calcul définie au cours de cette thèse montrent que les valeurs du WCTT des flux peuvent être réduites jusqu’à 50% par rapport aux valeurs de WCTT obtenues par les méthodes de calcul existantes. En outre, les résultats expérimentaux sur des applications avioniques réelles montrent des améliorations significatives des délais de transmission des flux "core-to-I/O", jusqu’à 94%, sans impact significatif sur ceux des flux "intercore". Ces améliorations sont dues à la stratégie d’allocation définie qui place les applications de manière à réduire l’impact des flux non critiques sur les flux critiques. Ces réductions de WCTT des flux "core-to-I/O" évitent le rejet des trames Ethernet. / Many-core architectures are more promising hardware to design real-time systems than multi-core systems as they should enable an easier mastered integration of a higher number of applications, potentially of different level of criticalities. In embedded real-time systems, these architectures will be integrated within backbone Ethernet networks, as they mostly provide Ethernet controllers as Input/Output(I/O) interfaces. Thus, a number of applications of different level of criticalities could be allocated on the Network-on-Chip (NoC) and required to communicate with sensors and actuators. However, the worst-case behavior of NoC for both inter-core and core-to-I/O communications must be established. Several NoCs targeting hard real-time systems, made of specific hardware extensions, have been designed. However, none of these extensions are currently available in commercially available NoC-based many-core architectures, that instead rely on wormhole switching with round-robin arbitration. Using this switching strategy, interference patterns can occur between direct and indirect flows on many-cores. Besides, the mapping over the NoC of both critical and non-critical applications has an impact on the network contention these core-to-I/O communications exhibit. These core-to-I/O flows (coming from the Ethernet interface of the NoC) cross two networks of different speeds: NoC and Ethernet. On the NoC, the size of allowed packets is much smaller than the size of Ethernet frames. Thus, once an Ethernet frame is transmitted over the NoC, it will be divided into many packets. When all the data corresponding to this frame are received by the DDR-SDRAM memory on the NoC, the frame is removed from the buffer of the Ethernet interface. In addition, the congestion on the NoC, due to wormhole switching, can delay these flows. Besides, the buffer in the Ethernet interface has a limited capacity. Then, this behavior may lead to a problem of dropping Ethernet frames. The idea is therefore to analyze the worst case transmission delays on the NoC and reduce the delays of the core-to-I/O flows. In this thesis, we show that the pessimism of the existing Worst-Case Traversal Time (WCTT) computing methods and the existing mapping strategies lead to drop Ethernet frames due to an internal congestion in the NoC. Thus, we demonstrate properties of such NoC-based wormhole networks to reduce the pessimism when modeling flows in contentions. Then, we propose a mapping strategy that minimizes the contention of core-to-I/O flows in order to solve this problem. We show that the WCTT values can be reduced up to 50% compared to current state-of-the-art real-time packet schedulability analysis. These results are due to the modeling of the real impact of the flows in contention in our proposed computing method. Besides, experimental results on real avionics applications show significant improvements of core-to-I/O flows transmission delays, up to 94%, without significantly impacting transmission delays of core-to-core flows. These improvements are due to our mapping strategy that allocates the applications in such a way to reduce the impact of non-critical flows on critical flows. These reductions on the WCTT of the core-to-I/O flows avoid the drop of Ethernet frames.

La prédictibilité est un aspect important des systèmes temps-réel critiques. Garantir la fonctionnalité de ces systèmespasse par la prise en compte des contraintes temporelles. Les architectures mono-cœurs traditionnelles ne sont plussuffisantes pour répondre aux besoins croissants en performance de ces systèmes. De nouvelles architectures multi-cœurssont conçues pour offrir plus de performance mais introduisent d'autres défis. Dans cette thèse, nous nous intéressonsau problème d’accès aux ressources partagées dans un environnement multi-cœur.La première partie de ce travail propose une approche qui considère la modélisation de programme avec des formules desatisfiabilité modulo des théories (SMT). On utilise un solveur SMT pour trouverun chemin d’exécution qui maximise le temps d’exécution. On considère comme ressource partagée un bus utilisant unepolitique d’accès multiple à répartition dans le temps (TDMA). On explique comment la sémantique du programme analyséet le bus partagé peuvent être modélisés en SMT. Les résultats expérimentaux montrent une meilleure précision encomparaison à des approches simples et pessimistes.Dans la deuxième partie, nous proposons une analyse de temps de réponse de programmes à flot de données synchroness'exécutant sur un processeur pluri-cœur. Notre approche calcule l'ensemble des dates de début d'exécution et des tempsde réponse en respectant la contrainte de dépendance entre les tâches. Ce travail est appliqué au processeur pluri-cœurindustriel Kalray MPPA-256. Nous proposons un modèle mathématique de l'arbitre de bus implémenté sur le processeur. Deplus, l'analyse de l'interférence sur le bus est raffinée en prenant en compte : (i) les temps de réponseet les dates de début des tâches concurrentes, (ii) le modèle d'exécution, (iii) les bancsmémoires, (iv) le pipeline des accès à la mémoire. L'évaluation expérimentale est réalisé sur desexemples générés aléatoirement et sur un cas d'étude d'un contrôleur de vol. / Predictability is of paramount importance in real-time and safety-critical systems, where non-functional properties --such as the timing behavior -- have high impact on the system's correctness. As many safety-critical systems have agrowing performance demand, classical architectures, such as single-cores, are not sufficient anymore. One increasinglypopular solution is the use of multi-core systems, even in the real-time domain. Recent many-core architectures, such asthe Kalray MPPA, were designed to take advantage of the performance benefits of a multi-core architecture whileoffering certain predictability. It is still hard, however, to predict the execution time due to interferences on sharedresources (e.g., bus, memory, etc.).To tackle this challenge, Time Division Multiple Access (TDMA) buses are often advocated. In the first part of thisthesis, we are interested in the timing analysis of accesses to shared resources in such environments. Our approach usesSatisfiability Modulo Theory (SMT) to encode the semantics and the execution time of the analyzed program. To estimatethe delays of shared resource accesses, we propose an SMT model of a shared TDMA bus. An SMT-solver is used to find asolution that corresponds to the execution path with the maximal execution time. Using examples, we show how theworst-case execution time estimation is enhanced by combining the semantics and the shared bus analysis in SMT.In the second part, we introduce a response time analysis technique for Synchronous Data Flow programs. These are mappedto multiple parallel dependent tasks running on a compute cluster of the Kalray MPPA-256 many-core processor. Theanalysis we devise computes a set of response times and release dates that respect the constraints in the taskdependency graph. We derive a mathematical model of the multi-level bus arbitration policy used by the MPPA. Further,we refine the analysis to account for (i) release dates and response times of co-runners, (ii)task execution models, (iii) use of memory banks, (iv) memory accesses pipelining. Furtherimprovements to the precision of the analysis were achieved by considering only accesses that block the emitting core inthe interference analysis. Our experimental evaluation focuses on randomly generated benchmarks and an avionics casestudy.

L'analyse statique de programme a pour but de prouver automatiquement qu'un programme vérifie certaines propriétés. L'interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l'ordre d'itération utilisés pendant le calcul d'invariants. Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l'analyse.Habituellement, l'interprétation abstraite consiste en un calcul de point fixe d'un opérateur obtenu après convergence d'une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d'améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement. L'interprétation abstraite peut égalementêtre rendue plus précise en distinguant tous les chemins d'exécution du programme, au prix d'une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d'utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d'itération de l'état de l'art pour obtenir des analyses plus précises.Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d'erreur. Notre technique a différents usages: elle permet de montrer qu'un état d'erreur est inatteignable, mais également d'inférer des préconditions aux boucles et aux fonctions.Nous appliquons nos méthodes d'analyse statique à l'estimation du temps d'exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d'exprimer ce problème via optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l'ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique. Enfin, nous présentons l'implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté. / Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. In this thesis, we propose several improvements on the abstract interpretation framework that enhance the overall precision of the analysis.Usually, abstract interpretation consists in computing an ascending sequence with widening, which converges towards a fixpoint which is a program invariant; then computing a descending sequence of correct solutions without widening. We describe and experiment with a method to improve a fixpoint after its computation, by starting again a new ascending/descending sequence with a smarter starting value. Abstract interpretation can also be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. Satisfiability modulo theories (SMT), whose efficiency has been considerably improved in the last decade, allows sparse representations of paths and sets of paths. We propose to combine this SMT representation of paths with various state-of-the-art iteration strategies to further improve the overall precision of the analysis.We propose a second coupling between abstract interpretation and SMT in a program verification framework called Modular Path Focusing, that computes function and loop summaries by abstract interpretation in a modular fashion, guided by error paths obtained with SMT. Our framework can be used for various purposes: it can prove the unreachability of certain error program states, but can also synthesize function/loop preconditions for which these error states are unreachable.We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis.We finally describe the design and the implementation of Pagai,a new static analyzer working over the LLVM compiler infrastructure,which computes numerical inductive invariants using the various techniques described in this thesis.Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages and benchmarks used in the community.

Le Network Calculus est une théorie visant à calculer des bornes pire-cas sur les performances des réseaux de communication. Le réseau est modélisé par un graphe orienté où les noeuds représentent des serveurs, et les flux traversant le réseau doivent suivre les arcs. S'ajoutent à cela des contraintes sur les courbes de trafic (la quantité de données passées par un point depuis la mise en route du réseau) et sur les courbes de service (la quantité de travail fournie par chaque serveur). Pour borner les performances pire-cas, comme la charge en différents points ou les délais de bout en bout, ces enveloppes sont combinées à l'aide d'opérateurs issus notamment des algèbres tropicales : min, +, convolution-(min, +)... Cette thèse est centrée sur l'algorithmique du Network Calculus, à savoir comment rendre effectif ce formalisme. Ce travail nous a amené d'abord à comparer les variations présentes dans la littérature sur les modèles utilisés, révélant des équivalences d'expressivité comme entre le Real-Time Calculus et le Network Calculus. Dans un deuxième temps, nous avons proposé un nouvel opérateur (min, +) pour traiter le calcul de performances en présence d'agrégation de flux, et nous avons étudié le cas des réseaux sans dépendances cycliques sur les flux et avec politique de service quelconque. Nous avons montré la difficulté algorithmique d'obtenir précisément les pires cas, mais nous avons aussi fourni une nouvelle heuristique pour les calculer. Elle s'avère de complexité polynomiale dans des cas intéressants. / Network Calculus is a theory aiming at computing worst-case bounds on performances in communication networks. The network is usually modelled by a digraph : the servers are located on the nodes and the flows must follow path in the digraph. There are constraints on the trafic curves (how much data have been through a given point since the activation of the network) and on the service curves (how much work each server may provide). To derive bounds on the worst-case performances, as the backlog or the end-to-end delay, these envelopes are combined thanks to tropical algebra operators: min, +, convolution... This thesis focuses on Network Calculus algorithmics, that is how effective is this formalism. This work led us to compare various models in the litterature, and to show expressiveness equivalence between Real-Time Calculus and Network Calculus. Then, we suggested a new (min, +) operator to compute performances bounds in networks with agregated flows and we studied feed-forward networks under blind multiplexing. We showed the difficulty to compute these bounds, but we gave an heuristic, which is polynomial for interesting cases.