Dans le domaine des soins de santé, l'imagerie médicale a rapidement progressé et est aujourd'hui largement utilisés pour le diagnostic médical et le traitement du patient. La santé mobile devient une tendance émergente qui fournit des soins de santé et de diagnostic à distance. de plus, à l'aide des télécommunications, les données médicale incluant l'imagerie médicale et les informations du patient peuvent être facilement et rapidement partagées entre les hôpitaux et les services de soins de santé. En raison de la grande capacité de stockage et de la bande passante de transmission limitée, une technique de compression efficace est nécessaire. En tant que technique de compression d'image certifiée médicale, WAAVES fournit des taux de compression élevé, tout en assurant une qualité d'image exceptionnelle pour le diagnostic médical. Le défi consiste à transmettre à distance l'image médicale de l'appareil mobile au centre de soins de santé via un réseau à faible bande passante. Nos objectifs sont de proposer une solution de compression d'image intégrée à une vitesse de compression de 10 Mo/s, tout en maintenant la qualité de compression. Nous examinons d'abord l'algorithme WAAVES et évaluons sa complexité logicielle, basée sur un profilage précis du logiciel qui indique un complexité de l'algorithme WAAVES très élevée et très difficile à optimiser de contraintes très sévères en terme de surface, de temps d'exécution ou de consommation d'énergie. L'un des principaux défis est que les modules Adaptative Scanning et Hierarchical Enumerative Coding de WAAVES prennent plus de 90% du temps d'exécution. Par conséquent, nous avons exploité plusieurs possibilités d'optimisation de l'algorithme WAAVES pour simplifier sa mise en œuvre matérielle. Nous avons proposé des méthodologies de mise en œuvre possible de WAAVES, en premier lieu une mise en œuvre logiciel sur plateforme DSP. En suite, nous avons réalisé notre implémentation matérielle de WAAVES. Comme les FPGAs sont largement utilisés pour le prototypage ou la mise en œuvre de systèmes sur puce pour les applications de traitement du signal, leur capacités de parallélisme massif et la mémoire sur puce abondante permet une mise en œuvre efficace qui est souvent supérieure aux CPUs et DSPs. Nous avons conçu WAAVES Encoder SoC basé sur un FPGA de Stratix IV de chez Altera, les deux grands blocs coûteux en temps: Adaptative Scanning et Hierarchical Enumerative Coding sont implementés comme des accélérateurs matériels. Nous avons réalisé ces accélérateurs avec deux niveaux d'optimisations différents et les avons intégrés dans notre Encodeur SoC. La mise en œuvre du matérielle fonctionnant à 100MHz fournit des accélérations significatives par rapport aux implémentations logicielles, y compris les implémentations sur ARM Cortex A9, DSP et CPU et peut atteindre une vitesse de codage de 10 Mo/s, ce qui répond bien aux objectifs de notre thèse. / In the field of healthcare, developments in medical imaging are progressing very fast. New technologies have been widely used for the support of patient medical diagnosis and treatment. The mobile healthcare becomes an emerging trend, which provides remote healthcare and diagnostics. By using telecommunication networks and information technology, the medical records including medical imaging and patient's information can be easily and rapidly shared between hospitals and healthcare services. Due to the large storage size and limited transmission bandwidth, an efficient compression technique is necessary. As a medical certificate image compression technique, WAAVES provides high compression ratio while ensuring outstanding image quality for medical diagnosis. The challenge is to remotely transmit the medical image through the mobile device to the healthcare center over a low bandwidth network. Our goal is to propose a high-speed embedded image compression solution, which can provide a compression speed of 10MB/s while maintaining the equivalent compression quality as its software version. We first analyzed the WAAVES encoding algorithm and evaluated its software complexity, based on a precise software profiling, we revealed that the complex algorithm in WAAVES makes it difficult to be optimized for certain implementations under very hard constrains, including area, timing and power consumption. One of the key challenges is that the Adaptive Scanning block and Hierarchical Enumerative Coding block in WAAVES take more than 90% of the total execution time. Therefore, we exploited several potentialities of optimizations of the WAAVES algorithm to simplify the hardware implementation. We proposed the methodologies of the possible implementations of WAAVES, which started from the evaluation of software implementation on DSP platforms, following this evaluation we carried out our hardware implementation of WAAVES. Since FPGAs are widely used as prototyping or actual SoC implementation for signal processing applications, their massive parallelism and abundant on-chip memory allow efficient implementation that often rivals CPUs and DSPs. We designed our WAAVES Encoder SoC based on an Altera's Stratix IV FPGA, the two major time consuming blocks: Adaptive Scanning and Hierarchical Enumerative Coding are designed as IP accelerators. We realized the IPs with two different optimization levels and integrated them into our Encoder SoC. The Hardware implementation running at 100MHz provides significant speedup compared to the other software implementation including ARM Cortex A9, DSP and CPU and can achieve a coding speed of 10MB/s that fulfills the goals of our thesis.

