La plupart des langages de programmation de haut niveau s'exécutent sur une machine virtuelle (VM) pour être indépendant du hardware utilisé. Pour atteindre de hautes performances, la VM repose généralement sur un compilateur à la volée (JIT), qui spécule sur le comportement du programme basé sur ses premières exécutions pour générer à la volée du code machine efficace et accélérer l'exécution du programme. Étant donné que plusieurs exécutions sont nécessaires pour spéculer correctement sur le comportement du programme, une telle VM nécessite un certain temps au démarrage pour atteindre les performances maximales. Le JIT est habituellement compilé en code exécutable avec le reste de la VM avant sa première utilisation. La thèse propose Sista, une architecture pour un JIT, dans laquelle l'état optimisé de la VM peut être persisté entre plusieurs démarrages de la VM et le JIT s'exécute dans le même environnement d'exécution que le programme exécuté. Pour ce faire, le JIT est divisé en deux parties. Une partie est de haut niveau: elle effectue des optimisations spécifiques au langage de programmation exécuté par la VM et est méta-circulaire. Sans connaissances des détails de bas niveau, cette partie peut être lue, éditée et déboguée pendant le fonctionnement du programme en utilisant les outils de développement du langage de programmation exécuté par la VM. La deuxième partie est de bas niveau: elle effectue des optimisations spécifiques au hardware utilisé et est compilée en code exécutable, au sein de la VM, avant sa première utilisation. Les deux parties du JIT utilisent une représentation intermédiaire bien définie pour échanger le code à optimiser. Cette représentation est indépendante du hardware utilisé et peut être persistée entre plusieurs démarrages de la VM, ce qui permet à la VM d'atteindre rapidement les performances maximales. Pour valider l'architecture, la thèse inclus la description d'une implémentation utilisant Pharo Smalltalk et sa VM. L'implémentation est évaluée par rapport à différents indices de performance, incluant l'exécution de programme utilisés en entreprise et de petits programmes utilisés pour mesurer la performance d'aspects spécifiques de la VM. Le JIT est implémenté selon l'architecture proposée et permet d'exécuter le programme jusqu'à 5x plus vite que la VM en production aujourd'hui. En outre, les indices de performance montrent que les performances maximales peuvent être atteintes presque immédiatement après le démarrage de la VM si cette dernière peut réutiliser l'état optimisé d'une autre exécution. / Most high-level programming languages run on top of a virtual machine (VM) to abstract away from the underlying hardware. To reach high-performance, the VM typically relies on an optimising just-in-time compiler (JIT), which speculates on the program behavior based on its first runs to generate at runtime efficient machine code and speed-up the program execution. As multiple runs are required to speculate correctly on the program behavior, such a VM requires a certain amount of time at start-up to reach peak performance. The optimising JIT itself is usually compiled ahead-of-time to executable code as part of the VM. The dissertation proposes Sista, an architecture for an optimising JIT, in which the optimised state of the VM can be persisted across multiple VM start-ups and the optimising JIT is running in the same runtime than the program executed. To do so, the optimising JIT is split in two parts. One part is high-level: it performs optimisations specific to the programming language run by the VM and is written in a metacircular style. Staying away from low-level details, this part can be read, edited and debugged while the program is running using the standard tool set of the programming language executed by the VM. The second part is low-level: it performs machine specific optimisations and is compiled ahead-of-time to executable code as part of the VM. The two parts of the JIT use a well-defined intermediate representation to share the code to optimise. This representation is machine-independent and can be persisted across multiple VM start-ups, allowing the VM to reach peak performance very quickly. To validate the architecture, the dissertation includes the description of an implementation on top of Pharo Smalltalk and its VM. The implementation is able to run a large set of benchmarks, from large application benchmarks provided by industrial users to micro-benchmarks used to measure the performance of specific code patterns. The optimising JIT is implemented according to the architecture proposed and shows significant speed-up (up to 5x) over the current production VM. In addition, large benchmarks show that peak performance can be reached almost immediately after VM start-up if the VM can reuse the optimised state persisted from another run.

