L’importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d’application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s’intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d’outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l’influence du flot d’informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l’applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l’angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d’un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d’établir un formalisme permettant la preuve du délai de bout-en-bout lors d’une démarche de développement incrémentale. / Real-time embedded systems are at the core of modern industrialized societies. They are a privileged target for the application of formal methods. The importance of real-time constraints in the specification of these systems requires the design of ad-hoc solutions. This work considers a class of real-time systems including those developed using OASIS, a tool-chain targeting hard real-time embedded systems developed at CEA LIST. We study the notion of end-to-end delay, which we propose to model as a constraint bearing directly on the influence of the input information flow over the output information flow . In order to cope with the growing complexity of real-time embedded systems, we study the possibility to apply this new notion of delay to the incremental development of such systems, by using both stepwise refinement and composition operators. We define the necessary and sufficient conditions to the preservation of the end-to-end delay by stepwise refinement. Similarly, we give sufficient conditions to compute the end-to-end delay in a compositional fashion. Together, these results permit to establish a formalism allowing to prove end-to-end delay properties in stepwise development methodologies.

Les travaux de recherche présentés dans cette thèse portent sur le problème de la perception de l’environnement en milieu urbain, complexe et dynamique et ce en présence de mesures extéroceptives bruitées et incomplètes obtenues à partir decapteurs embarqués. Le problème est formalisé sous l’angle de la fusion de données capteurs à l’aide d’une représentation spatiale de l’environnement. Ces travaux ont été réalisés pour la navigation autonome de véhicules intelligents dans le cadre du projet national ANR CityVIP. Après avoir considéré les principaux formalismes de modélisation de l’incertitude, un système de fusion de grilles spatio-référencées gérant l’incertitude avec des fonctions de croyances est étudié. Ce système est notamment capable de fusionner les mesures d’un lidar multi-nappes et multi-échos, obtenues à différents instants pour construire une carte locale dynamique sous la forme discrète d’une grille d’occupation évidentielle.Le principal avantage des fonctions de croyance est de représenter de manière explicite l’ignorance et ne nécessite donc pas d’introduire d’information à priori non fondée. De plus, ce formalisme permet d’utiliser facilement l’information conflictuelle pour déterminer la dynamique de la scène comme par exemple les cellules en mouvement. Le formalisme de grilles d’occupation évidentielles est présenté en détails et un modèle de capteur lidar multi-nappes et multi-echos est ensuite proposé. Deux approches de fusion séquentielle multi-grilles sont étudiées selon les paradigmes halocentréet égo-centré. Enfin, l’implémentation et les tests expérimentaux des approches sont décrits et l’injection d’informations géographiques connues a priori est étudiée. La plupart des travaux présentés ont été implémentés en temps réel sur un véhicule du laboratoire et de nombreux tests en conditions réelles ont été réalisés avec une interface d’analyse de résultat utilisant une rétro-projection dans une image grand angle. Les résultats ont été présentés dans 5 conférences internationales [Moras et al., 2010, Moras et al., 2011a, Moras et al., 2011b, Moras et al., 2012, Kurdej et al., 2012] etle système expérimental a servi à la réalisation de démonstrations officielles dans le cadre du projet CityVIP à Paris et lors de la conférence IEEE Intelligent Vehicles Symposium 2011 en Allemagne. / The research presented in this thesis focuses on the problem of the perception of the urban environment which is complex and dynamic in the presence of noisy and incomplete exteroceptive measurements obtained from on-board sensors. The problem is formalized in terms of sensor data fusion with a spatial representation of the environment. This work has been carried out for the autonomous navigation of intelligent vehicles within the national project ANR CityVIP. After having considered various formalisms to represent uncertainty, a fusion of spatio-referenced grids managing uncertainty with belief functions is studied. This system is capable of merging multi-layers and multi-echoes lidar measurements, obtainedat different time indexes to build a dynamic local map as a discrete evidential occupancy grid. The main advantages of belief functions are, firstly, to represent explicitly ignorance, which reduces the assumptions and therefore avoid introducing wrong a priori information and, secondly, to easily use conflicting information to determine the dynamics of the scene such as movements of the cells. The formalism of evidential occupancy grids is then presented in details and two multi-layers and multi-echos lidar sensor models are proposed. The propagation of the information through geometrical transformations is formalized in a similar way of image transformation framework. Then, the implementation of the approach is described and the injection of prior geographic information is finally investigated. Most of the works presented have been implemented in real time on a vehicle and many tests in real conditions have been realized. The results of these researches were presented through five international conferences [Moras et al., 2010, Moras et al., 2011a, Moras et al., 2011b, Moras et al., 2012], [Kurdej et al., 2012] and the experimental vehicle was presented at the official demonstration project CityVIP in Paris and at the IEEE Intelligent Vehicles Symposium 2011, in Germany.

