Cette thèse s'intéresse aux effets des attaques par fautes physiques sur le code d'un système embarqué en particulier la carte à puce. De telles attaques peuvent compromettre la sécurité du système en donnant accès à des informations confidentielles, en compromettant l'intégrité de données sensibles ou en perturbant le fonctionnement pendant l'exécution. Dans cette thèse, nous décrivons des propriétés de sécurité permettant d'exprimer les garanties du système et établissons un modèle d'attaque de haut niveau définissant les capacités d'un attaquant à modifier le système. Ces propriétés et ce modèle nous servent à vérifier la sécurité du code par analyse statique ou test dynamique, combinés avec l'injection d'attaques, simulant les conséquences logicielles des fautes physiques. Deux méthodologies sont ainsi développées afin de vérifier le comportement fonctionnel du code sous attaques, tester le fonctionnement des sécurités implémentées et identifier de nouvelles attaques. Ces méthodologies ont été mises en oeuvre dans un cadre industriel afin de faciliter le travail du développeur chargé de sécuriser un code de carte à puce.

On considère souvent IEEE 802.11 comme la technologie sous-jacente aux réseaux sans fil multisauts. Pourtant, dans de tels réseaux, 802.11 s'avère inefficace et/ou inéquitable dans de nombreuses situations. Cette thèse décrit un algorithme d'allocation dynamique et distribuée de débit permettant de garantir un partage équitable de la bande passante entre flux, tout en assurant une utilisation efficace du réseau. De plus, cette thèse propose une nouvelle méthode d'évaluation de l'efficacité d'un protocole en prenant en compte l'expérience utilisateur.

Les systèmes embarqués sont des équipements électroniques et informatiques, soumis à de nombreuses contraintes et dont le fonctionnement doit être continu. Pour définir le comportement de ces systèmes, les modèles de programmation dataflows sont souvent utilisés. Ce choix de modèle est motivé d'une part, parce qu'ils permettent de décrire un comportement cyclique, nécessaire aux systèmes embarqués ; et d'autre part, parce que ces modèles s'apprêtent à des analyses qui peuvent fournir des garanties de fonctionnement et de performance essentielles. La société Kalray propose une architecture embarquée, le MPPA. Il est accompagné du langage de programmation ΣC. Ce langage permet alors de décrire des applications sous forme d'un modèle dataflow déjà très étudié, le modèle Cyclo-Static Dataflow Graph(CSDFG). Cependant, les CSDFG générés par ce langage sont souvent trop complexes pour permettre l'utilisation des techniques d'analyse existantes. L'objectif de cette thèse est de fournir des outils algorithmiques qui résolvent les différentes étapes d'analyse nécessaires à l'étude d'une application ΣC, mais dans un temps d'exécution raisonnable, et sur des instances de grande taille. Nous étudions trois problèmes d'analyse distincts : le test de vivacité, l'évaluation du débit maximal, et le dimensionnement mémoire. Pour chacun de ces problèmes, nous fournissons des méthodes algorithmiques rapides, et dont l'efficacité a été vérifiée expérimentalement. Les méthodes que nous proposons sont issues de résultats sur les ordonnancements périodiques ; elles fournissent des résultats approchés et sans aucune garantie de performance. Pour pallier cette faiblesse, nous proposons aussi de nouveaux outils d'analyse basés sur les ordonnancements K-périodiques. Ces ordonnancements généralisent nos travaux d'ordonnancement périodiques et nous permettrons dans un avenir proche de concevoir des méthodes d'analyse bien plus efficaces.