Cette thèse revisite les problèmes d'accessibilité et de vivacité pour les au-tomates temporisés.L'accessibilité est couramment résolue par le calcul d'un arbre de recherche abstrait. L'abstraction est paramétrée par des bornes provenant des gardes de l'automate. Nous montrons que l'abstraction a 4LU de Behrmann et al. est la plus grande abstraction saine et complète pour les bornes LU. N' étant pas convexe, elle n'est pas mise en oeuvre dans les outils. Nous introduisons une méthode qui permet son utilisation éfficace. Finalement, nous proposons une optimisation des bornes à la volée exploitant le calcul de l'arbre.Le problème de vivacité requiert de détecter les exécutions Zenon/non-Zenon. Une solution standard ajoute une horloge à l'automate. Nous montrons qu'elle conduit a une explosion combinatoire. Nous proposons une solution qui évite ce problème pour une grande classe d'abstractions. Pour les abstractions LU nous montrons que détecter ces exécutions est un problèmeNP-complet. / We consider the classic model of timed automata introduced by Alurand Dill. Two fundamental properties one would like to check in this modelare reachability and liveness. This thesis revisits these classical problems.The reachability problem for timed automata asks if there exists a run ofthe automaton from the initial state to a given final state. The standard solutionto this problem constructs a search tree whose nodes are abstractionsof zones. For effectiveness, abstractions are parameterized by maximal lowerand upper bounds (LU-bounds) occurring in the guards of the automaton.Such abstractions are also termed as LU-abstractions. The a4LU abstractiondefined by Behrmann et al is the coarsest known LU-abstraction. Althoughit is potentially most productive to use the a4LU abstraction, it has not beenused in implementations as it could lead to non-convex sets. We show howone could use the a4LU abstraction efficiently in implementations. Moreover,we prove that a4LU abstraction is optimal: given only the LU-bound information,it is the coarsest possible abstraction that is sound and completefor reachability. We then concentrate on ways to get better LU-bounds. Inthe standard procedure the LU-bounds are obtained from a static analysisof the automaton. We propose a new method to obtain better LU-boundson-the-fly during exploration of the zone graph. The potential gains of proposedimprovements are validated by experimental results on some standardverification case studies.The liveness problem deals with infinite executions of timed automata.An infinite execution is said to be Zeno if it spans only a finite amountof time. Such runs are considered unrealistic. While considering infiniteexecutions, one has to eliminate Zeno runs or dually, find runs that arenon-Zeno. The B¨uchi non-emptiness problem for timed automata asks ifthere exists a non-Zeno run visiting an accepting state infinitely often. Thestandard solution to this problem adds an extra clock to take care of non-Zenoness. We show that this solution might lead to an exponential blowupin the search space. We propose a method avoiding this blowup for a wideclass of abstractions weaker than LU-abstractions. We show that such amethod does not exist for LU-abstractions unless P=NP. Another questionrelated to infinite executions of timed automata is to decide the existenceof Zeno runs. We provide the first complete solution to this problem. Itworks for a wide class of abstractions weaker than LU. Yet again, we showthe solution could lead to a blowup for LU-abstractions, unless P=NP.

Cette thèse est centrée sur la modélisation de l'exécution d'une application parallèle par un graphe de flot de données. Ce graphe, qui relie les tâches aux données partagées, est construit de manière dynamique. Cette construction, indépendante de l'ordonnancement des tâches effectué, permet de définir la sémantique des accès aux données et de controler la consommation mémoire de toute exécution. Nous étudions dans une première partie les algorithmes permettant la construction et la gestion d'un tel graphe de flot de données dans un environnement distribué. Un point crucial de ces algorithmes est la détection de terminaison des accès des tâches sur les données partagées. Nous proposons un algorithme réactif réalisant cette détection. L'implantation de cet algorithme est au centre de l'implantation distribuée de l'interface de programmation parallèle Athapascan-1. Cette interface permet la description du parallélisme d'une application par création de tâches asynchrones. La sémantique (de type lexicographique) de cette interface est également définie à partir du graphe de flot de données. Nous montrons dans une deuxième partie que la connaissance du flot de données d'une application permet de controler de manière théorique la durée et, surtout, la consommation mémoire de toute exécution. Ce controle est effectué à partir d'un ordonnancement séquentiel implicite des tâches. Nous proposons, implantons dans Athapascan-1 et évaluons deux algorithmes d'ordonnancement distribués permettant de limiter le volume de mémoire requis par toute exécution. Ces expérimentations permettent de valider les résultats théoriques obtenus.