Fruit d’un travail collaboratif entre le LAAS-CNRS de Toulouse et l’entreprise MEAS-France / TE Connectivity, ces travaux ont consisté en la mise en place d’une méthodologie permettant la réalisation de capteurs embarqués intelligents utilisant la fusion de données multi-physique pour estimer un paramètre en amoindrissant l’impact des variations environnementales.Nous explorons ici les méthodes liées à la modélisation et l’estimation de paramètres au travers des filtres de Kalman, pour les systèmes linéaires, et des filtres de Kalman étendus (EKF) et Unscented Kalman Filter pour les systèmes non-linéaires. Nous proposons ensuite des méthodes hybrides permettant d’obtenir le meilleur rapport charge de calculs/précision pour les systèmes présentant une évolution linéaire et une mesure non-linéaire.Après une étude de la complexité algorithmique des différentes solutions, nous proposons des méthodes permettant de diminuer la charge de calculs afin de satisfaire les contraintes temps-réel avec une faible puissance de calculs, telles que trouvées couramment dans les applications embarquées. La méthode développée est finalement appliquée sur deux cas applicatifs concrets : le capteur de qualité d’urée de la société MEAS-France/TE Connectivity et le capteur d’analyse du mouvement AREM développés au cours de la thèse au sein du LAAS-CNRS. / The work detailed in this document is the result of a collaborative effort of the LAAS-CNRS in Toulouse and MEAS-France / TE Connectivity during a period of three years.The goal here is to develop a methodology to design smart embedded sensors with the ability to estimate physical parameters based on multi-physical data fusion. This strategy tends to integrate sensors technologies, currently dedicated to lab measurements, in low powered embedded systems working in imperfects environments. After exploring model oriented methods, parameters estimations and Kalman filters, we detail various existing solutions upon which we can build a valid response to multi-physical data fusion problematics, for linear systems with the Kalman Filter, and for non-linear systems with the Extended Kalman Filter and the Unscented Kalman Filter.Then, we will synthesize a filter for hybrid systems, having a linear evolution model and a non-linear measurement model. For example, using the best of the two worlds in order to obtain the best complexity/precision ratio. Once we selected the estimation method, we detail computing power and algorithm complexity problematics in order to find available optimizations we can use to assess the usability of our system in a low power environment. Then we present the developed methodology application to the UQS sensor, sold by TE Connectivity, study case. This sensor uses near infra-red spectroscopy to determine the urea concentration in a urea/water solution, in order to control the nitrogen-oxyde depolluting process in gasoline engines. After a design principles presentation, we detail the model we created in order to represent the system, to simulate its behavior and to combine the measurement data to extract the desired concentration. During this step, we focus on the obstacles of our model calibration and the deviation compensation, due toworking conditions or to components aging process. Based on this development, we finally designed the hybrid models addressing the nominal working cases and the model re-calibration during the working duration of the product. After this, we presented obtained results, on simulated data, and on real-world measured data. Finally, we enhanced the methodology based on tabulated “black box” models which are easier to calibrate and cheaper to process. In conclusion, we reapplied our methodology to a different motion capture sensor, to compile all possible solutions and limits.