Les informations contenues dans les cartes routières numériques revêtent une importance grandissante dans le domaine des véhicules intelligents. La prise en compte d’environnements de plus en plus complexes a augmenté le niveau de précision exigé des informations cartographiques. Les cartes routières numériques, considérées ici comme des bases de données géographiques, contiennent des informations contextuelles sur le réseau routier, facilitant la compréhension correcte de l’environnement. En les combinant avec les données provenant des capteurs embarqués, une représentation plus fine de l’environnement peut être obtenue, améliorant grandement la compréhension de contexte du véhicule et la prise de décision. La performance des différents capteurs peut varier grandement en fonction du lieu considéré, ceci étant principalement dû à des facteurs environnementaux. Au contraire, une carte peut fournir ses informations de manière fiable, sans être affectée par ces éléments extérieurs, mais pour cela, elle doit reposer sur un autre élément essentiel : une source de localisation. Le secteur automobile utilise les systèmes de localisation globale par satellite (GNSS) à des fins de localisation absolue, mais cette solution n’est pas parfaite, étant soumise à différentes sources d’erreur. Ces erreurs sont elles aussi dépendantes de l’environnent d’évolution du véhicule (par exemple, des multi-trajets causés par des bâtiments). Nous sommes donc en présence de deux systèmes centraux, dont les performances sont d´dépendantes du lieu considéré. Cette étude se focalise sur leur dénominateur commun : la carte routière numérique, et son utilisation en tant qu’outil d’évaluation de leur performance. L’idée développée durant cette thèse est d’utiliser la carte en tant que canevas d’apprentissage, pour stocker des informations géoréférencées sur la performance des diésèrent capteurs équipant le véhicule, au cours de trajets répétitifs. Pour cela, une localisation robuste, relative à la carte, est nécessaire au travers d’une méthode de map-matching. La problématique principale réside dans la différence de précision entre la carte et le positionnement GNSS, créant des situations ambigües. Durant cette thèse, un algorithme de map-matching a été conçu pour gérer ces ambigüités en fournissant des hypothèses multiples lorsque nécessaire. L’objectif est d’assurer l’intégrité de l’algorithme en retournant un ensemble d’hypothèses contenant l’hypothèse correcte avec une grande probabilité. Cet algorithme utilise les capteurs proprioceptifs dans une approche de navigation à l’estime aidée d’informations cartographiques. Une procédure d’évaluation de cohérence, utilisant le GNSS comme information redondante de positionnement est ensuite appliquée, visant à isoler une hypothèse cohérente unique qui pourra ainsi être utilisée avec confiance dans le processus d’écriture dans la carte. L’utilisation de la carte numérique en écriture/lecture a été évaluée et la procédure complète d’écriture a été testée sur des données réelles, enregistrées par des véhicules expérimentaux sur route ouverte. / The information stored in digital road maps has become very important for intelligent vehicles. As intelligent vehicles address more complex environments, the accuracy requirements for this information have increased. Regarded as a geographic database, digital road maps contain contextual information about the road network, crucial for a good understanding of the environment. When combined with data acquired from on-board sensors, a better representation of the environment can be made, improving the vehicle’s situation understanding. Sensors performance can vary drastically depending on the location of the vehicle, mainly due to environmental factors. Comparatively, a map can provide prior information more reliably but to do so, it depends on another essential component: a localization system. Global Navigation Satellite Systems (GNSS) are commonly used in automotive to provide an absolute positioning of the vehicle, but its accuracy is not perfect: GNSS are prone to errors, also depending greatly on the environment (e.g., multipaths). Perception and localization systems are two important components of an intelligent vehicle whose performances vary in function of the vehicle location. This research focuses on their common denominator, the digital road map, and its use as a tool to assess their performance. The idea developed during this thesis is to use the map as a learning canvas, to store georeferenced information about the performance of the sensors during repetitive travels. This requires a robust localization with respect to the map to be available, through a process of map-matching. The main problematic is the discrepancy between the accuracy of the map and of the GNSS, creating ambiguous situations. This thesis develops a map-matching algorithm designed to cope with these ambiguities by providing multiple hypotheses when necessary. The objective is to ensure the integrity of the result by returning a hypothesis set containing the correct matching with high probability. The method relies on proprioceptive sensors via a dead-reckoning approach aided by the map. A coherence checking procedure using GNSS redundant information is then applied to isolate a single map-matching result that can be used to write learning data with confidence in the map. The possibility to handle the digital map in read/write operation has been assessed and the whole writing procedure has been tested on data recorded by test vehicles on open roads.

