Dans de nombreux domaines tels que l'avionique, la médecine ou la domotique, les applications logicielles jouent un rôle de plus en plus important, allant jusqu'à être critique pour leur environnement. Afin de pouvoir faire confiance à ces applications, leur développement est contraint par des exigences de sûreté de fonctionnement. En effet il est nécessaire de démontrer que ces exigences de haut-niveau sont prises en compte tout au long du cycle de développement et que des solutions concrètessont mises en œuvre pour parvenir à les respecter. De telles contraintes rendent le développement d'applications sûres de fonctionnement particulièrement complexe et difficile. Faciliter ce processus appelle à la recherche de nouvelles approches dedéveloppement qui intègrent des concepts de sûreté de fonctionnement et guident les développeurs lors de chacune des étapesnécessaires à la production d'une nouvelle application digne de confiance.Cette thèse propose ainsi de s'appuyer sur une approche dirigée par la conception pour guider le développement des applications sûres de fonctionnement. Cette approche est concrétisée à travers une suite d'outils nommée DiaSuite et offre du support dédié à chaque étape du développement. En particulier, un langage de conception permet de décrire à la fois les aspects fonctionnels et non-fonctionnels des applications en se basant sur un paradigme dédié et en intégrant des concepts de sûreté de fonctionnement tels que le traitement des erreurs. A partir de la description d'une application, du support est généré pour guider les phases d'implémentation et de vérification. En effet, la génération d'un framework de programmation dédié permet de guider l'implémentation tandis que la génération d'un modèle formel permet de guider la vérification statique de l'application et qu'un support de simulation permet de faciliter les tests. Cette approche est évaluée grâce à des cas d'études réalisés dans les domaines de l'avionique et de l'informatique ubiquitaire.

Ce mémoire, a pour objet de présenter une synthèse de mes travaux de recherche et de les mettre en perspective avec l'objectif général de la conception et du développement d'un environnement logiciel pour la modélisation et la simulation. Ils sont présentés selon trois axes thématiques : - bien modéliser pour mieux simuler, - calculer efficacement, précisément et juste, - générer un code de calcul dédié. Un dernier chapitre, plus technique, présente les contours et les fonctionnalités de cet environnement logiciel intégré pour la modélisation et la simulation, dont la conception a été le cadre général et le fil conducteur de l'essentiel de mes travaux.

Dans de nombreux domaines tels que l'avionique, la médecine ou la domotique, les applications logicielles jouent un rôle de plus en plus important, allant jusqu'à être critique pour leur environnement. Afin de pouvoir faire confiance à ces applications, leur développement est contraint par des exigences de sûreté de fonctionnement. En effet il est nécessaire de démontrer que ces exigences de haut-niveau sont prises en compte tout au long du cycle de développement et que des solutions concrètes sont mises en oeuvre pour parvenir à les respecter. De telles contraintes rendent le développement d'applications sûres de fonctionnement particulièrement complexe et difficile. Faciliter ce processus appelle à la recherche de nouvelles approches de développement qui intègrent des concepts de sûreté de fonctionnement et guident les développeurs lors de chacune des étapes nécessaires à la production d'une nouvelle application digne de confiance. Cette thèse propose ainsi de s'appuyer sur une approche dirigée par la conception pour guider le développement des applications sûres de fonctionnement. Cette approche est concrétisée à travers une suite d'outils nommée DiaSuite et offre du support dédié à chaque étape du développement. En particulier, un langage de conception permet de décrire à la fois les aspects fonctionnels et non-fonctionnels des applications en se basant sur un paradigme dédié et en intégrant des concepts de sûreté de fonctionnement tels que le traitement des erreurs. A partir de la description d'une application, du support est généré pour guider les phases d'implémentation et de vérification. En effet, la génération d'un framework de programmation dédié permet de guider l'implémentation tandis que la génération d'un modèle formel permet de guider la vérification statique de l'application et qu'un support de simulation permet de faciliter les tests. Cette approche est évaluée grâce à des cas d'études réalisés dans les domaines de l'avionique et de l'informatique ubiquitaire.