La CM (Criticité Mixte) est une solution pour intégrer différents niveaux de criticité dans le même système au sein des mécanismes industriels intégrant des infrastructures réseau différentes. Notre objectif est de proposer des solutions pour intégrer la criticité mixte dans des domaines industriels hautements contraints afin de mélanger des flux de différentes criticité au sein de la même infrastructure. Cette intégration implique des contraintes d'isolation : l'impact du traffic non critique sur le traffic critique doit être borné, et le plus faible possible. C'est une condition indispensable pour assurer le respect des contraintes de temps de transmission. Afin d'analyser ces délais de transmission et de centrer notre travail sur le déterminisme de ces transmissions, nous avons recours à une méthode de calcul de délai de bout en bout appelé l'approche par trajectoires. Dans ce travail, nous utilisons une version corrigée de l'approche par trajectoires, prenant en compte la serialisation des messages.Afin d'assurer les contraintes de délais dans les réseaux à criticité mixte, nous présentons tout d'abord un modèle théorique d'intégration de la criticité mixte. Ce modèles est issu de l'ordonnancement temps-réel en contexte processeur. Ce modèle présente une modélisation des flux considérant que chaque flux peut être de plusieurs niveaux de criticité.Pour intégrer la criticité mixte dans les réseaux temps-réel, nous proposons deux protocoles différents. Le premier est le protocole centralisé. Il est organisé autour de la désignation d'un noeud central dans le réseau, responsable de la synchronisation des niveaux de criticité de chaque noeud via a un mécanisme d'émission multiple fiable. Ce mécanisme est chargé de faire changer les niveaux de criticité de tous les noeuds au même instant. Le second protocole est basé sur une approche distribuée. Il propose une gestion locale à chaque noeud de la criticité. Chaque noeud gère individuellement son propre niveau de criticité interne. Ce protocol permet de préserver les transmissions d'une part du traffic non critique au sein du réseau, même en parallèle de transmissions de flux critiques.Afin de proposer une implémentation de ces protocoles dans Ethernet, nous détaillons comment réutiliser la marque de l'en-tête de Ethernet 802.1Q pour spécifier le niveau criticité d'un message directement au sein de la trame. Grâce à cette solution, chaque flux du réseau est marqué de son niveau de criticité et cette information peut être décodée par les noeuds du réseau afin d'opérer un ordonnancement en conséquence. De plus, en gestion centralisée, nous proposons une solution permettant d'intégrer les informations de gestion de la criticité directement dans les trames du protocole de synchronization d'horloge gls{PTP}.Durant notre travail, nous avons conçu un outil de simulation dénommé gls{ARTEMIS}. Cet outil est utilisé pour l'analyse de délais de transmission dans des réseaux temps-réel et pour l'analyse de scénarios d'ordonnancement à criticité mixte. Les résultats de simulation obtenus nous permettent de formuler différentes hypothèses sur les garanties de qualité de service offertes par les protocoles centralisé et décentralisé. En termes de transmission de trafic non critique, le protocole décentralisé permet d'assurer la transmission d'une certaine quantité de messages grâce au fait que certains noeuds du réseau soient resté en mode non-critique.Pour conclure, nous proposons des solutions d'intégration de la criticité mixte à la fois dans des contextes industriels lourds et dans des architectures Ethernet grand public. Les solutions proposées peuvent être à la fois adaptées à des réseaux synchronisés ou non synchronisés. Selon le protocole, la configuration individuelle à appliquer à chaque noeud peut être réduite afin de proposer des solutions implémentables sur du matériel moins coûteux / MC (Mixed-Criticality) is an answer for industrial systems requiring different network infrastructures to manage informations of different criticality levels inside the same system. Our purpose in this work is to find solutions to integrate gls{MC} inside highly constrained industrial domains in order to mix flows of various criticality levels inside the same infrastructure. This integration induces isolation constraints : the impact of non-critical traffic on critical traffic must be characterized and bounded. This a condition to respect timing constraints. To analyze transmission delays and focus on the determinism of transmissions, we use an end-to-end delay computation method called the trajectory approach. In our work, we use a corrected version of the trajectory approach taking into account the serialization of messages.To assure the respect of timing constraints in mixed critical networks, we first present a theoretical model of gls{MC} representation. This model is issued from gls{MC} tasks scheduling on processors. This model proposes a flow modelization which considers that each flow can be of one (low critical flows) or several criticality levels.To integrate gls{MC} inside gls{RT} networks, we propose two network protocols. The first is the centralized protocol. It is structured around the definition of a central node in the network, which is responsible for synchronizing the criticality level switch of each node through a reliable multicast protocol in charge of switching the network criticality level. This centralized protocol proposes solutions to detect the needs to change the criticality levels of all nodes and to transmit this information to the central node. The second protocol is based on a distributed approach. It proposes a local gls{MC} management on each node of a network. Each node individually manages its own internal criticality level. This protocol offers solutions to preserve when possible non-critical network flows even while transmitting critical flows in the network through weak isolation.In order to propose an implementation of these protocols inside Ethernet, we describe how to use Ethernet 802.1Q header tag to specify the criticality level of a message directly inside the frame. With this solution, each flow in the network is tagged with its criticality level and this information can be analyzed by the nodes of the network to transmit the messages from the flow or not. Additionnally, for the centralized approach, we propose a solution integrating gls{MC} configuration messages into gls{PTP} clock-synchronization messages to manage criticality configuration information in a network.In this work, we designed a simulation tool denoted as gls{ARTEMIS} (Another Real-Time Engine for Message-Issued Simulation). This tool is dedicated to gls{RT} networks analysis and gls{MC} integration scheduling scenarios. This tool, based on open and modular development guidelines, has been used all along our work to validate the theoretical models we presented through simulation. We integrated both centralized and decentralized protocols inside gls{ARTEMIS} core. The obtained simulations results allowed us to provide information about the gls{QOS} guarantees offered by both protocols. Concerning non-critical traffic : the decentralized protocol, by permitting specific nodes to stay in non-critical nodes, assures a highest success ratio of non-critical traffic correct transmission.As a conclusion, we propose solutions to integrate gls{MC} inside both industrial and gls{COTS} Ethernet architectures. The solutions can be either adapted to clock-synchronized or non clock-synchronized protocols. Depending on the protocol, the individual configuration required by each switch can be reduced to adapt these solutions to less costly network devices