Ces deux dernières décennies, les systèmes embarqués ont été introduits dans de nombreux domaines d’application (transport, industrie, habitat, médical...). Ces systèmes se sont vu confier des tâches plus importantes pour délivrer de nouveaux services aux utilisateurs avec des délais de mise sur le marché toujours plus courts et à moindre coût. L’intégration rapide de ces systèmes au sein de produits manufacturés est un avantage concurrentiel pour les industriels. Cependant, les pannes associées à ces systèmes et le niveau de complexité croissant des équipements ont rendu les interventions de maintenance bien plus délicates. L’identification des causes de certaines pannes représente actuellement un véritable challenge dans les activités de la maintenance. Elles entrainent une indisponibilité excessive des équipements.Cette thèse propose une architecture générique de surveillance “active” pour l’aide à la maintenance de systèmes mobiles. Cette architecture repose sur des entités de surveillance “intelligentes” capables d’évaluer l’état de santé des équipements surveillés. Notre contribution se situe à la rencontre de différentes communautés de Recherche et s’appuie notamment sur des concepts développés par lacommunauté PHM (Pronostics and Health Management).L’architecture proposée est mise en œuvre et appliquée a la surveillance d’un système réel de transport ferroviaire dans le cadre du projet SURFER (SURveillance active FERroviaire) conduit par Bombardier-Transport. / Over the last two decades, embedded systems have been introduced in several application areas (transportation, industry, housing, medical...). These systems have achieved more important tasks for delivering new services to users with ever shorter time-to-market deadlines at lower cost. The rapid integration of these systems within manufactured products is a competitive edge for companies. However, breakdowns related to these systems, along with the increasing level of equipment complexity, have made maintenance interventions much more difficult. Identifying root causes of some breakdowns currently represent a real challenge in the maintenance activities. They lead to an excessive downtime of equipment.This thesis proposes a versatile “active” monitoring architecture for the maintenance assistance of mobile systems. This architecture relies on “smart” monitoring entities that can assess the health state of monitored equipment. Our contribution gathers different Research communities and relies particularly on concepts developed by the PHM (Pronostics and Health Management) community.The proposed architecture is implemented and applied for monitoring a real railway transportation system within the SURFER project (SURveillance active FERroviaire) led by Bombardier-Transport.

