Le concept de pair à pair (P2P) a connu récemment de grands développements dans les domaines du partage de fichiers, du streaming vidéo et des bases de données distribuées. Le développement du concept de parallélisme dans les architectures de microprocesseurs et les avancées en matière de réseaux à haut débit permettent d'envisager de nouvelles applications telles que le calcul intensif distribué. Cependant, la mise en oeuvre de ce nouveau type d'application sur des réseaux P2P pose de nombreux défis comme l'hétérogénéité des machines, le passage à l'échelle et la robustesse. Par ailleurs, les protocoles de transport existants comme TCP et UDP ne sont pas bien adaptés à ce nouveau type d'application. Ce mémoire de thèse a pour objectif de présenter un environnement décentralisé pour la mise en oeuvre de calculs intensifs sur des réseaux pair à pair. Nous nous intéressons à des applications dans les domaines de la simulation numérique et de l'optimisation qui font appel à des modèles de type parallélisme de tâches et qui sont résolues au moyen d'algorithmes itératifs distribués or parallèles. Contrairement aux solutions existantes, notre environnement permet des communications directes et fréquentes entre les pairs. L'environnement est conçu à partir d'un protocole de communication auto-adaptatif qui peut se reconfigurer en adoptant le mode de communication le plus approprié entre les pairs en fonction de choix algorithmiques relevant de la couche application ou d'éléments de contexte comme la topologie au niveau de la couche réseau. Nous présentons et analysons des résultats expérimentaux obtenus sur diverses plateformes comme GRID'5000 et PlanetLab pour le problème de l'obstacle et des problèmes non linéaires de flots dans les réseaux.

Les systèmes temps-réel critiques sont de plus en plus complexes, et les exigences fonctionnelles et non-fonctionnelles ne cessent plus de croître. Le flot de conception de tels systèmes doit assurer, parmi d'autres propriétés, le déterminisme fonctionnel et la prévisibilité temporelle. Le déterminisme fonctionnel est inhérent aux modèles de calcul flot de données (ex. KPN, SDF, etc.) ; c'est pour cela qu'ils sont largement utilisés pour modéliser les systèmes embarqués de traitement de flux. Un effort considérable a été accompli pour résoudre le problème d'ordonnancement statique périodique et à mémoire de communication bornée des graphes flots de données. Cependant, les systèmes embarqués temps-réel optent de plus en plus pour l'utilisation de systèmes d'exploitation temps-réel et de stratégies d'ordonnancement dynamique pour gérer les tâches et les ressources critiques. Cette thèse aborde le problème d'ordonnancement temps-réel dynamique des graphes flots de données ; ce problème consiste à assigner chaque acteur dans un graphe à une tâche temps-réel périodique (i.e. calcul des périodes, des phases, etc.) de façon à : (1) assurer l'ordonnançabilité des tâches sur une architecture et pour une stratégie d'ordonnancement (ex. RM, EDF) données ; (2) exclure statiquement les exceptions d'overflow et d'underflow sur les buffers de communication ; et (3) optimiser les performances du système (ex. maximisation du débit, minimisation des tailles des buffers).

