Exploration de l'espace de design assistée par ordinateur pour les systèmes multi-coeurs

The growing complexity of embedded systems calls for modeling formalisms that can be simulated and analyzed to explore the space of design alternatives. This thesis describes the development of a modeling formalism and tools for design space exploration at early design stage.We extend the classical worst-case model checking for timed automata to stochastic analysis based on a refinement of temporal uncertainty intervals into delay distribution. On one hand we introduce the formalism of Duration Probabilistic Automata (DPA) supporting analysis as well as optimization. On the other hand we provide DESPEX (DEsign SPace EXplorer), a tool for performance evaluation of high-level models of applications running on multi-core platforms. We also show its usage on several case studies.La complexité croissante des systèmes embarqués nécessite des formalismes de modélisation qui peuvent être simulés et analysés pour explorer l'espace des alternatives de conception. Cette thèse décrit le développement d'un formalisme de modélisation et des outils pour l'exploration de l'espace de design au plus tôt dans le flot de conception. Nous étendons le model-checking classique au pire cas pour les automates temporisés à l'analyse stochastique basée sur un raffinement des intervalles d'incertitude temporelle par des distributions sur les délais. D'une part, nous introduisons le formalisme des Duration Probabilistic Automata (DPA) à partir duquel nous pouvons réaliser de l'analyse ainsi que de l'optimisation. D'autre part nous présentons DESPEX (Design Space Explorer), un outil d'évaluation de performance de modèles de haut niveau des applications qui s'exécutent sur les plates-formes multi-coeurs. Nous montrons également son utilisation sur plusieurs cas d'étude