Les constructeurs automobiles proposent de plus en plus des systèmes d'aide à la conduite, en anglais Advanced Driver Assistance Systems (ADAS), utilisant des caméras et des algorithmes de traitement d'images. Pour embarquer des applications ADAS, les fondeurs proposent des architectures embarquées hétérogènes. Ces Systems-on-Chip (SoCs) intègrent sur la même puce plusieurs processeurs de différentes natures. Cependant, avec leur complexité croissante, il devient de plus en plus difficile pour un industriel automobile de choisir un SoC qui puisse exécuter une application ADAS donnée avec le respect des contraintes temps-réel. De plus le caractère hétérogène amène une nouvelle problématique : la répartition des charges de calcul entre les différents processeurs du même SoC.Pour répondre à cette problématique, nous avons défini au cours de cette thèse une méthodologie globale de l’analyse de l'embarquabilité d'algorithmes de traitement d'images pour une exécution temps-réel. Cette méthodologie permet d'estimer l'embarquabilité d'un algorithme de traitement d'images sur plusieurs SoCs hétérogènes en explorant automatiquement les différentes répartitions de charge de calcul possibles. Elle est basée sur trois contributions majeures : la modélisation d'un algorithme et ses contraintes temps-réel, la caractérisation d'un SoC hétérogène et une méthode de prédiction de performances multi-architecture. / Car manufacturers increasingly provide Advanced Driver Assistance Systems (ADAS) based on cameras and image processing algorithms. To embed ADAS applications, semiconductor companies propose heterogeneous architectures. These Systems-on-Chip (SoCs) are composed of several processors with different capabilities on the same chip. However, with the increasing complexity of such systems, it becomes more and more difficult for an automotive actor to chose a SoC which can execute a given ADAS application while meeting real-time constraints. In addition, embedding algorithms on this type of hardware is not trivial: one needs to determine how to spread the computational load between the different processors, in others words the mapping of the computational load.In response to this issue, we defined during this thesis a global methodology to study the embeddability of image processing algorithms for real-time execution. This methodology predicts the embeddability of a given image processing algorithm on several heterogeneous SoCs by automatically exploring the possible mapping. It is based on three major contributions: the modeling of an algorithm and its real-time constraints, the characterization of a heterogeneous SoC, and a performance prediction approach which can address different types of architectures.

