Cette thèse discute le problème de test de production en grand volume des circuits radio-fréquences (RF) et à ondes millimétriques (mm-wave). Le test des fonctionnalités RF et à ondes millimétriques est très onéreux. Le test intégré est une alternative prometteuse pour faciliter la procédure et réduire les couts, mais il est difficile à mettre en œuvre car il ne faut en aucun cas qu'il réduit la performance du circuit sous test (CUT). Dans cette thèse, nous étudions une technique du test intégré qui repose sur l'utilisation de capteurs non-intrusifs qui prend en compte la variabilité du procédé de fabrication. Cette technique est extrêmement intéressante pour les concepteurs des circuits RF et mm-wave car il leur permet de dissocier le test de la conception. Les capteurs non-intrusifs sont constitués d'étages analogiques triviaux et de composants simples qui sont copiés de la topologie du CUT et sont placés sur la puce à proximité du CUT. Ils offrent simplement une "image" des variations du procédé de fabrication, ce qui leur permet de suivre les variations de performance du CUT. En substance, cette technique tire parti des phénomènes non désirés de variabilité de procédé de fabrication. Le paradigme du test alternatif est utilisé pour estimer les performances du CUT à partir des mesures des capteurs non intrusifs, afin de remplacer les tests standards qui mesurent les performances directement. Ce principe de test est appliqué à deux différents CUTs, nommément un amplificateur à bas bruit à 2.4GHz réalisé en CMOS 65nm et un amplificateur à bas bruit large bande à 60GHz réalisé en CMOS 65nm. Nous démontrons qu'en ajoutant quelques capteurs non-intrusifs sur la puce, qui n'engendrent pratiquement pas de surcout de surface, et en obtenant de ces capteurs non-intrusifs certaines mesures dans le domaine continu et à basse fréquence, nous sommes capable de suivre les variations de toutes les performances du CUT avec une erreur de prédiction moyenne inférieure à l’écart-type de la performance, et une erreur de prédiction maximum qui est inférieure ou au moins comparable aux erreurs de mesure dans un équipement de test automatisé conventionnel. / This thesis addresses the high-volume production test problem for RF and millimeter-wave (mm-wave) circuits. Testing the RF/mm-wave functions of systems-on-chip (SoCs) incurs a very high cost. Built-in test is a promising alternative to facilitate testing and reduce costs, but it is challenging since it should by no means degrade the performance of the Circuit Under Test (CUT). In this work, we study a built-in test technique which is based on non-intrusive variation-aware sensors. The non-intrusive property is very appealing for designers since the sensors are totally transparent to the design and, thereby, the test is completely dissociated from the design. The non-intrusive sensors are dummy analog stages and single layout components that are copied from the topology of the CUT and are placed on the die in close physical proximity to the CUT. They simply offer an “image” of process variations and by virtue of this they are capable of tracking variations in the performances of the CUT. In essence, the technique capitalizes on the undesired phenomenon of process variations. The alternate test paradigm is employed to map the outputs of the non-intrusive sensors to the performances of the CUT, in order to replace the standard tests for measuring the performances directly. The proposed test idea is applied to two different CUTs, namely a 2.4GHz CMOS 65nm inductive degenerated Low-Noise Amplifier (LNA) and a wide-band mm-wave 60GHz CMOS 65nm 3-stage LNA. We demonstrate that by adding on-chip a few non-intrusive sensors of practically zero area-overhead and by obtaining on these non-intrusive sensors DC or low-frequency measurements, we are able to track variations in all performances of the CUT with an average prediction error lower than one standard deviation of the performance and a maximum prediction error that is lower or at least comparable to the measurement and repeatability errors in a conventional Automatic Test Equipment (ATE) environment.

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 plates-formes MPSoC permettent de satisfaire les contraintes de performance, de flexibilité et de consommation énergétique requises par les systèmes embarqués émergents. Elles intègrent un nombre important de processeurs, des blocs de mémoire et des périphériques, hiérarchiquement organisés par un réseau d'interconnexion. Le développement du logiciel est réputé difficile, notamment dû à la gestion d'un grand nombre d'entités (tâches/threads/processus). L'exécution concurrente de ces entités permet d'exploiter efficacement l'architecture mais complexifie le processus de mise au point et notamment l'analyse des erreurs. D'une part, les exécutions peuvent être non-déterministes notamment dû à la concurrence, c'est à dire qu'elles peuvent se dérouler d'une manière différente à chaque reprise. En conséquence, il n'est pas garanti qu'une erreur se produirait durant la phase de mise au point. D'autre part, la complexité de l'architecture et de l'exécution peut rendre trop important le nombre d'éléments à analyser afin d'identifier une erreur. Il pourrait donc être difficile de se focaliser sur des éléments potentiellement fautifs. Un des défis majeurs du développement logiciel MPSoC est donc de réduire le temps de la mise au point. Dans cette thèse, nous proposons une méthodologie de mise au point qui aide le développeur à identifier les erreurs dans le logiciel MPSoC. Notre premier objectif est de déboguer une même exécution plusieurs fois afin d'analyser des sources potentielles de l'erreur jusqu'à son identification. Nous avons donc identifié les sources de non-déterminisme MPSoC et proposé des mécanismes de ré-exécution déterministe les plus adaptés. Notre deuxième objectif vise à minimiser les ressources pour reproduire une exécution afin de satisfaire la contrainte MPSoC de maîtrise de l'intrusion. Nous avons donc utilisé des mécanismes efficaces de ré-exécution déterministe et considéré qu'une partie du comportement non-déterministe. Le troisième objectif est de permettre le passage à l'échelle, c'est à dire de déboguer des exécutions caractérisées par un nombre d'éléments de plus en plus croissant. Nous avons donc proposé une méthode qui permet de circonscrire et de déboguer qu'une partie de l'exécution. De plus, cette méthode s'applique aux différents types d'architectures et d'applications MPSoC. / MPSoC platforms provide high performance, low power consumption and flexi-bility required by the emerging embedded systems. They incorporate many proces-sing units, memory blocs and peripherals, hierarchically organized by interconnec-tion network. The software development is known to be difficult, namely due to themanagement of multiple entities (tasks/threads/processes). The concurrent execu-tion of these entities allows to exploit efficiently the architecture but complicatesthe refinement process of the software and especially the debugging activity. Onthe one hand, the executions of the software can be non-deterministic, namely dueto the concurrency, i.e. they perform differently each time. Consequently, thereis no guaranties that an error will occur during the debugging activity. On theother hand, the complexity of the architecture and the execution can increase theelements to be analyzed in the debugging process. As a result, it can be difficultto concentrate on the potentially faulty elements. Therefore, one of the most im-portant challenges in the development process of MPSoC software is to reduce thetime of the refinement process.In this thesis, we propose a new methodology to refine the MPSoC softwarewhich helps the developers to do the debugging activity. Our first objective is tobe able to debug the same execution several times in order to analyze potentialsources of the error. To do so, we identified the sources of non-determinism in theMPSoC software executions and propose the most appropriate methods to recordand replay them. Our second objective is to reduce the execution overhead requi-red by the record mechanisms to limit the intrusiveness which is an importantMPSoC constraint. To accomplish this objective, we consider a part of the non-deterministic behaviour and selected efficient record-replay methods. The thirdobjective is to provide a scalable solution, i.e. to be able to debug more and morecomplex executions, characterized by an increasing number of elements. Therefore,we propose a partial replay method which allows to isolate and debug a fraction ofthe execution elements. Moreover, this method applies to different types of archi-tectures and applications MPSoC.

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.

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