Les systèmes informatiques envahissent notre vie quotidienne et sont devenus des éléments essentiels de chacun de nos instants de vie. La technologie de l'information est un secteur d'activités offrant des opportunités considérables pour l'innovation et cet aspect paraît sans limite. Cependant, des systèmes à logiciel intégré ont donné des résultats décevants. Selon les constats, ils étaient non fiables, parfois dangereux et ne fournissaient pas les résultats attendus. La faiblesse des pratiques de développement constitue la principale raison des échecs de ces systèmes. Ceci est dû à la complexité des logiciels modernes et au manque de connaissances adéquates et propres. Le développement logiciel fournit un cadre contribuant à simplifier la conception de systèmes complexes, afin d'en obtenir une meilleure compréhension et d'assurer une très grande qualité à un coût moindre. Dans les domaines de l'automatique, de la surveillance médicale, de l'avionique..., les systèmes embarqués hautement critiques sont candidats aux erreurs pouvant conduire à des conséquences graves en cas d'échecs. La thèse vise à résoudre ce problème, en fournissant un ensemble de techniques, d'outils et un cadre pour développer des systèmes hautement critiques, en utilisant des techniques formelles à partir de l'analyse des exigences jusqu'à la production automatique de code source, en considérant plusieurs niveaux intermédiaires. Elle est structurée en deux parties: d'une part des techniques et des outils et d'autre part des études de cas. La partie concernant des techniques et des outils présente une structure intégrant un animateur de modèles en temps-réel, un cadre de correction de modèles et le concept de charte de raffinement, un cadre de modélisation en vue de la certification, un modèle du coeur pour la modélisation en boucle fermée et des outils de générations automatiques de code. Ces cadres et outils sont utilisés pour développer les systèmes critiques à partir de l'analyse des exigences jusqu'à la production du code, en vérifiant et en validant les étapes intermédiaires en vue de fournir un modèle formel correct satisfaisant les propriétés souhaitées attendues au niveau le plus concret. L'introduction de nouveaux outils concourt à améliorer la vérification des propriétés souhaitées qui ne sont pas apparentes aux étapes initiales du développement du système. Nous évaluons les propositions faites au travers de cas d'études du domaine médical et du domaine des transports. De plus, le travail de cette thèse a étudié la représentation formelle des protocoles médicaux, afin d'améliorer les protocoles existants. Nous avons complètement formalisé un protocole réel d'interprétation des ECG, en vue d'analyser si la formalisation était conforme à certaines propriétés relevant du protocole. Le processus de vérification formelle a mis en évidence des anomalies dans les protocoles existants. Nous avons aussi découvert une structure hiérarchique pour une interprétation efficace permettant de découvrir un ensemble de conditions qui peuvent être utiles pour diagnostiquer des maladies particulières à un stade précoce. L'objectif principal du formalisme développé est de tester la correction et la consistance du protocole médical / Software systems are pervasive in all walks of our life and have become an essential part of our daily life. Information technology is one major area, which provides powerful and adaptable opportunities for innovation, and it seems boundless. However, systems developed using computer-based logic have produced disappointing results. According to stakeholders, they are unreliable, at times dangerous, and fail to provide the desired outcomes. Most significant reasons of system failures are the poor development practices for system development. This is due to the complex nature of modern software and lack of adequate and proper understanding. Software development provides a framework for simplifying the complex system to get a better understanding and to develop the higher fidelity quality systems at lower cost. Highly embedded critical systems, in areas such as automation, medical surveillance, avionics, etc., are susceptible to errors, which can lead to grave consequences in case of failures. This thesis intends to contribute to further the use of formal techniques for the development computing systems with high integrity. Specifically, it addresses that formal methods are not well integrated into established critical systems development processes by defining a new development life-cycle, and a set of associated techniques and tools to develop highly critical systems using formal techniques from requirements analysis to automatic source code generation using several intermediate layers with rigorous safety assessment approach. The approach has been realised using the Event-B formalism. This thesis has mainly two parts: techniques and tools and case studies. The techniques and tools section consists of development life-cycle methodology, a framework for real-time animator, refinement chart, a set of automatic code generation tools and formal logic based heart model for close loop modeling. New development methodology, and a set of associated techniques and tools are used for developing the critical systems from requirements analysis to code implementation, where verification and validation tasks are used as intermediate layers for providing a correct formal model with desired system behavior at the concrete level. Introducing new tools help to verify desired properties, which are hidden at the early stage of the system development. We also critically evaluate the proposed development methodology and developed techniques and tools through case studies in the medical and automotive domains. In addition, the thesis work tries to address the formal representation of medical protocols, which is useful for improving the existing medical protocols. We have fully formalised a real-world medical protocol (ECG interpretation) to analyse whether the formalisation complies with certain medically relevant protocol properties. The formal verification process has discovered a number of anomalies in the existing protocols. We have also discovered a hierarchical structure for the ECG interpretation efficiently that helps to find a set of conditions that can be very helpful to diagnose particular disease at the early stage. The main objective of the developed formalism is to test correctness and consistency of the medical protocol

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés / The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control