Le besoin en calculs est toujours plus important et difficile à satisfaire, spécialement dans le domaine de l’informatique embarquée qui inclue les voitures autonomes, drones et téléphones intelligents. Les systèmes embarqués doivent respecter des contraintes fortes de temps, de consommation et de sécurité. Les nouveaux processeurs parallèles et hétérogènes comme le MPPA® de Kalray utilisé dans cette thèse, doivent alors combiner haute performance et basse consommation. Pour cela, le MPPA® intègre 288 coeurs, regroupés en 18 clusters à mémoire locale partagée, un réseau sur puce et des moteurs DMA pour les communications. Ces processeurs sont difficiles à programmer, engendrant des coûts de développement importants. Cette thèse a pour objectif de simplifier leur programmation tout en optimisant les performances finales. Nous proposons pour cela AOS, une librairie de communication et synchronisation haute performance gérant les mémoires locales distribuées des processeurs clustérisés. La librairie atteint 70% de la crête matérielle pour des transferts supérieurs à 8 KB. Nous proposons plusieurs outils de développement basés sur AOS et des modèles de programmation flux-dedonnées pour accélérer le développement d’applications parallèles pour processeurs clustérisés, notamment OpenVX qui est un nouveau standard pour les applications de vision et les réseaux de neurones. Nous automatisons l’optimisation de l’application OpenVX en faisant du pré-chargement de données et en les fusionnants, pour éviter le mur de la bande passante mémoire externe. Les résultats montrent des facteurs d’accélération super linéaires. / The growing need for computing is more and more challenging, especially in the embedded system world with autonomous cars, drones, and smartphones. New highly parallel and heterogeneous processors emerge to answer this challenge. They operate in constrained environments with real-time requirements, reduced power consumption, and safety. Programming these new chips is a time-consuming and challenging task leading to huge software development costs. The Kalray MPPA® processor is a competitive example for low-power super-computing on a single chip. It integrates up to 288 VLIW cores grouped in 18 clusters, each fitted with shared local memory. These clusters are interconnected with a high-bandwidth network-on-chip, and DMA engines are used to communicate. This processor is used in this thesis for experimental results. We propose the AOS library enabling highperformance communications and synchronizations of distributed local memories on clustered manycores. AOS provides 70% of the peak hardware throughput for transfers larger than 8 KB. We propose tools for the implementation of static and dynamic dataflow programs based on AOS to accelerate the parallel application developments onto clustered manycores. We propose an implementation of OpenVX for clustered manycores on top of AOS. OpenVX is a standard based on dataflow for the development of computer vision and neural network computing. The proposed OpenVX implementation includes automatic optimizations like data prefetch to overlap communications and computations, or kernel fusion to avoid the main memory bandwidth bottleneck. Results show super-linear speedups.

De nos jours, l'augmentation de la complexité des systèmes embarqués impose la prise en charge, dès les premiers prototypes et au niveau logiciel, d'exigences habituellement traitées plus tardivement voire même seulement lors du passage en série, comme notamment les contraintes de sûreté de fonctionnement. Nous proposons une méthodologie de développement de logiciels embarqués pouvant répondre aux besoins et contraintes de développement de ces logiciels dans la phase de prototypage. La flexibilité de la méthodologie garantit une meilleure gestion des évolutions récurrentes caractérisant les logiciels dans cette phase de prototypage. Aussi, grâce à sa structure bien adaptée, l'aspect automatisé de son intégration et de sa mise en place, notre méthodologie garantit une réduction significative des coûts du passage en série et de la mise en place de normes telles que l'ISO 26262 ou la DO-178. Pour illustrer les résultats que nous obtenons grâce à notre méthodologie et la chaîne d'outils associée, nous l'appliquons dans le cadre d'un projet industriel d'innovation qui consiste à la robotisation d'un véhicule prototype. Le cas d'étude se concentre sur la fonction "accélérateur" de ce prototype. / Nowadays, the increasing complexity of embedded systems requires the management, from the first prototypes and software level, of requirements usually handled later even only when passing in production, such as including dependability constraints. We propose a development methodology for embedded software that can meet the needs and constraints of developing this software in the prototyping phase. The flexibility of the methodology ensures better management of recurring changes characterizing the software in the prototyping phase. Also, due to its well-adapted structure, and automated aspect of its integration and implementation, our methodology ensures a significant cost reduction of serialization and implementation of norms such as ISO 26262 or DO-178. To illustrate the results, we apply our methodology and the associated toolchain to an innovative industrial project which consists to robotize a prototype car. The case study focuses on the accelerator function of the prototype.