Les 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.

Lors d’un développement logiciel, et plus particulièrement d’un développement d’applications embarquées avioniques, les activités de vérification représentent un coût élevé. Une des pistes prometteuses pour la réduction de ces coûts est l’utilisation de méthodes formelles. Ces méthodes s’appuient sur des fondements mathématiques et permettent d’effectuer des tâches de vérification à forte valeur ajoutée au cours du développement. Les méthodes formelles sont déjà utilisées dans l’industrie. Cependant, leur difficulté d’appréhension et la nécessité d’expertise pour leur mise en pratique sont un frein à leur utilisation massive. Parallèlement au problème des coûts liés à la vérification logicielle, vient se greffer la complexification des logiciels et du contexte de développement. L’Ingénierie Dirigée par les Modèles (IDM) permet de faire face à ces difficultés en proposant des modèles, ainsi que des activités pour en tirer profit.Le but des travaux présentés dans cette thèse est d’établir un lien entre les méthodes formelles et l’IDM afin de proposer à des utilisateurs non experts une approche de vérification formelle et automatique de programmes susceptible d’améliorer les processus de vérification actuels. Nous proposons de générer automatiquement sur le code source des annotations correspondant aux propriétés comportementales attendues du logiciel, et ce, à partir de son modèle de conception. Ces annotations peuvent ensuite être vérifiées par des outils de preuve déductive, afin de s’assurer que le comportement du code est conforme au modèle. Cette thèse CIFRE s’inscrit dans le cadre industriel d’Atos. Il est donc nécessaire de prendre en compte le contexte technique qui s’y rattache. Ainsi, nous utilisons le standard UML pour la modélisation,le langage C pour l’implémentation et l’outil Frama-C pour la preuve du code. Nous tenons également compte des contraintes du domaine du logiciel avionique dans lequel Atos est impliqué et notamment les contraintes liées à la certification.Les contributions de cette thèse sont la définition d’un sous-ensemble des machines à états UML dédié à la conception comportementale de logiciel avionique et conforme aux pratiques industrielles existantes, la définition d’un patron d’implémentation C, la définition de patrons de génération des propriétés comportementales sur le code à partir du modèle et enfin l’implémentation de l’approche dans un prototype compatible avec l’environnement de travail des utilisateurs potentiels en lien avec Atos. L’approche proposée est finalement évaluée par rapport à l’objectif de départ, par rapport aux attentes de la communauté du génie logiciel et par rapport aux travaux connexes. / During software development, and more specifically embedded avionics applications development, verification is very expensive. A promising lead to reduce its costs is the use of formal methods. Formal methods are mathematical techniques which allow performing rigorous and high-valued verification tasks during software development. They are already applied in industry. However, the high level of expertise required for their use is a major obstacle for their massive use. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The goal of this PhD thesis is to establish a link between formal methods and MDE in order to propose to non-expert users a formal and automatic software verification approach which helps to improve software verification processes. We propose to automatically generate annotations, corresponding to the expected behavioural properties of the software, from the design model to the source code. Then, these annotations can be verified using deductive proof tools in order to ensure that the behaviour of the code conforms to the design model. This PhD thesis takes place in the industrial context of Atos. So, it is necessary to take into account its technical specificities. We use UML for the design modeling, the C language for the software implementation and the Frama-C tool for the proof of this implementation. We also take into account the constraints of the avionics field in which Atos intervenes, and specifically the certification constraints. The contributions of this PhD thesis are the definition of a subset of UML state machine dedicated to the behavioural design of embedded avionics software and in line with current industrial practices, the definition of a C implementation pattern, the definition of generation patterns for the behavioural properties from the design model to the source code and the implementation of the whole approach in a prototype in accordance with the working environment of the potential users associated with Atos. The proposed approach is then assessed with respect to the starting goal of the thesis, to the expectation of the software engineering community and to related work.