La conception de systèmes embarqués modernes est de plus en plus complexe, car plus de fonctionnalités sont intégrées dans ces systèmes. En même temps, afin de répondre aux exigences de calcul tout en conservant une consommation d'énergie de faible niveau, MPSoCs sont apparus comme les principales solutions pour tels systèmes embarqués. En outre, les systèmes embarqués sont de plus en plus adaptatifs, comme l'adaptabilité peut apporter un certain nombre d'avantages, tels que la flexibilité du logiciel et l'efficacité énergétique. Cette thèse vise la conception sécuritaire de ces MPSoCs adaptatifs. Tout d'abord, chaque configuration de système doit être analysée en ce qui concerne ses propriétés fonctionnelles et non fonctionnelles. Nous présentons un cadre abstraite de conception et d'analyse qui permet des décisions d'implémentation rapide et rentable. Ce cadre est conçu comme un support de raisonnement intermédiaire pour les environnements de co-conception de logiciel / matériel au niveau de système. Il peut élaguer l'espace de conception à sa plus grande portée, et identifier les candidats de solutions de conception de manière rapide et efficace. Dans ce cadre, nous utilisons un codage basé sur l'horloge abstraite pour modéliser les comportements du système. Différents scénarios d'applications de mapping et de planification sur MPSoCs sont analysés via les traces d'horloge qui représentent les simulations du système. Les propriétés d'intérêt sont l'exactitude du comportement fonctionnel, la performance temporelle et la consommation d'énergie. Deuxièmement, la gestion de la reconfiguration de MPSoCs adaptatifs doit être abordée. Nous sommes particulièrement intéressés par les MPSoCs implémentés sur des architectures reconfigurables (ex. FPGAs) qui offrent une bonne flexibilité et une efficacité de calcul pour les MPSoCs adaptatifs. Nous proposons un cadre général de conception basé sur la technique de la synthèse de contrôleurs discrets (DCS) pour résoudre ce problème. L'avantage principal de cette technique est qu'elle permet une synthèse d'un contrôleur automatique selon une spécification des objectifs de contrôle. Dans ce cadre, le comportement de reconfiguration du système est modélisé en termes d'automates synchrones en parallèle. Le problème de calcul de la gestion reconfiguration selon de multiples objectifs concernant, par exemple, les usages des ressources, la performance et la consommation d'énergie, est codé comme un problème de DCS. Le langage de programmation BZR existant et l'outil Sigali sont employés pour effectuer DCS et générer un contrôleur qui satisfait aux exigences du système. Finalement, nous étudions deux façons différentes de combiner les deux cadres de conception proposées pour MPSoCs adaptatifs. Tout d'abord, ils sont combinés pour construire un flot de conception complet pour MPSoCs adaptatifs. Deuxièmement, ils sont combinés pour présenter la façon dont le manager run-time calculé par le second cadre peut être intégré dans le premier cadre afin de réaliser des simulations et des analyses combinées de MPSoCs adaptatifs.

En C, une stratégie classique pour implémenter les codes de gestion d'erreur est de faire suivre chaque opération qui peut générer une erreur d'une structure conditionnelle qui teste si l'opération a renvoyé une erreur. Ce stratégie basique, cependant, est sujette à erreurs, et il est courant d'oublier des opérations de nettoyage requises, ainsi que d'oublier de mettre à jour des codes de gestion d'erreur existants lorsque la fonction est étendue avec de nouvelles opérations. De plus, une partie importante du code doit souvent être dupliquée. Un style de programmation, <EM> stratégie goto </EM>, qui peut réduire en partie certaines de ces difficultés. Pour améliorer la structure des codes de gestion d'erreur dans les logiciels système, nous définissions un algorithme qui permet de transformer les codes de gestion d'erreur implémentés suivant la stratégie basique en codes de gestion d'erreur qui utilisent la <EM> stratégie goto</EM>. Même lorsque les codes de gestion d'erreurs sont structurés, la gestion et la libération des ressources allouées restent un problème lorsqu'il s'agit d'assurer la robustesse du code système. Dans cette thèse, nous proposons un algorithme <EM> microscopique </EM> de détection d'omission de libération de ressource, basé sur une analyse principalement intra-procédurale, qui prend en compte les flux et les chemins du code et qui cible et exploite les propriétés des codes de gestion d'erreur. Notre algorithme est résistant aux faux positifs dans l'ensemble des acquisitions de ressources et des opérations de libération, ce qui produit un faible taux de faux positifs dans les rapports renvoyés par l'outil tout en passant à l'échelle.