Les nouveaux systèmes ont souvent recours à une implémentation distribuée du logiciel, pour des raisons d'efficacité et à cause de l'emplacement physique de certains capteurs et actuateurs. S'assurer de la correction d'un logiciel distribué est difficile car cela impose de considérer tous les enchevêtrements possibles des actions exécutées par des processus distincts. Cette thèse propose une méthode pour générer, à partir d'un modèle d'application haut niveau, une implémentation distribuée correcte et efficace. Le modèle de l'application comporte des composants communiquant au moyen d'interactions multiparties avec priorités. L'exécution d'une interaction multipartie, qui correspond à un pas de la sémantique, change de façon atomique l'état de tous les composants participant à l'interaction. On définit une implantation distribuée comme un ensemble de processus communiquant par envoi de message asynchrone. La principale difficulté est de produire une implémentation correcte et efficace des interactions multiparties avec priorités, en utilisant uniquement l'envoi de message comme primitive. La méthode se fonde sur un flot de conception rigoureux qui raffine progressivement le modèle haut niveau en un modèle bas niveau, à partir duquel le code pour une plateforme particulière est généré. Tous les modèles intermédiaires apparaissant dans le flot sont exprimés avec la même sémantique que le modèle original. À chaque étape du flot, les interactions complexes sont remplacés par des constructions utilisant des interactions plus simples. En particulier, le dernier modèle obtenu avant la génération du code ne contient que des interactions modélisant l'envoi de message. La correction de l'implémentation est obtenue par construction. L'utilisation des interactions multiparties comme primitives dans le modèle de l'application permet de réduire très significativement l'ensemble des états atteignables, par rapport à un modèle équivalent mais utilisant des primitives de communication plus simples. Les propriétés essentielles du système sont vérifiées à ce niveau d'abstraction. Chaque transformation constituante du flot de conception est suffisamment simple pour être complètement formalisée et prouvée, en termes d'équivalence observationelle ou d'équivalence de trace entre le modèles avant et après transformation. L'implémentation ainsi obtenue est correcte par rapport au modèle original, ce qui évite une coûteuse vérification a posteriori. Concernant l'efficacité, la performance de l'implémentation peut être optimisée en choisissant les paramètres adéquats pour les transformations, ou en augmentant la connaissance des composants. Cette dernière solution requiert une analyse du modèle de départ afin de calculer la connaissance qui est réutilisée pour les étapes ultérieures du flot de conception. Les différentes transformations et optimisations constituant le flot de conception ont été implémentées dans le cadre de BIP. Cette implémentation a permis d'évaluer les différentes possibilités ainsi que l'influence des différents paramètres, sur la performance de l'implémentation obtenue avec plusieurs exemples. Le code généré utilise les primitives fournies par les sockets POSIX, MPI ou les pthreads pour envoyer des messages entre les processus.

Dans cette Thèse, la conception robuste avec un modèle incertain d'un système électromécanique avec vibro-impact est fait. Le système électromécanique est constitué d'un chariot, dont le mouvement est excité par un moteur à courant continu et un marteau embarqué dans ce chariot. Le marteau est relié au chariot par un ressort non linéaire et par un amortisseur linéaire, de façon qu'un mouvement relatif existe entre eux. Une barrière flexible linéaire, placé à l'extérieur du chariot limite les mouvements de marteau. En raison du mouvement relatif entre le marteau et la barrière, impacts peuvent se produire entre ces deux éléments. Le modèle du système développé prend en compte l'influence du courant continu moteur dans le comportement dynamique du système. Certains paramètres du système sont incertains, tels comme les coefficients de rigidité et d'amortissement de la barrière flexible. L'objectif de la Thèse est de réaliser une optimisation de ce système électromécanique par rapport aux paramètres de conception afin de maximiser l'impact puissance sous la contrainte que la puissance électrique consommée par le moteur à courant continu est inférieure à une valeur maximale. Pour choisir les paramètres de conception dans le problème d'optimisation, une analyse de sensibilité a été réalisée afin de définir les paramètres du système les plus sensibles. L'optimisation est formulée dans le cadre de la conception robuste en raison de la présence d'incertitudes dans le modèle. Les lois de probabilités liées aux variables aléatoires du problème sont construites en utilisant le Principe du Maximum l'Entropie et les statistiques de la réponse stochastique du système sont calculées en utilisant la méthode de Monte Carlo. L'ensemble d'équations non linéaires sont présentés, et un solveur temporel adapté est développé. Le problème d'optimisation non linéaire stochastique est résolu pour différents niveaux d'incertitudes, et aussi pour le cas déterministe. Les résultats sont différents, ce qui montre l'importance de la modélisation stochastique / In this Thesis, the robust design with an uncertain model of a vibro-impact electromechanical system is done. The electromechanical system is composed of a cart, whose motion is excited by a DC motor (motor with continuous current), and an embarked hammer into this cart. The hammer is connected to the cart by a nonlinear spring component and by a linear damper, so that a relative motion exists between them. A linear flexible barrier, placed outside of the cart, constrains the hammer movements. Due to the relative movement between the hammer and the barrier, impacts can occur between these two elements. The developed model of the system takes into account the influence of the DC motor in the dynamic behavior of the system. Some system parameters are uncertain, such as the stiffness and the damping coefficients of the flexible barrier. The objective of the Thesis is to perform an optimization of this electromechanical system with respect to design parameters in order to maximize the impact power under the constraint that the electric power consumed by the DC motor is lower than a maximum value. To chose the design parameters in the optimization problem, an sensitivity analysis was performed in order to define the most sensitive system parameters. The optimization is formulated in the framework of robust design due to the presence of uncertainties in the model. The probability distributions of random variables are constructed using the Maximum Entropy Principle and statistics of the stochastic response of the system are computed using the Monte Carlo method. The set of nonlinear equations are presented, and an adapted time domain solver is developed. The stochastic nonlinear constrained design optimization problem is solved for different levels of uncertainties, and also for the deterministic case. The results are different and this show the importance of the stochastic modeling