Les attaques par canaux auxiliaires telles que l'analyse différentielle de la consommation de courant (DPA) et l'analyse différentielle des émissions électromagnétiques (DEMA) constituent une menace sérieuse pour la sécurité des systèmes embarqués. L'objet de cette thèse est d'étudier les vulnérabilités des implantations logicielles des algorithmes cryptographiques face à ces attaques pour concevoir un processeur d'un nouveau type. Pour cela, nous commençons par identifier les différents éléments des processeurs embarqués qui peuvent être exploités pour obtenir des informations secrètes. Puis, nous introduisons des stratégies qui privilégient un équilibre entre performance et sécurité pour protéger de telles architectures au niveau transfert de registres (RTL). Nous présentons également la conception et l'implantation d'un processeur sécurisé, le SecretBlaze-SCR. Enfin, nous évaluons l'efficacité des solutions proposées contre les analyses électromagnétiques globales et locales à partir de résultats expérimentaux issus d'un prototype du SecretBlaze-SCR réalisé sur FPGA. A travers cette étude de cas, nous montrons qu'une combinaison appropriée de contre-mesures permet d'accroître significativement la résistance aux analyses par canaux auxiliaires des processeurs tout en préservant des performances satisfaisantes pour les systèmes embarqués. / Side-channel attacks such as differential power analysis (DPA) and differential electromagnetic analysis (DEMA) pose a serious threat to the security of embedded systems. The aim of this thesis is to study the side-channel vulnerabilities of software cryptographic implementations in order to create a new class of processor. For that purpose, we start by identifying the different elements of embedded processors that can be exploited to reveal the secret information. Then, we introduce several strategies that seek a balance between performance and security to protect such architectures at the register transfer level (RTL). We also present the design and implementation details of a secure processor, the SecretBlaze-SCR. Finally, we evaluate the effectiveness of the proposed solutions against global and local electromagnetic analyses from experimental results obtained with a FPGA-based SecretBlaze-SCR. Through this case study, we show that a suitable combination of countermeasures significantly increases the side-channel resistance of processors while maintaining satisfactory performance for embedded systems.

Cette thèse porte sur l’utilisation de techniques d’accélération matérielle pour la conception de processeurs basés sur l’optimisation dynamique de binaires. Dans ce type de machine, les instructions du programme exécuté par le processeur sont traduites et optimisées à la volée par un outil de compilation dynamique intégré au processeur. Ce procédé permet de mieux exploiter les ressources du processeur cible, mais est délicate à exploiter car le temps de cette recompilation impacte de manière très significative l’effet global de ces optimisations. Dans cette thèse, nous montrons que l’utilisation d’accélérateurs matériels pour certaines étapes clés de cette compilation (construction de la représentation intermédiaire, ordonnancement des instructions), permet de ramener le temps de compilation à des valeurs très faible (en moyenne 6 cycles par instruction, contre plusieurs centaines dans le cas d’une mise en œuvre classique). Nous avons également montré comment ces techniques peuvent être exploitées pour offrir de meilleurs compromis performance/consommation sur certains types de noyaux de calculs. La thèse à également débouché sur la mise à disposition de la communauté de recherche du compilateur développé. / This thesis is focused on the hardware acceleration of processors based on Dynamic Binary Translation. Such architectures execute binaries by translating and optimizing each instruction at run-time, thanks to a DBT toolchain embedded in the system. This process leads to a better ressource utilization but also induces execution time overheads, which affect the overall performances. During this thesis, we've shown that the use of hardware components to accelerate critical parts of the DBT process (First translation, generation of an intermediate representation and instruction scheduling) drastically reduce the compilation time (around 6 cycles to schedule one instruction, against several hundreds for a fully-software DBT). We've also demonstrated that the proposed approach enables several continuous optimizations flow, which offers better energy/performance trade-offs. Finally, the DBT toolchain is open-source and available online.