Le travail présenté dans ce mémoire s'inscrit dans le domaine des Environnements Informatiques pour l'Apprentissage Humain (EIAH), plus précisément celui de l'ingénierie des EIAH dans le cadre d'une approche de type " Learning Design ". Cette approche propose de construire des EIAH à partir de la description formelle d'une activité d'apprentissage. Elle suppose l'existence d'un langage de modélisation communément appelé EML (Educational Modelling Language) et d'un moteur capable d'interpréter ce langage. LDL est le langage sur lequel nous avons travaillé, en relation avec l'infrastructure LDI intégrant un moteur d'interprétation de LDL. L'EML est utilisé pour produire un scénario, modèle formel d'une activité d'apprentissage. L'EIAH servant de support au déroulement de l'activité décrite dans le scénario est alors construit de manière semi-automatique au sein de l'infrastructure associée au langage selon le processus suivant : le scénario est créé lors d'une phase de conception ; il est instancié et déployé sur une plate-forme de services lors d'une phase d'opérationnalisation (choix des participants à l'activité, affectation des rôles, choix des ressources et services) ; le scénario instancié et déployé est pris en charge par le moteur qui va l'interpréter pour en assurer l'exécution. Dans ce cadre, l'activité se déroule conformément à ce qui a été spécifié dans le scénario. Or il est impossible de prévoir par avance tout ce qui peut se produire dans une activité, les activités étant par nature imprévisibles. Des situations non prévues peuvent survenir et conduire à des perturbations dans l'activité, voire à des blocages. Il devient alors primordial de fournir les moyens de débloquer la situation. L'enseignant peut par ailleurs vouloir exploiter une situation ou une opportunité en modifiant l'activité en cours d'exécution. C'est le problème qui est traité dans cette thèse : il s'agit de fournir les moyens d'adapter une activité " à la volée ", c'est-à-dire pendant son exécution, de manière à pouvoir gérer une situation non prévue et poursuivre l'activité. La proposition que nous formulons s'appuie sur la différentiation entre les données convoquées dans chacune des trois phases du processus de construction de l'EIAH : la conception, l'opérationnalisation et l'exécution. Nous exhibons un modèle pour chacune de ces phases, qui organise ces données et les positionne les unes par rapport aux autres. Adapter une activité " à la volée " revient alors à modifier ces modèles en fonction des situations à traiter. Certaines nécessitent la modification d'un seul de ses modèles, d'autres conduisent à propager les modifications d'un modèle vers un autre. Nous considérons l'adaptation " à la volée " comme une activité à part entière menée, en parallèle de l'activité d'apprentissage, par un superviseur humain qui dispose d'un environnement adéquat pour observer l'activité, détecter les éventuels problèmes et y remédier par intervention dans l'activité d'apprentissage en modifiant les modèles qui la spécifient. Pour développer les outils support à la modification et les intégrer dans l'infrastructure LDI, nous avons eu recours à des techniques de l'Ingénierie Dirigée par les Modèles. Les modèles manipulés dans ces outils en sont ainsi des données à part entière : les outils réalisés n'en offrent ainsi que plus de flexibilité et d'abstraction. Les modèles sont alors exploités comme des leviers pour atteindre et modifier les données ciblées par l'adaptation.