Les applications de gestion de flux sont responsables de la majorité des calculs des systèmes embarqués (vidéo conférence, vision par ordinateur). Leurs exigences de haute performance rendent leur mise en œuvre parallèle nécessaire. Par conséquent, il est de plus en plus courant que les systèmes embarqués modernes incluent des processeurs multi-cœurs qui permettent un parallélisme massif. La mise en œuvre des applications de gestion de flux sur des multi-cœurs est difficile à cause de leur complexité, qui tend à augmenter, et de leurs exigences strictes à la fois qualitatives (robustesse, fiabilité) et quantitatives (débit, consommation d'énergie). Ceci est observé dans l'évolution de codecs vidéo qui ne cessent d'augmenter en complexité, tandis que leurs exigences de performance demeurent les mêmes. Les modèles de calcul (MdC) flot de données ont été développés pour faciliter la conception de ces applications qui sont typiquement composées de filtres qui échangent des flux de données via des liens de communication. Ces modèles fournissent une représentation intuitive des applications de gestion de flux, tout en exposant le parallélisme de tâches de l'application. En outre, ils fournissent des analyses statiques pour la vivacité et l'exécution en mémoire bornée. Cependant, les applications de gestion de flux modernes comportent des filtres qui échangent des quantités de données variables, et des liens de communication qui peuvent être activés / désactivés. Dans cette thèse, nous présentons un nouveau MdC flot de données, le Boolean Parametric Data Flow (BPDF), qui permet le paramétrage de la quantité de données échangées entre les filtres en utilisant des paramètres entiers et l'activation et la désactivation de liens de communication en utilisant des paramètres booléens. De cette manière, BPDF est capable de exprimer des applications plus complexes, comme les décodeurs vidéo modernes. Malgré l'augmentation de l'expressivité, les applications BPDF restent statiquement analysables pour la vivacité et l'exécution en mémoire bornée. Cependant, l'expressivité accrue complique grandement la mise en œuvre. Les paramètres entiers entraînent des dépendances de données de type paramétrique et les paramètres booléens peuvent désactiver des liens de communication et ainsi éliminer des dépendances de données. Pour cette raison, nous proposons un cadre d'ordonnancement qui produit des ordonnancements de type ``aussi tôt que possible'' (ASAP) pour un placement statique donné. Il utilise des contraintes d'ordonnancement, soit issues de l'application (dépendance de données) ou de l'utilisateur (optimisations d'ordonnancement). Les contraintes sont analysées pour la vivacité et, si possible, simplifiées. De cette façon, notre cadre permet une grande variété de politiques d'ordonnancement, tout en garantissant la vivacité de l'application. Enfin, le calcul du débit d'une application est important tant avant que pendant l'exécution. Il permet de vérifier que l'application satisfait ses exigences de performance et il permet de prendre des décisions d'ordonnancement à l'exécution qui peuvent améliorer la performance ou la consommation d'énergie. Nous traitons ce problème en trouvant des expressions paramétriques pour le débit maximum d'un sous-ensemble de BPDF. Enfin, nous proposons un algorithme qui calcule une taille des buffers suffisante pour que l'application BPDF ait un débit maximum. / Streaming applications are responsible for the majority of the computation load in many embedded systems (video conferencing, computer vision etc). Their high performance requirements make parallel implementations a necessity. Hence, more and more modern embedded systems include many-core processors that allow massive parallelism. Parallel implementation of streaming applications on many-core platforms is challenging because of their complexity, which tends to increase, and their strict requirements both qualitative (e.g., robustness, reliability) and quantitative (e.g., throughput, power consumption). This is observed in the evolution of video codecs that keep increasing in complexity, while their performance requirements remain the same or even increase. Data flow models of computation (MoCs) have been developed to facilitate the design process of such applications, which are typically composed of filters exchanging streams of data via communication links. Data flow MoCs provide an intuitive representation of streaming applications, while exposing the available parallelism of the application. Moreover, they provide static analyses for liveness and boundedness. However, modern streaming applications feature filters that exchange variable amounts of data, and communication links that are not always active. In this thesis, we present a new data flow MoC, the Boolean Parametric Data Flow (BPDF), that allows parametrization of the amount of data exchanged between the filters using integer parameters and the enabling and disabling of communication links using boolean parameters. In this way, BPDF is able to capture more complex streaming applications, like video decoders. Despite the increase in expressiveness, BPDF applications remain statically analyzable for liveness and boundedness. However, increased expressiveness greatly complicates implementation. Integer parameters result in parametric data dependencies and the boolean parameters disable communication links, effectively removing data dependencies. We propose a scheduling framework that facilitates the scheduling of BPDF applications. Our scheduling framework produces as soon as possible schedules for a given static mapping. It takes us input scheduling constraints that derive either from the application (data dependencies) or from the user (schedule optimizations). The constraints are analyzed for liveness and, if possible, simplified. In this way, our framework provides flexibility, while guaranteeing the liveness of the application. Finally, calculation of the throughput of an application is important both at compile-time and at run-time. It allows to verify at compile-time that the application meets its performance requirements and it allows to take scheduling decisions at run-time that can improve performance or power consumption. We approach this problem by finding parametric throughput expressions for the maximum throughput of a subset of BPDF graphs. Finally, we provide an algorithm that calculates sufficient buffer sizes for the BPDF graph to operate at maximum throughput.

Les systèmes embarqués ont évolué d'une manière spectaculaire et sont devenus partie intégrante de notre quotidien. En réponse aux exigences grandissantes en termes de nombre de fonctionnalités et donc de flexibilité, les parties logicielles de ces systèmes se sont vues attribuer une place importante malgré leur manque d'efficacité, en comparaison aux solutions matérielles. Par ailleurs, vu la prolifération des systèmes nomades et à ressources limités, tenir compte de la performance est devenu indispensable pour bien les concevoir. Dans cette thèse, nous proposons une démarche rigoureuse et intégrée pour la modélisation et l'évaluation de performance tôt dans le processus de conception. Cette méthode permet de construire des modèles, au niveau système, conformes aux spécifications fonctionnelles, et intégrant les contraintes non-fonctionnelles de l'environnement d'exécution. D'autre part, elle permet d'analyser quantitativement la performance de façon rapide et précise. Cette méthode est guidée par les modèles et se base sur le formalisme $mathcal{S}$BIP que nous proposons pour la modélisation stochastique selon une approche formelle et par composants. Pour construire des modèles conformes au niveau système, nous partons de modèles purement fonctionnels utilisés pour générer automatiquement une implémentation distribuée, étant donnée une architecture matérielle cible et un schéma de répartition. Dans le but d'obtenir une description fidèle de la performance, nous avons conçu une technique d'inférence statistique qui produit une caractérisation probabiliste. Cette dernière est utilisée pour calibrer le modèle fonctionnel de départ. Afin d'évaluer la performance de ce modèle, nous nous basons sur du model checking statistique que nous améliorons à l'aide d'une technique d'abstraction. Nous avons développé un flot de conception qui automatise la majorité des phases décrites ci-dessus. Ce flot a été appliqué à différentes études de cas, notamment à une application de reconnaissance d'image déployée sur la plateforme multi-cœurs STHORM. / In the present work, we tackle the problem of modeling and evaluating performance in the context of embedded systems design. These have become essential for modern societies and experienced important evolution. Due to the growing demand on functionality and programmability, software solutions have gained in importance, although known to be less efficient than dedicated hardware. Consequently, considering performance has become a must, especially with the generalization of resource-constrained devices. We present a rigorous and integrated approach for system-level performance modeling and analysis. The proposed method enables faithful high-level modeling, encompassing both functional and performance aspects, and allows for rapid and accurate quantitative performance evaluation. The approach is model-based and relies on the $mathcal{S}$BIP formalism for stochastic component-based modeling and formal verification. We use statistical model checking for analyzing performance requirements and introduce a stochastic abstraction technique to enhance its scalability. Faithful high-level models are built by calibrating functional models with low-level performance information using automatic code generation and statistical inference. We provide a tool-flow that automates most of the steps of the proposed approach and illustrate its use on a real-life case study for image processing. We consider the design and mapping of a parallel version of the HMAX models algorithm for object recognition on the STHORM many-cores platform. We explored timing aspects and the obtained results show not only the usability of the approach but also its pertinence for taking well-founded decisions in the context of system-level design.

Au cours des dernières années, l'utilisation d’appareils embarqués a augmenté rapidement en raison de la commodité qu'ils offrent dans la vie quotidienne. Les appareils embarqués se caractérisent par leur petite taille, leur portabilité ainsi que leur capacité d'échanger des données avec d'autres appareils grâce à leur service de communication réseau. L'analyse du comportement et les interactions entre ces appareils a abouti dans l'établissement d’un nouveau type de système, appelé systèmes embarqués en réseau.En tant que la popularité actuelle des systèmes embarqués en réseau grandissent, il y a une tendance de relever leurs défis de conception existants afin de développer d'applications fonctionnelles. Ces défis concernent l'utilisation de leurs ressources matérielles limitées (p.ex. la mémoire du processeur, l'unité d'alimentation) et l'hétérogénéité du système en termes de logiciel, de matériel et aussi des mécanismes d'interaction entre les appareils. A cet effet, dans cette thèse nous présentons une approche rigoureuse considérant tous les défis grâce à un flot de conception basée sur techniques de modélisation. Le flot utilise le formalisme BIP pour la construction hiérarchique de systèmes autour de composants et il est facilement utilisé, car chaque étape est entièrement automatisée par des outils et méthodes développés. En plus, ce flot perme la simulation des systèmes à chaque étape de développement, la vérification par l'exploration de l'espace de conception, la génération de code et la calibration des modèles développés, afin de présenter fidèlement le système réel. Les modèles calibrés peuvent analyser la performance de system et aussi valider des exigences sur le system. Finalement, les résultats d'analyse de performance peuvent apporter des améliorations sur la conception de système cible.Notre approche est présenté sur plusieurs bien connus domaines applicatifs des systèmes embarqués en réseau, comme les systèmes automobiles, les systèmes de l'automation industrielle, les systèmes de réseaux de capteurs sans fil (WSN systèmes) et les systèmes pour l'internet des objets (IoT systèmes). Chaque domaine inclut différentes caractéristiques et technologies, mais dispose également différent défis. Ces défis sont considérés par les outils développés pour chaque domaine, qui sont validées contre les outils existantes, comme MATLAB/Simulink, RTaW-Sim, OPNET Modeler et Cooja. La validation se fait grâce à les cas d’études sur les applications industrielles ou les benchmark réalistes des systèmes embarqués en réseau. Nos expérimentations illustrent le soutien d'une meilleure analyse par les outils développés en fournissant d'abord résultats similaires pendant la simulation et en plus les capacités de génération automatique de code et la vérification des exigences. / Over the latest years the use of embedded devices has expanded rapidly due to the convenience they offer in daily life. Embedded devices are characterized by their tiny size, their portability as well as their ability to exchange data with other devices through a dedicated network unit. The analysis of the behavior and interactions between such devices lead to the emergence of a new system type, called networked embedded systems.As the current popularity of networked embedded systems grows, there is a trend for addressing their existing design challenges in the development of functional applications. These challenges relate to the use of their limited hardware resources (e.g. processor memory, power unit) and the system heterogeneity in terms of software, hardware as well as communication mechanisms between the embedded devices. To this end, in this thesis we present a rigorous approach considering all the design challenges through a model-based design flow. The flow uses BIP as an underlying framework for the hierarchical construction of component-based systems and it is easily employed, as each step is fully supported by developed tools and methods. Its benefits include early-stage simulation and testing, verification of functional correctness, generation of deployable code and collection of performance data from real executions, in order to calibrate the developed models. Calibrated models represent faithfully the real system and can analyze system performance as well as evaluate accurately system requirements. Additionally, performance analysis results may provide design enhancements in the target system.Our approach is demonstrated in several well-known application domains of networked embedded systems, namely the automotive, industrial automation, Wireless Sensor Network (WSN) and Internet of Things (IoT) systems. Each domain includes different characteristics and technologies, but also features different challenges. These challenges are considered by developed tools for each domain, which are validated against existing domain-specific, such as MATLAB/Simulink, RTaW-Sim, OPNET Modeler and Cooja. The validation is facilitated through case-studies in industrial or benchmark networked embedded systems. Our experiments illustrate the support of a better fine-grained analysis from the developed tools by initially providing similar simulation results and additionally offering capabilities for automated code generation as well as requirement verification.

Les fonctions de commande et de contrôle sont parmi les plus importantes des systèmes embarqués critiques utilisés dans des activités telles les transports, la santé ou la gestion de l’énergie. Leur impact potentiel sur la sûreté de fonctionnement fait de la vérification de leur correction l’un des points les plus critiques de leur développement. Cette vérification est usuellement effectuée en accord avec les normes de certification décrivant un ensemble d’objectifs à atteindre afin d’assurer un haut niveau de qualité du système et donc de prévenir l’apparition de défauts. Cette vérification du logiciel est traditionnellement basée sur de nombreux tests et des activitiés de relectures de code, toutefois les versions les plus récentes des standards de certification permettent l’utilisation de nouvelles approches de développement telles que l’ingénierie dirigée par les modèles et les méthodes formelles ainsi que l’utilisation d’outil pour assister les processus de développement. Les outils de génération automatique de code sont exploités dans la plupart des processus de développement de systèmes embarqués critiques afin d’éviter des erreurs de programmation liées à l’humain et pour assurer le respect des règles de production de code. Ces outils ayant pour vocation de remplacer les humains pour la production de code, des erreurs dans leur conception peuvent causer l’apparition d’erreurs dans le code généré. Il est donc nécessaire de vérifier que le niveau de qualité de l’outil est le même que celui du code produit en s’assurant que les objectifs spécifiées dans les normes de qualification sont couverts. Nos travaux visent à exploiter l’ingénierie dirigée par les modèles et les méthodes formelles pour développer ces outils et ainsi atteindre un niveau de qualité plus élevé que les approches traditionnelles. Les fonctions critiques de commande et de contrôle sont en grande partie conçues à l’aide de langages graphiques à flot de données. Ces langages sont utilisés pour modéliser des systèmes complexes à l’aide de blocs élémentaires groupés dans des librairies de blocs. Un bloc peut être un objet logiciel sophistiqué exposant une haute variabilité tant structurelle que sémantique. Cette variabilité est à la fois liée aux valeurs des paramètres du bloc ainsi qu’à son contexte d’utilisation. Dans notre travail, nous concentrons notre attention en premier lieu sur la spécification formelle de ces blocs ainsi que sur la vérification de ces spécifications. Nous avons évalué plusieurs approches et techniques dans le but d’assurer une spécification formelle, structurellement cohérente, vérifiable et réutilisable des blocs. Nous avons finalement conçu un langage basé sur l’ingénierie dirigées par les modèles dédié à cette tâche. Ce langage s’inspire des approches des lignes de produit logiciel afin d’assurer une gestion de la variabilité des blocs à la fois correcte et assurant un passage à l’échelle. Nous avons appliqué cette approche et la vérification associée sur quelques exemples choisis de blocs issus d’applications industrielles et l’avons validé sur des prototypes logiciels que nous avons développé. Les blocs sont les principaux éléments des langages d’entrée utilisés pour la génération automatique de logiciels de commande et de contrôle. Nous montrons comment les spécifications formelles de blocs peuvent être transformées en des annotations de code afin de simplifier et d’automatiser la vérification du code généré. Les annotations de code sont vérifiées par la suite à l’aide d’outils spécialisés d’analyse statique de code. En utilisant des observateur synchrones pour exprimer des exigences de haut niveau sur les modèles en entrée du générateur, nous montrons comment la spécification formelle de blocs peut être utilisée pour la génération d’annotations de code et par la suite pour la vérification automatique des exigences. / Control and command softwares play a key role in safety-critical embedded systems used for human related activities such as transportation, healthcare or energy. Their impact on safety makes the assessment of their correctness the central point in their development activities. Such systems verification activities are usually conducted according to normative certification guidelines providing objectives to be reached in order to ensure development process reliability and thus prevent flaws. Verification activities usually relies on tests and proof reading of the software but recent versions of certification guidelines are taking into account the deployment of new development paradigms such as model-based development, and formal methods; or the use of tools in assistance of the development processes. Automatic code generators are used in most safety-critical embedded systems development in order to avoid human related software production errors and to ensure the respect of development quality standards. As these tools are supposed to replace humans in the software code production activities, errors in these tools may result in embedded software flaws. It is thus in turn mandatory to ensure the same level of correctness for the tool itself than for the expected produced code. Tools verification shall be done according to qualification guidelines. We advocate in our work the use of model-based development and formal methods for the development of these tools in order to reach a higher quality level. Critical control and command software are mostly designed using graphical dataflow languages. These languages are used to express complex systems relying on atomic operations embedded in blocks that are gathered in block libraries. Blocks may be sophisticated pieces of software with highly variable structure and semantics. This variability is dependent on the values of the block parameters and of the block's context of use. In our work, we focus on the formal specification and verification of such block based languages. We experimented various techniques in order to ensure a formal, sound, verifiable and usable specification for blocks. We developed a domain specific formal model-based language specifically tailored for the specification of structure and semantics of blocks. This specification language is inspired from software product line concepts in order to ensure a correct and scalable management of the blocks variability. We have applied this specification and verification approach on chosen block examples from common industrial use cases and we have validated it on tool prototypes. Blocks are the core elements of the input language of automatic code generators used for control and command systems development. We show how our blocks formal specification can be translated as code annotations in order to ease and automate the generated code verification. Code annotations are verified using specialised static code analysis tools. Relying on synchronous observers to express high level requirements at the input model level, we show how formal block specification can also be used for the translation of high level requirements as verifiable code annotations discharged using the same specialised tooling. We finally target the assistance of code generation tools qualification activities by arguing on the ability to automatically generate qualification data such as requirements, tests or simulation results for the verification and development of automatic code generators from the formal block specification.

Les logiciels embarqués critiques de contrôle-commande sont soumis à des contraintes fortes englobant le déterminisme, la correction logique et la correction temporelle. Nous supposons que les spécifications sont exprimées à l'aide du langage formel de description d'architectures logicielles temps réel multipériodiques Prelude. L'objectif de cette thèse est, à partir d'un programme Prelude ou d'un ensemble de tâches temps réel dépendantes, de générer un code multithreadé exécutable sur une architecture multicœur tout en respectant la sémantique initiale. Pour cela, nous avons développé une boîte à outil, SchedMCore,permettant : - d'une part, la vérification formelle de l'ordonnançabilité. La vérification proposée est basée sur le parcours exhaustif du comportement avec pas de temps discret. Il est alors possible d'analyser des politiques en-ligne (FP, gEDF, gLLF et LLREF) mais également de calculer une affectation de priorité fixe valide et une séquence valide hors-ligne.- d'autre part, l'exécution multithreadée sur une cible multicœur. L'exécutif encode les politiques proposées étudiées dans la partie d'analyse d'ordonnançabilité, à savoir les quatre politiques en-ligne ainsi que les séquences valides générées. L'exécutif permet 3 modes d'utilisation, allant de la simulation temporelle à l'exécution temps précis des comportements des tâches. Il est compatible Posix et facilement portable sur divers OS. / A real-time control-command embedded system is subject to strong constraints such as determinism, logical and temporal correctness. We assume that the specifications are expressed using the formal software architecture description language Prelude, dedicated to real-time multiperiodic applications. The goal of this thesis is, given a Prelude program or dependent real-time taskset, to generate amultithreaded executable code over a multicore architecture while respecting the original semantic. To do so we have developed a toolbox, SchedMcore, that allows: - the formal verification of schedulability. The verification is based on the exhaustive exploration of the behaviour with a discret time frame. It is possible to analyse on-line policies (FP, gEDF, gLLF et LLREF), as well as to compute a fixed valid priority assignment and a valid off-line sequence.- the multithreaded execution over a multicore target. The framework encodes the same policies as those studied in the first part (the four on-line policies and the generated sequences). The framework provides three usage modes, from temporal simulation to time accurate execution. The executive is compatible with Posix and easily portable on several OS.

Cette thèse présente comment l’intégration de systèmes multi-agents au sein de systèmes embarqués peut permettre d’optimiser la gestion des tâches. Nous relevons un manque de flexibilité pour les systèmes embarqués et posons l’hypothèse d’une solution multi-agents permettant la prise en compte dynamique du contexte d’évolution du système. Les systèmes embarqués, intégrés à l’environnement utilisateur, sont contraints en termes d’espace physique et donc de ressources matérielles. Ces limites impliquent un besoin d’optimisation des ressources. Nous proposons d’expérimenter des algorithmes de négociation multi-agents pour déléguer des tâches entre les différentes ressources. Pour valider nos hypothèses, nous détaillons les caractéristiques des systèmes multi-agents, leurs comportements, leurs modèles,les plateformes sur lesquelles ils évoluent, leurs standards de communication et leurs algorithmes sociaux. Nous avons constaté que la majorité des travaux du domaine agent se concentraient sur d’autres problématiques. Par conséquent, nous avons proposé la formalisation de systèmes multiagents embarqués et d’une plateforme multi-agents adaptée. Nous avons ensuite expérimenté cette plateforme au sein de systèmes embarqués avec le cas d’étude du traitement d’images, notamment avec le calcul d’une interpolation de pixels. Nous avons mené des études de performances pour estimer le coût administratif d’une solution multiagents,puis avons considéré ces résultats au regard des gains de capacité de nos systèmes embarqués. Nos dernières expérimentations mettent à l’épreuve notre solution de délégation de tâches entre plusieurs cartes embarquées dans un contexte hétérogène. / This thesis shows how the integration of multi-agents systems within embedded systems can optimize tasks management. We notice a lack of flexibility for embedded systems and hypothesize that a multi-agents solution will allow the dynamic consideration of the system context of evolution. Embedded systems, being integrated into the user environment, are limited in terms of physical space and thus hardware resources. These limits involve the necessity to optimize the resources. We suggest experimenting multi-agents negotiation algorithms to delegate tasks between several resources. To validate our hypotheses, we detail the characteristics of multi-agents systems, their behavior, their models, the platforms on which they evolve, their communication standards and their social algorithms.We observed that the majority of the works of the multi-agents domain concentrated on other problems. Therefore, we proposed the formalization of embedded multi-agents systems and of anadapted multi-agents platform. We then experimented this platform within embedded systems with the case study of image processing, especially the calculation of a pixels interpolation.We led performance studies to estimate the administrative cost of a multi-agents solution, then considered these results in relation to the capacity earnings of our embedded systems. Our last experiments put to the test our solution of tasks delegation between several embedded cards within a heterogeneous context.