Dans le domaine de l'apprentissage machine, les réseaux de neurones profonds sont devenus la référence incontournable pour un très grand nombre de problèmes. Ces systèmes sont constitués par un assemblage de couches, lesquelles réalisent des traitements élémentaires, paramétrés par un grand nombre de variables. À l'aide de données disponibles pendant une phase d'apprentissage, ces variables sont ajustées de façon à ce que le réseau de neurones réponde à la tâche donnée. Il est ensuite possible de traiter de nouvelles données. Si ces méthodes atteignent les performances à l'état de l'art dans bien des cas, ils reposent pour cela sur un très grand nombre de paramètres, et donc des complexités en mémoire et en calculs importantes. De fait, ils sont souvent peu adaptés à l'implémentation matérielle sur des systèmes contraints en ressources. Par ailleurs, l'apprentissage requiert de repasser sur les données d'entraînement plusieurs fois, et s'adapte donc difficilement à des scénarios où de nouvelles informations apparaissent au fil de l'eau. Dans cette thèse, nous nous intéressons dans un premier temps aux méthodes permettant de réduire l'impact en calculs et en mémoire des réseaux de neurones profonds. Nous proposons dans un second temps des techniques permettant d'effectuer l'apprentissage au fil de l'eau, dans un contexte embarqué. / In the field of machine learning, deep neural networks have become the inescapablereference for a very large number of problems. These systems are made of an assembly of layers,performing elementary operations, and using a large number of tunable variables. Using dataavailable during a learning phase, these variables are adjusted such that the neural networkaddresses the given task. It is then possible to process new data.To achieve state-of-the-art performance, in many cases these methods rely on a very largenumber of parameters, and thus large memory and computational costs. Therefore, they are oftennot very adapted to a hardware implementation on constrained resources systems. Moreover, thelearning process requires to reuse the training data several times, making it difficult to adapt toscenarios where new information appears on the fly.In this thesis, we are first interested in methods allowing to reduce the impact of computations andmemory required by deep neural networks. Secondly, we propose techniques for learning on thefly, in an embedded context.

Un énorme progrès dans les performances des semiconducteurs a été accompli ces dernières années. Avec l’´émergence d’applications complexes, les systèmes embarqués doivent être à la fois performants et fiables. Une multitude de travaux ont été proposés pour améliorer l’efficacité des systèmes embarqués en réduisant le décalage entre la flexibilité des solutions logicielles et la haute performance des solutions matérielles. En vertu de leur nature reconfigurable, les FPGAs (Field Programmable Gate Arrays) représentent un pas considérable pour réduire ce décalage performance/flexibilité. Cependant, la reconfiguration dynamique a toujours souffert d’une limitation liée à la latence de reconfiguration.Dans cette thèse, une nouvelle technique de reconfiguration dynamiqueau niveau ”grain-moyen” pour les circuits à base de blocks DSP48E1 est proposée. L’idée est de profiter de la reprogrammabilité des blocks DSP48E1 couplée avec un circuit d’interconnection reconfigurable afin de changer la fonction implémentée par le circuit en un cycle horloge. D’autre part, comme les nouvelles technologies s’appuient sur la réduction des dimensions des transistors ainsi que les tensions d’alimentation, les circuits électroniques sont devenus de plus en plus susceptibles aux fautes transitoires. L’impact de ces erreurs au niveau système peut être catastrophique et les SETs (Single Event Transients) sont devenus une menace tangible à la fiabilité des systèmes embarqués, en l’occurrence pour les applications critiques comme les systèmes de transport. Les techniques de fiabilité qui se basent sur des taux d’erreurs (SERs) surestimés peuvent conduire à un gaspillage de ressources et par conséquent un cout en consommation de puissance électrique. Il est primordial de prendre en compte le phénomène de masquage d’erreur pour une estimation précise des SERs.Cette thèse propose une nouvelle modélisation inter-couches de la vulnérabilité des circuits qui combine les mécanismes de masquage au niveau transistor (TLM) et le masquage au niveau Système (SLM). Ce modèle est ensuite utilisé afin de construire une architecture adaptative tolérante aux fautes qui évalue la vulnérabilité effective du circuit en runtime. La stratégie d’amélioration de fiabilité est adaptée pour ne protéger que les parties vulnérables du système, ce qui engendre un circuit fiable avec un cout optimisé. Les expérimentations effectuées sur un système de détection d’obstacles à base de radar pour le transport ferroviaire montre que l’approche proposée permet d’´établir un compromis fiabilité/ressources utilisées. / During the last few decades, a tremendous progress in the performance of semiconductor devices has been accomplished. In this emerging era of high performance applications, machines need not only to be efficient but also need to be dependable at circuit and system levels. Several works have been proposed to increase embedded systems efficiency by reducing the gap between software flexibility and hardware high-performance. Due to their reconfigurable aspect, Field Programmable Gate Arrays (FPGAs) represented a relevant step towards bridging this performance/flexibility gap. Nevertheless, Dynamic Reconfiguration (DR) has been continuously suffering from a bottleneck corresponding to a long reconfiguration time.In this thesis, we propose a novel medium-grained high-speed dynamic reconfiguration technique for DSP48E1-based circuits. The idea is to take advantage of the DSP48E1 slices runtime reprogrammability coupled with a re-routable interconnection block to change the overall circuit functionality in one clock cycle. In addition to the embedded systems efficiency, this thesis deals with the reliability chanllenges in new sub-micron electronic systems. In fact, as new technologies rely on reduced transistor size and lower supply voltages to improve performance, electronic circuits are becoming remarkably sensitive and increasingly susceptible to transient errors. The system-level impact of these errors can be far-reaching and Single Event Transients (SETs) have become a serious threat to embedded systems reliability, especially for especially for safety critical applications such as transportation systems. The reliability enhancement techniques that are based on overestimated soft error rates (SERs) can lead to unnecessary resource overheads as well as high power consumption. Considering error masking phenomena is a fundamental element for an accurate estimation of SERs.This thesis proposes a new cross-layer model of circuits vulnerability based on a combined modeling of Transistor Level (TLM) and System Level Masking (SLM) mechanisms. We then use this model to build a self adaptive fault tolerant architecture that evaluates the circuit’s effective vulnerability at runtime. Accordingly, the reliability enhancement strategy is adapted to protect only vulnerable parts of the system leading to a reliable circuit with optimized overheads. Experimentations performed on a radar-based obstacle detection system for railway transportation show that the proposed approach allows relevant reliability/resource utilization tradeoffs.