Le perçage est un procédé de fabrication répandu dans le milieu industriel. Le secteur aéronautique a recours à ce procédé pour usiner de nombreuses pièces. Les chambres de combustions en sont un exemple. Exposées à des cycles thermiques sévères, elles sont percées d’une multitude de trous de refroidissement. Chez Safran Helicopter Engines, motoriste spécialisé dans la conception de turbines à gaz pour hélicoptères, ce perçage est réalisé à l’aide d’un procédé d’usinage unique : le perçage par percussion laser à la volée. Ce procédé phare leur permet de réaliser des milliers de trous inclinés dans des tôles en matériaux réfractaires. Safran Helicopter Engines cherche à maintenir son avance dans la production de turbines en s’appuyant sur les innovations constantes du procédé de perçage. Ce travail de thèse s’est articule autour du développement d’un nouveau procédé de perçage laser. De manière à définir un procédé fiable et efficace, plusieurs stratégies de perçage sont étudiées via les possibilités offertes par un laser à fibre milliseconde de haute puissance. Les résultats obtenus laissent entrevoir des perspectives intéressantes en termes d’augmentation de cadence de production à qualité d’usinage équivalente. L’amélioration des performances a été démontrée expérimentalement sur un banc d’essais représentatif des machines de production. Des trous de 400 μm de diamètre incliné à 60o ont pu être réalisés avec un cycle de perçage raccourci au minimum d’un facteur 2. Cette thèse présente également des éléments de compréhension des phénomènes de formation d’un trou. Pour cela, une modélisation des processus thermo hydrodynamiques impliqués dans le procédé de perçage laser a été développée. Ce modèle basé sur une approche par éléments finis repose sur l’étude thermique au cours de l’interaction entre le faisceau laser et la matière. Une partie du modèle inclut les phénomènes de propagation du faisceau dans la cavité en cours de formation afin de traduire de manière plus réaliste le dépôt d’énergie. / Drilling is a well-known manufacturing process. The aeronautic industry uses this process to machine a lot of elements. Among them, we can mention turbine blades, fuel injectors, combustion chambers. The latter are exposed to serious thermal stresses. To limit their impacts, combustion chambers are drilled with multiples cooling holes. At Safran Helicopter Engines, engines manufacturer specialized in engines design for helicopters, drilling is performed with a unique machining process : on the fly laser percussion drilling. This flagship process allows drilling thousands of tilted holes on refractory materials. Safran Helicopter Engines seeks to preserve its leading position in turbo engines manufacturing by looking for steady innovative drilling process. This thesis is structured around the development of a new laser drilling process. To define a reliable and efficient process, several drilling strategies were studied through the possibilities offered by a high-power millisecond fiber laser. The presented results allow catching a glimpse of the possibilities of production improvement. The performance enhancement was established through experimentation with a test bench. Holes of 400 μm diameter with an angle of 60o were drilled with a reduced processing time thanks to this new drilling process. In this thesis, we also propose a theoretical approach describing the hole formation. A mathematical model, accounting for all the physical process taking place during the drilling process is introduced. This model is based on finite elements method and considers the laser beam propagation within the drilled holes by solving Maxwell equations