Dans le but d'établir un modèle prédictif pour la croissance tumorale in-vivo et la thérapie, le modèle multi-échelle doit être élaboré et calibré par étape et de façon individuelle pour chaque type de cellule ciblé et pour di érents environnements (in-vitro et in-vivo). Nous présenterons, en tant que preuve de concept et à partir de di érentes sources de données, les étapes de la construction et de la paramétrisation du modèle de la croissance avasculaire des lignées de cellules EMT6/Ro et SK-MES-1. Dans une première étape, un modèle multi-échelle à base d'agents a été construit et validé avec des données provenant de la littérature sur les sphéroïdes multicellulaires de carcinomes mammaires de souris EMT6/Ro. Pour cette lignée de cellules, il a pu prédire que la cinétique de croissance est contrôlée par une combinaison de contraintes spatiales et de limitation des nutriments. Il a été trouvé que l'ATP est la ressource critique que les cellules essayent de garder constante en permutant d'un métabolisme aérobique à anaérobique et ce pour de larges plages de concentrations d'oxygène et de glucose. La saturation de la croissance a été observé uniquement dans le cas de faibles concentrations d'oxygène et de glucose ce que le modèle a pu expliqué par une migration guidée par l'adhésion de cellule à cellule. Dans une seconde étape, le modèle a été adapté à la lignée cellulaire SK-MES-1. Nous avons calibré la cinétique de croissance qualitativement en analysant des images de cryosections de sphéroïdes marquées pour l'apoptose et la prolifération et quantitativement en la comparant des courbes de croissance. Au delà de l'ATP, le lactate a été identi é comme contrôlant la taille du noyau nécrotique. Pour rendre compte de la situation in-vivo, nous proposons une extension du modèle qui prend en compte un réseau de vaisseaux sanguins et le phénomène de l'angiogenèse associé. A n de paramétrer les propriétés des vaisseaux fonctionnels et dans le but de valider les lois de l'angiogenèse, nous menons à partir d'images de perfusion d'agents de contraste une étude de sensibilité aux paramètres. Dans un premier temps, nous résolvons le problème direct de la perfusion des agents de contraste dans un réseau de vaisseaux perméables ou non. Ensuite, nous résolvons le problème inverse rigoureusement et, grâce à des comparaisons directes entre les paramètres originaux et ceux récupérés, nous étudions la capacité de prédiction du modèle dans di érents cas.

Cette thèse apporte une contribution à la compréhension des dynamiques de marché et à la prise de décision des traders à l'aide d'une plateforme de simulation de marchés multi-agents. La modélisation multi-agents permet notamment d'étudier le système boursier comme un système complexe évolutif dans lequel chaque trader artificiel possède son propre comportement possède son propre comportement et qui, par ses prises de décision, influence l'ensemble des autres acteurs du système. Dans une première partie, nous mettons en évidence à l'aide de "traders à intelligence zéro" (ZIT), le rôle de la microstructure pour comprendre la nature des principaux faits stylisés de l'évolution des prix. Les résultats issus de nombreuses simulations, indiquent que l'usage des ZIT n'est pas suffisant pour reproduire de façon convaincante les évolutions de prix réels, car ceux-ci doivent être appréhendés à la fois de manière qualitative mais aussi quantitative. Nous montrons que seuls des éléments de stratégies de trading et une forte calibration peuvent améliorer cette réplication par simulation, suggérant que les aspects comportementaux importent tout autant que les aspects micro structurels. Dans une seconde partie, nous concentrons notre recherche sur la problématique de la rationalité dans le corpus de la théorie moderne du portefeuille. Le marché artificiel nous permet de tester si des stratégies naïves peuvent surpasser, en terme de performance, des modèles plus complexes. Diverses stratégies d'investissement sont implémentées dans le système artificiel et mises en interaction afin d'observer leur survie dans des compétitions écologiques basées sur leurs performances relatives. Certaines de ces stratégies d'investissements sont fondées sur des variations du modèle canonique de la théorie de portefeuilles de Markowitz, d'autres suivent des principes de diversification naïfs, d'autres encore obéissent à des combinaisons de stratégies rationnelles sophistiquées et de stratégies naïves. Enfin, de manière à mieux saisir les facteurs qui influent sur la performance du portefeuille, nous montrons les effets de la fréquence de pondération et des préférences pour le risque des investisseurs sur l'issue de ces compétitions. Pour finir, afin de fournir une mesure de performance absolue orientée vers l'évaluation ex-post d'un large éventail de stratégies de trading des investisseurs (agents dans notre cas) nous proposons un nouvel algorithme de complexité polynomiale permettant de déterminer la borne supérieure absolue des profits atteignables pour n'importe quelle stratégie sur une période de temps donnée. Cet algorithme met en contact deux champs a priori éloignés: la théorie des graphes d'une part et la finance computationnelle d'autre part.