La compilation est une étape indispensable dans la création d'applications performantes.Cette étape autorise l'utilisation de langages de haut niveau et indépendants de la cible tout en permettant d'obtenir de bonnes performances.Cependant, de nombreux freins empêchent les compilateurs d'optimiser au mieux les applications.Pour les compilateurs statiques, le frein majeur est la faible connaissance du contexte d'exécution, notamment sur l'architecture et les données utilisées.Cette connaissance du contexte se fait progressivement pendant le cycle de vie de l'application.Pour tenter d'utiliser au mieux les connaissances du contexte d'exécution, les compilateurs ont progressivement intégré des techniques de génération de code dynamique.Cependant ces techniques ne se focalisent que sur l'utilisation optimale du matériel et n'utilisent que très peu les données.Dans cette thèse, nous nous intéressons à l'utilisation des données dans le processus d'optimisation d'applications pour GPU Nvidia.Nous proposons une méthode utilisant différents moments pour créer des bibliothèques adaptatives capables de prendre en compte la taille des données.Ces bibliothèques peuvent alors fournir les noyaux de calcul les plus adapté au contexte.Sur l'algorithme de la GEMM, la méthode permet d'obtenir des gains pouvant atteindre 100~\% tout en évitant une explosion de la taille du code.La thèse s'intéresse également aux gains et coûts de la génération de code lors de l'exécution, et ce du point de vue de la vitesse d'exécution, de l'empreinte mémoire et de la consommation énergétique.Nous proposons et étudions 2 approches de génération de code à l'exécution permettant la spécialisation de code avec un faible surcoût.Nous montrons que ces 2 approches permettent d'obtenir des gains en vitesse et en consommation comparables, voire supérieurs, à LLVM mais avec un coût moindre. / Compilation is an essential step to create efficient applications.This step allows the use of high-level and target independent languages while maintaining good performances.However, many obstacle prevent compilers to fully optimize applications.For static compilers, the major obstacle is the poor knowledge of the execution context, particularly knowledge on the architecture and data.This knowledge is progressively known during the application life cycle.Compilers progressively integrated dynamic code generation techniques to be able to use this knowledge.However, those techniques usually focuses on improvement of hardware capabilities usage but don't take data into account.In this thesis, we investigate data usage in applications optimization process on Nvidia GPU.We present a method that uses different moments in the application life cycle to create adaptive libraries able to take into account data size.Those libraries can therefore provide more adapted kernels.With the GEMM algorithm, the method is able to provide gains up to 100~\% while avoiding code size explosion.The thesis also investigate runtime code generation gains and costs from the execution speed, memory footprint and energy consumption point of view.We present and study 2 light-weight runtime code generation approaches that can specialize code.We show that those 2 approaches can obtain comparable, and even superior, gains compared to LLVM but at a lower cost.

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

Architectures hétérogènes sont largement utilisées dans le domaine de calcul haute performance. Cependant, le développement d'applications sur des architectures hétérogènes est indéniablement fastidieuse et sujette à erreur pour un programmeur même expérimenté. Pour passer une application aux architectures multi-cœurs hétérogènes, les développeurs doivent décomposer les données de l'entrée, gérer les échanges de valeur intermédiaire au moment d’exécution et garantir l'équilibre de charge de système. L'objectif de cette thèse est de proposer une solution de programmation parallèle pour les programmeurs novices, qui permet de faciliter le processus de codage et garantir la qualité de code. Nous avons comparé et analysé les défauts de solutions existantes, puis nous proposons un nouvel outil de programmation STEPOCL avec un nouveau langage de domaine spécifique qui est conçu pour simplifier la programmation sur les architectures hétérogènes. Nous avons évalué la performance de STEPOCL sur trois cas d'application classiques : un stencil 2D, une multiplication de matrices et un problème à N corps. Le résultat montre que : (i) avec l'aide de STEPOCL, la performance d'application varie linéairement selon le nombre d'accélérateurs, (ii) la performance de code généré par STEPOCL est comparable à celle de la version manuscrite. (iii) les charges de travail, qui sont trop grandes pour la mémoire d'un seul accélérateur, peuvent être exécutées en utilisant plusieurs accélérateurs. (iv) grâce à STEPOCL, le nombre de lignes de code manuscrite est considérablement réduit. / Heterogeneous architectures have been widely used in the domain of high performance computing. However developing applications on heterogeneous architectures is time consuming and error-prone because going from a single accelerator to multiple ones indeed requires to deal with potentially non-uniform domain decomposition, inter-accelerator data movements, and dynamic load balancing. The aim of this thesis is to propose a solution of parallel programming for novice developers, to ease the complex coding process and guarantee the quality of code. We lighted and analysed the shortcomings of existing solutions and proposed a new programming tool called STEPOCL along with a new domain specific language designed to simplify the development of an application for heterogeneous architectures. We evaluated both the performance and the usefulness of STEPOCL. The result show that: (i) the performance of an application written with STEPOCL scales linearly with the number of accelerators, (ii) the performance of an application written using STEPOCL competes with an handwritten version, (iii) larger workloads run on multiple devices that do not fit in the memory of a single device, (iv) thanks to STEPOCL, the number of lines of code required to write an application for multiple accelerators is roughly divided by ten.