Les langages de programmation typés dynamiquement tels que JavaScript et Python repoussent la vérification de typage jusqu’au moment de l’exécution. Afin d’optimiser la performance de ces langages, les implémentations de machines virtuelles pour langages dynamiques doivent tenter d’éliminer les tests de typage dynamiques redondants. Cela se fait habituellement en utilisant une analyse d’inférence de types. Cependant, les analyses de ce genre sont souvent coûteuses et impliquent des compromis entre le temps de compilation et la précision des résultats obtenus. Ceci a conduit à la conception d’architectures de VM de plus en plus complexes. Nous proposons le versionnement paresseux de blocs de base, une technique de compilation à la volée simple qui élimine efficacement les tests de typage dynamiques redondants sur les chemins d’exécution critiques. Cette nouvelle approche génère paresseusement des versions spécialisées des blocs de base tout en propageant de l’information de typage contextualisée. Notre technique ne nécessite pas l’utilisation d’analyses de programme coûteuses, n’est pas contrainte par les limitations de précision des analyses d’inférence de types traditionnelles et évite la complexité des techniques d’optimisation spéculatives. Trois extensions sont apportées au versionnement de blocs de base afin de lui donner des capacités d’optimisation interprocédurale. Une première extension lui donne la possibilité de joindre des informations de typage aux propriétés des objets et aux variables globales. Puis, la spécialisation de points d’entrée lui permet de passer de l’information de typage des fonctions appellantes aux fonctions appellées. Finalement, la spécialisation des continuations d’appels permet de transmettre le type des valeurs de retour des fonctions appellées aux appellants sans coût dynamique. Nous démontrons empiriquement que ces extensions permettent au versionnement de blocs de base d’éliminer plus de tests de typage dynamiques que toute analyse d’inférence de typage statique. / Dynamically typed programming languages such as JavaScript and Python defer type checking to run time. In order to maximize performance, dynamic language virtual machine implementations must attempt to eliminate redundant dynamic type checks. This is typically done using type inference analysis. However, type inference analyses are often costly and involve tradeoffs between compilation time and resulting precision. This has lead to the creation of increasingly complex multi-tiered VM architectures. We introduce lazy basic block versioning, a simple just-in-time compilation technique which effectively removes redundant type checks from critical code paths. This novel approach lazily generates type-specialized versions of basic blocks on the fly while propagating context-dependent type information. This does not require the use of costly program analyses, is not restricted by the precision limitations of traditional type analyses and avoids the implementation complexity of speculative optimization techniques. Three extensions are made to the basic block versioning technique in order to give it interprocedural optimization capabilities. Typed object shapes give it the ability to attach type information to object properties and global variables. Entry point specialization allows it to pass type information from callers to callees, and call continuation specialization makes it possible to pass return value type information back to callers without dynamic overhead. We empirically demonstrate that these extensions enable basic block versioning to exceed the capabilities of static whole-program type analyses.