Avec l’apparition des nouvelles technologies de communication, le nombre des systèmes embarqués avionique et automobile est en constante augmentation. La gestion des communications entre ces systèmes devient alors de plus en plus complexe à mettre en oeuvre dans un contexte où les contraintes temporelles et environnementales sont très fortes et où le taux d’échanges de messages en augmentation continuelle. L’utilisation optimale des réseaux pour acheminer les données tout en respectant les contraintes temporelles imposées est essentielle du point de vue de la sûreté de fonctionnement. Historiquement, pour répondre aux problématiques d’efficacité et de sûreté, les industriels ont développé une palette de réseaux embarqués dédiés à leurs applications cibles (CAN, LIN, . . . ). Ces réseaux présentaient des débits relativement faibles à un moment où un besoin croissant en bande passante se faisait ressentir. le choix d’utiliser le concept de composants dit ‘sur étagères’ (off the shelf COTS) permettait alors de pallier à ce nouveau besoin. Dans un souci de conservation des capacités des réseaux à garantir les contraintes temporelles imposées par les systèmes embarqués temps réel, les industriels ont dû adapter ce concept de composants sur étagères aux systèmes embarqués. L’intérêt de l’utilisation de ces composants est un gain non négligeable en bande passante et en poids pour des coûts de développements relativement faibles. L’introduction de ces composants nouveaux s’est faite de telle sorte que leur impact sur les standards préexistants et les systèmes connectés soit minimal. C’est ainsi que les réseaux dit ‘hétérogènes’ ont vu leur apparition. Ces réseaux constituent une hybridation entre les technologies embarquées historiques et les composants sur étagère. Ils consistent en des réseaux d’extrémité utilisant des technologies éprouvées (telles que le CAN) interconnectés via des passerelles à un réseau fédérateur (backbone) utilisant des composants sur étagères. Dès lors, le défi majeur à relever lors de l’utilisation d’un réseau fédérateur est de respecter les contraintes temporelles des applications sollicitant les différents réseaux. L’objectif est mis à mal sur les points d’interconnexion des réseaux hétérogènes (Passerelles). Ainsi l’approche principale utilisée pour le passage d’un réseau à un autre est l’encapsulation de trames. Pour atteindre l’optimalité de performance de cette technique plusieurs paramètres sont à prendre en compte tels que le nombre de trames à encapsuler, les ordonnancements utilisés, le coût en bande passante ainsi que l’impact sur les distributions de délais (gigue). Dans l’optique de préservation des performances des réseaux, l’objet de nos travaux porte sur l’étude, la comparaison et la proposition de techniques permettant l’interconnexion de réseaux hétérogènes temps réels à la fois pour des applications à faibles et à fortes contraintes temporelles. Après un état de l’art sur les réseaux temps réel, nous spécifions différentes techniques d’interconnexion de réseaux hétérogènes, puis, nous présentons une étude de cas basée sur une architecture réseau interconnectant différents bus CAN via un réseau fédérateur sans fil Wi-Fi. L’étude que nous avons menée montre, par le biais de différentes simulations, que cette architecture réseau est une bonne candidate pour la transmission de flux à contraintes temporelles faibles. Une architecture réseau interconnectant différents bus CAN via un réseau fédérateur Ethernet commuté est ensuite considérée dans une seconde étude de cas ciblant les applications à fortes contraintes temporelles. Dans un premier temps, nous prenons en compte le cas d’un réseau fédérateur Ethernet-PQSE et, dans un second temps, le cas d’Ethernet-AVB. Cette étude nous permet de montrer l’impact des différentes techniques d’interconnexion sur les délais des flux du réseau. / With the emergence of new communication technologies, the number of avionics and automotive embedded systems is constantly increasing. The management of communications between these systems becomes increasingly complex to implement in a context where temporal and environmental constraints are very strong and where messages exchange rate is continuously increasing. The optimal use of networks to transmit data while fulfilling the imposed temporal constraints is essential from a safety point of view. Historically, in order to address safety and efficiency issues, manufacturers have developed a range of embedded networks dedicated to their target applications (CAN, LIN, . . . ). These networks have relatively low bit rates at a point of time where a growing need for bandwidth was felt. To overcome this new need, the choice of using the concept of so-called ’off-theshelf’ components (COTS) has been made. In order to preserve the networks abilities to guarantee the temporal constraints imposed by the real time embedded systems, manufacturers had to adapt the concept of off-the-shelf components to embedded systems. The benefits of using these components is a non-negligible gain in bandwidth and weight for relatively low development costs. The introduction of these new components has been made in such a way that their impact on pre-existing standards and connected systems is minimal. thereby, so-called ’heterogeneous’ networks have emerged. These networks are a hybridization of historical embedded technologies and off-the-shelf components. They consist of stub networks using proven technologies (such as CAN) interconnected via gateways to a backbone network using off-the-shelf components. Thus, the major challenge while using a heterogeneous network is to respect the temporal constraints of the applications requesting the different parts of the networks. This objective can be damaged at the interconnection points of the heterogeneous networks (Gateways). The main used approach to pass frames from one network to another is the encapsulation. To achieve the optimum performances of this technique, several parameters have to be considered such as the number of frames encapsulated, the used scheduling policy, the bandwidth cost as well as the impact on delay distributions (jitter). In order to preserve networks performances, the aim of our work is to study, compare and propose techniques ennabling the interconnection of real-time heterogeneous networks for application with both soft and hard temporal constraints. After a state of the art on real-time networks, we have specified different techniques for the interconnection of heterogeneous networks, then we have presented a case study based on a network architecture interconnecting different CAN buses via a wireless backbone network (Wi-Fi ). The study we conducted shows, through various simulations, that this network architecture is a good contender for the transmission of flows with soft temporal constraints. A network architecture interconnecting different CAN busses via a switched Ethernet backbone is considered in a second case study targeting applications with hard temporal constraints. Two different Ethernet backbone networks are taken into account. We studied first, the case of a switched Ethernet-PQSE backbone network. Then the case of a switched Ethernet-AVB backbone is considered. This study enabled us to highlight the impact of the different used interconnection techniques on network flows delays.

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.

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