Les travaux présentés dans ce mémoire proposent une méthode originale de génération automatique de tests à partir de modèles SysML pour la validation de systèmes embarqués. Un sous-ensemble du langage SysML (appelé SysML4MBT) regroupant les éléments de modélisation pris en compte dans notre approche a été défini et une stratégie de génération de tests dédiée (intitulée ComCover) a été créée. Cette stratégie, basée sur les principes du critère de couverture de modèles bien connu Def-Use, s'intéresse à la couverture des communications (envois / réceptions) au sein du système et entre le système et son environnement.La mise en œuvre opérationnelle d'un prototype, basé sur un générateur de tests à partir de modèle UML, a nécessité la définition de règles de réécriture permettant la transformation du modèle SysML4MBT vers le format d'entrée natif du générateur de tests tout en conservant l'expressivité de SysML4MBT. Finalement, les étapes de concrétisation des tests en scripts exécutables et l'établissement automatique du verdict lors de l'exécution sur banc de test définis durant le projet VETESS permettent l'établissement d'une chaîne outillée opérationnelle de génération et d'exécution automatique de tests à partir de spécifications SysML. Cette chaîne outillée a été étrennée sur plusieurs cas d'étude automobile tels que l'éclairage avant, les essuie-glaces ou la colonne de direction de véhicule. Sur ce dernier exemple, nous avons eu l'opportunité d'exécuter les tests sur un banc de test physique. Ces cas d'étude ont permis de valider chacune des étapes de l'approche proposée. / The work introduced in this thesis is in line with an original SysML Model-Based Testing approach to validate automotive mechatronic systems. A subset of SysML notation (called SysML4MBT) supported to express the test model is defined and a dedicated test generation strategy (called ComCover) is created. This strategy, based on the well-known Def-Use criteria, deals with the coverage of communications (sends / receives) inside the system and between the system and its environment.The development of an operational prototype, based on a UML-based test generator, has required the definition of rewriting rules to derive the input model of the UML test generator from the SysML4MBT model, by preserving the SysML4MBT expressivity.Finally, the concretization of tests in executable scripts and the assignment of a verdict by executing tests on test bench defined during the VETESS project, complete the operational toolchain that allows tests generation and execution from SysML models.This toolchain has been tried out on several automotive case studies as front lightings, wiper or steering column. Concerning this last experimentation, we have had the opportunity to execute test on a physical test bench. These case studies allow validating each step of the proposed approach.

La validation des systèmes est un des aspects critiques dans les phases de développement. Cette validation est d'autant plus importante pour les systèmes embarqués, dont le fonctionnement doit être autonome, mais aussi contraint par des limitations physiques et techniques. Avec la complexification des systèmes embarqués ces dernières années, l'applications de méthodes de validation durant le développement devient trop couteux, et la mise en place de mécanismes de vérification post-conception est nécessaire. L'utilisation de traces d'exécution, permettant de capturer le comportement du système lors de son exécution, se révèle efficace pour la compréhension et la validation des systèmes observés. Cependant, les outils d'exploitation de traces actuels se confrontent à deux défis majeurs, à savoir, la gestion de traces pouvant atteindre des tailles considérables, et l'extraction de mesures pertinentes à partir des informations bas-niveau contenues dans ces traces. Dans cette thèse, faite dans le cadre du projet FUI SoC-TRACE, nous présentons trois contributions. La première concerne la définition d'un format générique pour la représentation des traces d'exécution, enrichi en sémantique. La seconde concerne une infrastructure d'analyse utilisant des mécanismes de workflow permettant l'analyse générique et automatique de traces d'exécution. Cette infrastructure répond au problème de gestion des traces de tailles considérables textit{via} des mécanismes de streaming, permet la création d'analyses modulaires et configurables, ainsi qu'un enchainement automatique des traitements. Notre troisième contribution propose une méthode générique pour l'analyse de performances de systèmes Linux. Cette contribution propose à la fois la méthode et les outils de collecte de traces, mais aussi le workflow permettant d'obtenir des profils unifiés pour les traces capturées. La validation de nos propositions ont été faites d'une part sur des traces issues de cas d'usages proposés par STMicroelectronics, partenaire du projet, et d'autre part sur des traces issues de programmes de benchmarks. L'utilisation d'un format enrichi en sémantique a permis de mettre en évidence des anomalies d'exécutions, et ce de manière semi-automatique. L'utilisation de mécanismes de streaming au sein de notre infrastructure nous a permis de traiter des traces de plusieurs centaines de gigaoctets. Enfin, notre méthode d'analyse générique nous a permis de mettre en évidence, de manière automatique et sans connaissances a priori des programmes, le fonctionnement interne de ces différents benchmarks. La généricité de nos solutions a permis d'observer le comportement de programmes similaires sur des plates-formes et des architectures différentes, et d'en montrer leur impact sur les exécutions. / Validation process is a critical aspect of systems development. This process is a major concern for embedded systems, to assess their autonomous behavior, led by technical and physical constraints. The growth of embedded systems complexity during last years prevents the use of complex and costly development processes such as formal methods. Thus, post-conception validations must be applied. Execution traces are effective for validation and understanding as they allow the capture of systems behavior during their executions. However, trace analysis tools face two major challenges. First, the management of huge execution traces. Second, the ability to retrieve relevant metrics, from the low-level information the trace contains. This thesis was done as part of the SoC-TRACE projet, and presents three contributions. Our first contribution is a definition of a generic execution trace format that expresses semantics. Our second contribution is a workflow-based infrastructure for generic and automatic trace analysis. This infrastructure addresses the problem of huge traces management using streaming mechanisms. It allows modular and configurable analyses, as well as automatic analyses execution. Our third contribution is about the definition of a generic performance analyses for Linux systems. This contribution provides methods and tools for trace recording, and also analysis workflow to obtain unified performance profiles. We validate our contributions on traces from use cases given by STMicroelectronics, partner of the project, and also on traces recorded from benchmarks executions. Our trace format with semantics allowed us to automatically bring out execution problems. Using streaming mechanisms, we have been able to analyze traces that can reach several hundreds of gigabytes. Our generic analysis method for systems let us to automatically highlight, without any prior knowledge, internal behavior of benchmark programs. Our generic solutions point out a similar execution behavior of benchmarks on different machines and architectures, and showed their impact on the execution.