Le travail présenté dans ce mémoire s'inscrit dans le domaine des Environnements Informatiques pour l'Apprentissage Humain (EIAH), plus précisément celui de l'ingénierie des EIAH dans le cadre d'une approche de type « Learning Design ». Cette approche propose de construire des EIAH à partir de la description formelle d'une activité d'apprentissage. Elle suppose l'existence d'un langage de modélisation communément appelé EML (Educational Modelling Language) et d'un moteur capable d'interpréter ce langage. LDL est le langage sur lequel nous avons travaillé, en relation avec l'infrastructure LDI intégrant un moteur d'interprétation de LDL. L'EML est utilisé pour produire un scénario, modèle formel d'une activité d'apprentissage. L'EIAH servant de support au déroulement de l'activité décrite dans le scénario est alors construit de manière semi-automatique au sein de l'infrastructure associée au langage selon le processus suivant : le scénario est créé lors d'une phase de conception ; il est instancié et déployé sur une plate-forme de services lors d'une phase d'opérationnalisation (choix des participants à l'activité, affectation des rôles, choix des ressources et services) ; le scénario instancié et déployé est pris en charge par le moteur qui va l'interpréter pour en assurer l'exécution. Dans ce cadre, l'activité se déroule conformément à ce qui a été spécifié dans le scénario. Or il est impossible de prévoir par avance tout ce qui peut se produire dans une activité, les activités étant par nature imprévisibles. Des situations non prévues peuvent survenir et conduire à des perturbations dans l'activité, voire à des blocages. Il devient alors primordial de fournir les moyens de débloquer la situation. L'enseignant peut par ailleurs vouloir exploiter une situation ou une opportunité en modifiant l'activité en cours d'exécution. C'est le problème qui est traité dans cette thèse : il s'agit de fournir les moyens d'adapter une activité « à la volée », c'est-à-dire pendant son exécution, de manière à pouvoir gérer une situation non prévue et poursuivre l'activité. La proposition que nous formulons s'appuie sur la différentiation entre les données convoquées dans chacune des trois phases du processus de construction de l'EIAH : la conception, l'opérationnalisation et l'exécution. Nous exhibons un modèle pour chacune de ces phases, qui organise ces données et les positionne les unes par rapport aux autres. Adapter une activité « à la volée » revient alors à modifier ces modèles en fonction des situations à traiter. Certaines nécessitent la modification d'un seul de ses modèles, d'autres conduisent à propager les modifications d'un modèle vers un autre. Nous considérons l'adaptation « à la volée » comme une activité à part entière menée, en parallèle de l'activité d'apprentissage, par un superviseur humain qui dispose d'un environnement adéquat pour observer l'activité, détecter les éventuels problèmes et y remédier par intervention dans l'activité d'apprentissage en modifiant les modèles qui la spécifient. Pour développer les outils support à la modification et les intégrer dans l'infrastructure LDI, nous avons eu recours à des techniques de l'Ingénierie Dirigée par les Modèles. Les modèles manipulés dans ces outils en sont ainsi des données à part entière : les outils réalisés n'en offrent ainsi que plus de flexibilité et d'abstraction. Les modèles sont alors exploités comme des leviers pour atteindre et modifier les données ciblées par l'adaptation. / The work presented in this paper is in the field of Technology for Human Learning (TEL), specifically that of engineering in the context of TEL-type approach "Learning Design". This approach proposes to build ILE from the formal description of a learning activity. It assumes the existence of a common modeling language called EML (Educational Modelling Language) and an engine capable of interpreting this language. LDL is the language on which we worked in conjunction with the LDI infrastructure including a motor interpretation of LDL. The EML is used to produce a scenario, a formal model of learning activity. The ILE serving to support the conduct of the activity described in the scenario is then constructed semi-automatically in the infrastructure associated with the language using the following process: the script is created during a design phase; it is instantiated and deployed on a platform of services in an operational phase (selection of participants in the activity, role assignment, choice of resources and services); instantiated and deployed scenario is supported by the engine will interpret it to ensure its implementation. In this context, the activity takes place in accordance with what was specified in the script. It is impossible to predict in advance all that can occur in an activity, the activities are by nature unpredictable. Unforeseen situations can occur and lead to disturbances in the activity, or even blocks. It then becomes important to provide the means to break the deadlock. The teacher may also want to exploit a situation or opportunity by altering the activity in progress. This is the problem that is addressed in this thesis: to provide the means to adapt an activity "on the fly", that is to say while running, so you can not handle a situation provided and continue the activity. The proposal we make is based on the differentiation between data convened in each of the three phases of construction of the ILE: design, operationalization and implementation. We exhibit a model for each phase, which organizes the data and positions to each other. Adapt an activity "on the fly" then returns to modify these models in different situations to deal with. Some require the modification of one of its models, while others lead to propagate changes from one model to another. We consider adaptation "on the fly" as a separate activity conducted in parallel with the learning activity by a human supervisor has an adequate environment to observe the activity, identify potential problems and be remedied by intervention in the learning activity by modifying the templates that specify. To develop tools to support the change and integrate them into the LDI infrastructure, we have used the techniques of Model Driven Engineering. Handled in these models are tools and data in its own right tools and made no offer more flexibility and abstraction. The models are then used as levers to achieve and change the data targeted by the adaptation.

Nous présentons dans ces travaux une contribution concernant la distribution de simulations de système complexe dans des environnements distribués ouverts. Nous considérons ces environnements comme des écosystèmes computationnels, dont nous décrivons les propriétés et les caractéristiques, dans lesquels évoluent, de par leur exécution, les simulations. Elles sont modélisées sous la forme d'un réseau d'interactions représenté à l'aide d'un graphe dynamique. En considérant les différentes dynamiques possibles, nous proposons un formalisme général représentant ces graphes, ainsi qu'une interface de programmation, GraphStream, permettant de les manipuler et de les étudier.Le graphe dynamique est alors un sujet d'étude dans lequel nous recherchons des organisations, que nous suivons dans le temps, afin de minimiser les coûts de communication entre les machines et d'équilibrer la charge de calcul. Nous apportons une amélioration visant à réduire les oscillations des résultats de l'algorithme AntCo2 utilisant des colonies de fourmis numériques qui, grâce à des mécanismes de compétition et de collaboration, détecte des organisations. La stabilité de ces dernières est déterminée par l'intermédiaire d'une heuristique de recherche distribuée et dynamique de centroïdes.Un intergiciel est proposé permettant de distribuer de manière décentralisée et dynamique les simulations dans un écosystème computationnel en favorisant les organisations et en respectant l'équilibrage de charge.