Cette thèse s'inscrit dans le cadre de la mise en œuvre de l'ingénierie dirigée par les modèles (IDM) pour le développement des systèmes embarquées. Ces systèmes ayant généralement des ressources limitées (mémoire et/ou calculs), exigent que le code généré soit le plus optimisé possible. L'objectif de cette thèse est de produire à partir d'un modèle spécifié dans le langage UML, un code assembleur plus compact que le code assembleur produit par les compilateurs de code. Malgré l'évolution croissante des compilateurs optimisés, les compilateurs les plus répandus comme le GCC (Gnu Compiler Collection) sont incapables d'effectuer certains types d'optimisations qu'il est possible d'effectuer à un plus haut niveau d'abstraction dans une phase de pré-génération de code. En effet, certaines informations (liées à la sémantique d'exécution du langage UML) sont perdues lors de la génération de code. Ces informations, utiles pour les optimisations de haut niveau, sont invisibles par le compilateur de code vue qu'il prend toutes les informations liées au système modélisé à partir du code généré. Nous proposons ainsi une nouvelle approche dirigée par les modèles pour le développement des systèmes à ressources limitées, qui élimine l'étape de la génération de code en remplaçant cette étape par une compilation directe des modèles. Nous avons développé le premier compilateur de modèles UML (GUML : le front-end UML pour le compilateur GCC) qui génère directement de l'assembleur (sans passer par un langage de programmation) à partir des modèles UML. GUML permet de compiler les classes, les activités et les machines à états UML. Il permet de générer, en compilant certaines machines à états, un code assembleur plus compact que le code assembleur produit par GCC. Deux optimisations de GCC sont améliorées : l'élimination de code mort et l'élimination des expressions redondantes.

La complexité des systèmes sur puce s'accentue pour supporter les nouvelles applications dans le domaine des télécommunications et du multimédia. La tendance actuelle des nouvelles architectures matérielles converge vers des plateformes multi-cœurs à plusieurs unités de calcul (processeurs, DSP, IP) interconnectées par un réseau sur puce qui peut être configurable au niveau de ses interfaces réseau. Pour ce genre d'architectures, les environnements de génération de code classiques ne sont plus adaptés. Cette thèse propose un flot de génération de code de configuration pour le déploiement des applications de type flots de données sur les architectures à base d'IPs interconnectés à travers un réseau sur puce configurable. Le flot commence par un modèle de haut niveau de l'application et de l'architecture et propose une méthodologie de partitionnement des ressources. Le processus de génération de code passe par plusieurs étapes modélisées par diverses représentations intermédiaires du système. Le flot a été développé par la suite dans un environnement basé sur le standard IEEE 1685 (IP-XACT). Le flot proposé a été appliqué pour la génération et la validation du code de configuration en vue de déployer une application 3GPP-LTE de télécommunication sur la plateforme Magali. Le flot a ensuite été généralisé pour supporter, en plus de la génération du code de configuration, la génération du code logiciel exécutable par les processeurs.

Cette thèse, à caractère industriel, vise à répondre à une problématique de production de l’entreprise ITK. Par la mise en oeuvre des techniques de l’ingénierie dirigée par les modèles, nous proposons un environnement de modélisation et de simulation pour la croissance des plantes. Outre sa facilité d’utilisation pour les agronomes, le prototype obtenu permet la génération automatique de code Java des modèles à intégrer dans des outils d’aide à la décision exécutés sur une plateforme Java Enterprise Edition. / This PhD thesis has an industrial purpose. It is motivated by a software production issue met within the ITK company. Using the techniques provided by model-driven engineering, we propose a modeling and simulation environment dedicated to plant growth. The prototype achieved proves to be easy to use for crop modelers. It is also enhanced with a Java code generation feature. The models obtained from this code generation are designed to be integrated into decision support systems running on a Java Entreprise Edition platform.

En aéronautique civile, les systèmes électriques qui composent l'avion sont de plus en plus nombreux, de par l'accroissement des fonctionnalités, des besoins des usagers (confort), mais aussi par le besoin d'améliorer les performances des actionneurs électromécaniques et hydrauliques, voire de les remplacer par du tout électrique. Ainsi, les systèmes d'électroniques de puissance sont les premiers dispositifs électriques que voient les actionneurs. Ces dispositifs sont interfacés avec les interfaces de pilotage par des systèmes de contrôles-commandes.<br />Les normes aéronautiques imposent que tous les dispositifs utilisés dans un avion répondent à des contraintes sévères quant à leur fiabilité et leur sécurité de fonctionnement. Dans le cas précis des convertisseurs statiques qui pilotent les actionneurs, on est confronté aux normes de fonctionnement des réseaux électriques, aux normes C.E.M., aux normes environnementales (au sens du contexte du dispositif), et aux normes liés aux systèmes de contrôle.<br />Le marché de l'aéronautique, bien que très spécifique, est très concurrentiel au niveau mondial. Les multiples objectifs de matériels très performants, très fiables, très sûrs, mais les moins chers possibles sont donc de véritables problématiques.<br />Dans le cadre des convertisseurs statiques, un moyen pour réduire les coûts est l'utilisation de DSP (Digital Signal Processors) pour maximiser l'intégration de la commande et pour réduire les coûts, mais ce composant n'est pas conçu pour le milieu aéronautique.<br />L'ensemble de cette étude porte sur la conception d'un nouveau type de radar marqué par plusieurs ruptures technologiques. Le prototype réalisé comporte un convertisseur statique piloté par un DSP, mais ayant des fonctionnalités qui vont largement au-delà du convertisseur basique d'électronique de puissance. L'aspect « système » est largement pris en compte. Le convertisseur mis en oeuvre est un dispositif autonome de pilotage de moteurs.