Les systèmes embarqués, y compris les dispositifs, l’intergiciel et le logiciel pour la création de sous-systèmes intelligents capables de gérer le contrôle d’appareils électroniques, font de plus en plus partie de nos vies quotidiennes : ils sont intégrés dans des infrastructures de base, (par exemple dans la gestion des routes et des chemins de fer) et sont désormais utilisés en tant que technologies-clés par des millions d'applications logicielles chaque jour. En outre, l'évolution rapide et continue des systèmes embarqués modernes a provoqué de nouveaux défis. Par exemple, la conception des processus complexes qui causent des retards dans le temps de commercialisation et la conséquente augmentation des coûts globaux. Ces systèmes sont plus enclins aux erreurs et par conséquence il devient prioritaire de fournir aux concepteurs des outils effectifs et efficaces pour les aider à surmonter les difficultés liées à la conception des systèmes globales, pour la vérification et pour la validation. Cette thèse est la définition et le développement d'une méthodologie de modélisation basée sur le profil de MARTE et sur le profil de SysML dans un contexte avionique, et orientée à la réutilisation des composantes logicielles et à leur vérification. Cette thèse vise à discuter et illustrer aussi l'efficacité d’une stratégie basée sur la combinaison d’UML, MARTE (Modeling and Analysis of Real Type and Embedded Systems) et des langages SysML sur des étapes différentes de la modélisation d'un système embarqué / Embedded Systems, including devices, middleware and software for the creation of intelligent sub-systems able of monitoring and controlling appliances, are more and more part of our world everyday lives; they are included in the basic infrastructure of society such as roads and railways and are key technologies used by millions of people every day. Moreover the continuous rapid evolution of modern embedded systems has given rise to new challenges: such as increasingly complex design processes that cause delays in time to market and cause escalation of overall design costs. Additionally, these systems are more prone to containing errors, and it becomes more relevant to provide designers with effective tools to aid them in overcoming the difficulties related to the overall system design, verification and validation. This thesis contributes to the definition and to the development of a model based methodology grounded on the OMG’s MARTE profile (Modeling and Analysis of Real Type and Embedded Systems) and on SysML profile to model requirements targeting an avionic case study, with a particular attention to the reuse of the modelled components and to the benefits of their verification. This thesis aims at discussing and illustrating the effectiveness of using a combination of UML, MARTE and SysML languages at the different steps of the embedded system modelling efforts and to provide within this thesis a set of methodological guidelines/steps and an approach to create design model, stores and verify them