Le marché de l'électronique grand public est dominé par les systèmes embarqués du fait de leur puissance de calcul toujours croissante et des nombreuses fonctionnalités qu'ils proposent.Pour procurer de telles caractéristiques, les architectures des systèmes embarqués sont devenues de plus en plus complexes (pluralité et hétérogénéité des unités de traitements, exécution concurrente des tâches, ...).Cette complexité a fortement influencé leur programmabilité au point où rendre difficile la compréhension de l'exécution d'une application sur ces architectures.L'approche la plus utilisée actuellement pour l'analyse de l'exécution des applications sur les systèmes embarqués est la capture des traces d'exécution (séquences d'événements, tels que les appels systèmes ou les changements de contexte, générés pendant l'exécution des applications).Cette approche est utilisée lors des activités de test, débogage ou de profilage des applications.Toutefois, suivant certains cas d'utilisation, les traces d'exécution générées peuvent devenir très volumineuses, de l'ordre de plusieurs centaines de gigaoctets.C'est le cas des tests d'endurance ou encore des tests de validation, qui consistent à tracer l'exécution d'une application sur un système embarqué pendant de longues périodes, allant de plusieurs heures à plusieurs jours.Les outils et méthodes d'analyse de traces d'exécution actuels ne sont pas conçus pour traiter de telles quantités de données.Nous proposons une approche de réduction du volume de trace enregistrée à travers une analyse à la volée de la trace durant sa capture.Notre approche repose sur les spécificités des applications multimédia, qui sont parmi les plus importantes pour le succès des dispositifs populaires comme les Set-top boxes ou les smartphones.Notre approche a pour but de détecter automatiquement les fragments (périodes) suspectes de l'exécution d'une application afin de n'enregistrer que les parties de la trace correspondant à ces périodes d'activités.L'approche que nous proposons comporte deux étapes : une étape d'apprentissage qui consiste à découvrir les comportements réguliers de l'application à partir de la trace d'exécution, et une étape de détection d'anomalies qui consiste à identifier les comportements déviant des comportements réguliers.Les nombreuses expériences, réalisées sur des données synthétiques et des données réelles, montrent que notre approche permet d'obtenir une réduction du volume de trace enregistrée d'un ordre de grandeur avec d'excellentes performances de détection des comportements suspects. / The consumer electronics market is dominated by embedded systems due to their ever-increasing processing power and the large number of functionnalities they offer.To provide such features, architectures of embedded systems have increased in complexity: they rely on several heterogeneous processing units, and allow concurrent tasks execution.This complexity degrades the programmability of embedded system architectures and makes application execution difficult to understand on such systems.The most used approach for analyzing application execution on embedded systems consists in capturing execution traces (event sequences, such as system call invocations or context switch, generated during application execution).This approach is used in application testing, debugging or profiling.However in some use cases, execution traces generated can be very large, up to several hundreds of gigabytes.For example endurance tests, which are tests consisting in tracing execution of an application on an embedded system during long periods, from several hours to several days.Current tools and methods for analyzing execution traces are not designed to handle such amounts of data.We propose an approach for monitoring an application execution by analyzing traces on the fly in order to reduce the volume of recorded trace.Our approach is based on features of multimedia applications which contribute the most to the success of popular devices such as set-top boxes or smartphones.This approach consists in identifying automatically the suspicious periods of an application execution in order to record only the parts of traces which correspond to these periods.The proposed approach consists of two steps: a learning step which discovers regular behaviors of an application from its execution trace, and an anomaly detection step which identifies behaviors deviating from the regular ones.The many experiments, performed on synthetic and real-life datasets, show that our approach reduces the trace size by an order of magnitude while maintaining a good performance in detecting suspicious behaviors.

Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.