Les simulations par agents, ou centrées individu, permettent, par opposition aux modèles centrés groupe, de prendre en compte la manière dont les entités composant un sys- tème interagissent entre elles et ainsi de faire le lien entre ses niveaux microscopiques et macroscopiques. Les marchés financiers, bien qu'étant des systèmes composés de nombreuses entités en interaction, sont souvent étudiés à l'aide de modèle centrés groupe, qui montrent leur limites lorsqu'il s'agit d'expliquer l'émergence de certains phénomènes observables dans les séries de prix. Nous proposons par conséquent un modèle de marché financier centré individu, permettant de reproduire de manière réaliste leur fonctionnement, à la fois à une échelle intra-journalière et à une échelle inter-journalière. Ce modèle nous a permis dans un premier temps de proposer une théorie pour expliquer l'origine des faits stylisés, qui sont des propriétés statistiques des cours de prix observables sur l'ensemble des marchés financiers et dont l'origine est mal expliquée. Notre proposition, étayée par les expérimentations que nous avons réalisées avec notre modèle, montre que les faits stylisés semblent en majeure partie causés par la manière dont le marché est structuré et par la manière dont les agents économiques interagissent à travers lui. Dans un second temps, nous avons utilisé notre modèle pour étudier les variations extrêmes de prix observables sur les marchés financiers, que l'on nomme "bulles" quand elles sont à la hausse et "krachs" quand elles sont à la baisse. Nous avons illustré avec notre modèle, en nous appuyant sur les théories proposées par certains économistes pour expliquer ces événéments, que ces épisodes critiques dans les prix peuvent survenir lorsqu'une partie suffisante de la population des investisseurs adopte une stratégie spéculatrice.

Der vierte Band der wissenschaftlichen Schriftenreihe Eingebettete Selbstorganisierende Systeme widmet sich der Entwicklung von Fehlermodellen für eingebettete, verteilte Multi – Prozessorsysteme. Diese werden zu einem hierarchischen Netzwerk zur Steuerung von Flugzeugen (Avionik) verbunden und mehr und mehr im Automotive Bereich eingesetzt. Hier gilt es höchste Sicherheitsstandards einzuhalten und maximale Verfügbarkeit zu garantieren. Herr Fischer integriert die Modellierung von möglichen Fehlern in den Entwurfsprozess. Auf Grundlage des π-Kalküls entwickelt Herr Fischer ein formales Fehlermodell, das eine einheitliche Modellierung von Fehlerfällen unterstützt. Dabei werden interessante Bezüge zur Bi-Simulation sowie zu Methoden des Modell Checkings hergestellt. Die theoretischen Ergebnisse werden an einem komplexen Beispiel anschaulich illustriert. So kann der Leser die Mächtigkeit des entwickelten Ansatzes nachvollziehen und wird motiviert, die entwickelte Methodik auf weitere Anwendungsfälle zu übertragen. / The 4th volume of the scientific series Eingebettete, selbstorganisierende Systeme (Embedded Self-Organized Systems) outlines the design of fault models for embedded distributed multi processor systems. These multi processor systems will be connected to a hierarchical network to control airplanes (avionics) and also be used more and more in the automotive area. Here it is essential to meet highest safety standards and to ensure the maximum of availability. Mr Fischer integrates the modelling of potential faults into the design process. Based on the pi-calculus, he develops a formal framework, which supports a standardised modelling of faults. Thereby, interesting connections to the Bi-Simulation as well as to methods of the Model checking are established. The theoretical results are depicted on a complex example. So it is possible for the reader to understand the complexity of this approach and is motivated to use the developed methodology in other applications. I am glad that Mr Fischer publishes his important research in this scientific series.

Reliability in terms of functional properties from the safety-liveness spectrum is an indispensable requirement of low-level operating-system (OS) code. However, with evermore complex and thus less predictable hardware, quantitative and probabilistic guarantees become more and more important. Probabilistic model checking is one technique to automatically obtain these guarantees. First experiences with the automated quantitative analysis of low-level operating-system code confirm the expectation that the naive probabilistic model checking approach rapidly reaches its limits when increasing the numbers of processes. This paper reports on our work-in-progress to tackle the state explosion problem for low-level OS-code caused by the exponential blow-up of the model size when the number of processes grows. We studied the symmetry reduction approach and carried out our experiments with a simple test-and-test-and-set lock case study as a representative example for a wide range of protocols with natural inter-process dependencies and long-run properties. We quickly see a state-space explosion for scenarios where inter-process dependencies are insignificant. However, once inter-process dependencies dominate the picture models with hundred and more processes can be constructed and analysed.