Alors que les systèmes embarqués sont de plus en plus nombreux, complexes, connectés et chargés de tâches critiques, la question de comment intégrer l'analyse précise de sécurité à la conception de systèmes embarqués doit trouver une réponse. Dans cette thèse, nous étudions comment les méthodes de vérification formelle automatiques peuvent aider les concepteurs de systèmes embarqués à évaluer l'impact des modifications logicielles et matérielles sur la sécurité des systèmes. Une des spécificités des systèmes embarqués est qu'ils sont décrits sous la forme de composants logiciels et matériels interagissant. Vérifier formellement de tels systèmes demande de prendre tous ces composants en compte. Nous proposons un exemple d'un tel système (basé sur Intel SGX) qui permet d'établir un canal sécurisé entre un périphérique et une application. Il est possible d'en vérifier un modèle de haut-niveau ou une implémentation bas-niveau. Ces deux niveaux diffèrent dans le degré d'intrication entre matériel et logiciel. Dans le premier cas, nous proposons une approche orientée modèle, à la fois au niveau partitionnement et conception logicielle, permettant une description à haut niveau d'abstraction du matériel et du logiciel et permettant une transformation de ces modèles en une spécification formelle sur laquelle une analyse de sécurité peut être effectuée avec l'outil ProVerif. Dans le second cas, nous considérons une implémentation logicielle et un modèle matériel plus concret pour effectuer des analyses de sécurité plus précises toujours avec ProVerif. / As embedded systems become more complex, more connected and more involved in critical tasks, the question of how strict security analysis can be performed during embedded system design needs to be thoroughly addressed. In this thesis, we study how automated formal verification can help embedded system designers in evaluating the impact of hardware and software modifications on the security of the whole system. One of the specificities of embedded system design-which is of particular interest for formal verification-is that the system under design is described as interacting hardware and software components. Formally verifying these systems requires taking both types of components into account. To illustrate this fact, we propose an example of a hardware/software co-design (based on Intel SGX) that provides a secure channel between a peripheral and an application. Formal verification can be performed on this system at different levels: from a high-level view (without describing the implementations) or from a low-level implementation. These two cases differ in terms of how tightly coupled the hardware and software components are. In the first case, we propose a model-based approach-for both the partitioning and software design phases- which enables us to describe software and hardware with high-level models and enables a transformation of these models into a formal specification which can be formally analyzed by the ProVerif tool. In the second case, we consider a software implementation and a more concrete