Cette thèse propose une approche pour intégrer l'utilisation des propriétés temporisées stochastiques dans un processus continu de design fondé sur des modèles à l'exécution. La spécification temporelle de services est un aspect important des architectures à base de composants, par exemple dans des réseaux distribués volatiles de nœuds informatiques. L'approche models@runtime facilite la gestion de ces architectures en maintenant des modèles abstraits des archi- tectures synchronisés avec la structure physique de la plate-forme d'exécution distribuée. Pour les systèmes auto-adaptatifs, la prédiction de délais et de débit d'un assemblage de composants est primordial pour prendre la décision d'adaptation et accepter les évolutions qui sont conformes aux spécifications temporelles. Dans ce but, nous définissons une extension du métamodèle fondée sur les réseaux de Petri stochastiques comme un modèle temporisé interne pour la prédiction. Nous concevons une bibliothèque de patrons pour faciliter la spécification et la prédiction des propriétés temporisées classiques de modèles à l'exécution et rendre la synchronisation des comportements et des changements structurels plus facile. D'autre part, nous appliquons l'approche de la modélisation par aspects pour tisser les modèles temporisés internes dans les modèles temporisés de comportement du composant et du système. Notre moteur de prédiction est suffisament rapide pour effectuer la prédiction à l'exécution dans un cadre réaliste et valider des modèles à l'exécution.

Aujourd'hui, les environnements ubiquitaires font partie de notre vie quotidienne. À la maison, au travail, dans les voitures, dans les hôtels, les supermarchés et autres espaces publiques, nous rencontrons des technologies qui visent à rendre notre vie plus simple et plus facile d'une façon transparente. Durant ces dernières années, le potentiel de ces environnements a été de plus en plus exploité, notamment avec l'avènement et l'utilisation généralisée des smartphones. Ce type de dispositifs permet l'exécution d'applications qui ont la capacité de s'adapter parfaitement à l'état courant de l'environnement. De telles applications, appelées "applications sensibles au contexte", bénéficient de l'information du contexte et des services qui sont présents dans leur environnement pour améliorer et changer automatiquement leur comportement. Toutefois, ces adaptations nécessitent une intégration d'informations qui doit être effectuée en tenant compte de l'hétérogénéité en termes de dispositifs, de plateformes d'exécution, et de protocoles de communication ainsi que la mobilité des applications de sorte que les différentes responsabilités de l'adaptation peuvent être distribuées. Pour faire face à ces défis, et compte tenu des limitations des solutions existantes, nous fournissons deux contributions majeures dans cette dissertation. Tout d'abord nous introduisons l'intergiciel SPACES comme une solution d'intégration des informations contextuelles et ensuite nous définissons le paradigme de "boucles de contrôle ubiquitaires" pour adapter les applications sensibles au contexte. En particulier, dans SPACES, nous définissons un méta-modèle inspiré du style architectural REST (REpresentational State Transfer) pour favoriser l'échange des informations contextuelles en tant que ressources, ce qui représente le fondement de notre approche. Ensuite, nous définissons les connecteurs SPACES pour modulariser les différents concepts et préoccupations identifiés par le méta-modèle. Ces connecteurs sont conçus en utilisant les principes de la programmation orientée composant et ils sont incorporés dans le modèle Service Component Architecture (SCA) pour être utilisés dans différents types d'applications, et ainsi indépendamment des applications sensibles au contexte. Grâce à la définition de SPACES, nous sommes en mesure d'élaborer la seconde contribution de la dissertation--i.e., les boucles de contrôle ubiquitaires. Inspiré par les concepts de l'informatique autonome, les boucles de contrôle offre la flexibilité nécessaire pour intégrer de nouveaux participants dans le processus d'adaptation (par exemple, des applications sensibles au contexte, des services et des systèmes existants) tout en fournissant un support pour la mobilité et l'intégration de nouveaux mécanismes de communication en cas de besoin. Dans le noyau des boucles de contrôle ubiquitaires--i.e., la prise de décision-- nous employons des techniques de programmation par contraintes pour optimiser la configuration courante de l'application en intégrant des critères qui garantissent une meilleure expérience à l'utilisateur final, tels que les coûts associés à l'adaptation, les ressources consommées ou encore la qualité de service offerte par la nouvelle configuration. Enfin, nous validons notre proposition avec trois études de cas: Tout d'abord une politique de Caching or Off-Loading, dans laquelle le comportement de l'application est modifiée lors de l'exécution, ensuite TRACK.ME, une plateforme pour effectuer des expérimentations scientifiques et enfin DIGIHOME, une plateforme pour la création des maisons intelligentes. Ces scénarios démontrent la pertinence de notre approche lorsque différents types de dispositifs, des protocoles et des technologies de mise en œuvre sont impliqués dans le processus d'adaptation.

Les patrons de conception répertorient les bonnes pratiques de la programmation par ob- jets. Les solutions des patrons, appelées motifs, apparaissent avec une densité croissante dans les bibliothèques et cadriciels. Les effets de cette densité sur la modularité, l'adaptation et la réutilisation des programmes sont mal connus. Or la dispersion et le mélange du code lié à l'im- plémentation des motifs rendent difficile l'étude de ces effets. La programmation par aspects est une technique nouvelle dédiée au traitement de ces deux symptômes. En modularisant les motifs dans des aspects, nous pouvons analyser de manière plus fine les problèmes d'implémentation et de composition des motifs liés à leur densité. Cette thèse aborde les problèmes de la densité, de l'implémentation et de la composition des motifs avec AspectJ, une extension de Java pour les aspects. À partir du cas concret du cadri- ciel JHotDraw, nous montrons qu'une forte densité est un facteur de risque sur la modularité et l'adaptation d'un programme objet. Nous présentons la transformation des motifs à l'aide des aspects et nous décrivons les idiomes d'AspectJ supportant leur modularisation. Nous exami- nons la modularité et la réutilisation des compositions de motifs définies avec les aspects. Nous proposons la résolution des interactions entre motifs à l'aide du langage de coupe des aspects. Enfin nous développons une méthode de programmation avec AspectJ basée sur l'usage conjoint des classes et des aspects. Ces travaux nous permettent de conclure sur l'intérêt des aspects comme moyen d'étude et de traitement de la densité des motifs. Ils ouvrent également des pistes pour l'amélioration des langages d'aspects.

Les systèmes logiciels modernes se caractérisent par un besoin d'évolutions perpétuelles et rapides, comme par exemple dans le monde de l'informatique mobile. Pour faciliter le développe\-ment et l'évolution rapide de systèmes complexes, des approches de génie logiciel ont été proposées, telles que les architectures logicielles et la méthode de conception agile. Néanmoins, les solutions actuelles offrent peu de support pour permettre l'évolution fiable d'un système, c'est-à-dire permettre sa modification tout en garantissant le respect de ses exigences de qualités de service et de bon fonctionnement global. La contribution de cette thèse est CALICO, un canevas de développement agile pour la conception et l'évolution fiable de systèmes logiciels à composants et orientés services. Le développement agile repose sur l'utilisation d'un cycle de développement itératif et incrémental qui permet à l'architecte d'itérer entre les étapes de conception de l'architecture et de débogage du logiciel dans son environnement d'exécution. A chaque itération du cycle, l'architecte peut faire évoluer son logiciel et fiabiliser ses évolutions grâce à l'exécution d'analyses statiques et dynamiques complémentaires. Ainsi, lors de la conception et de l'évolution d'un système, l'architecte dispose d'un ensemble de métamodèles pour spécifier la structure de l'architecture de son logiciel et ses diverses exigences de qualité de services. Lors du déploiement, CALICO utilise les modèles spécifiés pour instancier le système sur la plate-forme d'exécution cible et les garde synchronisés avec le logiciel lors de son exécution. De cette façon, l'architecte dispose toujours d'une vue conceptuelle qui lui permet de raisonner sur les propriétés critiques de son logiciel lors d'une évolution. De plus, pour fiabiliser ces évolutions, CALICO offre un cadre fédérateur qui autorise la réutilisation de nombreux outils d'analyse statique des architectures logicielles et de débogage dynamique qui étaient jusqu'alors dispersés dans différentes plates-formes existantes. Ainsi, chaque évolution peut être analysée statiquement sur la vue conceptuelle avant d'être propagée au système logiciel. Les analyses dynamiques reposent quant à elles sur des valeurs disponibles à l'exécution. La capture de ces valeurs est effectuée grâce à une instrumentation automatique du système logiciel. CALICO permet donc de fiabiliser les évolutions même si les plates-formes d'exécution sous-jacentes ne le proposent pas nativement. Notre contribution se concrétise par une implémentation multi plates-formes. La version actuelle prend en charge quatre plates-formes à composants et une plate-forme à services. Par ailleurs, les tests de performances que nous avons réalisés démontrent que CALICO est utilisable pour la conception et l'évolution fiable de larges applications jusqu'à 10000 composants et services, ce qui correspond à la montée en charge maximale de la plupart des plates-formes d'exécution.

Les intergiciels et les applications réparties se caractérisent par un nombre élevé de fonctionnalités à intégrer pour aboutir à un logiciel fini. Par ailleurs ils s'appliquent à de nombreux contextes d'exécution, de l'embarqué fortement contraint aux systèmes d'information ouverts sur l'Internet. Cette diversité engendre des besoins multiples allant, pour n'en citer que quelques uns, de la tolérance aux fautes, aux communications distantes ou à l'ordonnancement sous contrainte. Ce mémoire porte sur l'ingénierie des intergiciels et des applications réparties. Notre objectif est de proposer des solutions pour l'intégration des différentes fonctionnalités de ces logiciels. Pour cela, les études décrites dans ce mémoire portent sur trois techniques principales : la réexivité, les aspects et les composants. Dans un premier axe, nous abordons la conception et la réalisation de service pour des applications réparties CORBA à l'aide de la réflexivité. Nous avons proposé un service d'observation d'exécution d'exécutions réparties. Nous montrons que la réflexivité permet de séparer clairement les différentes préoccupations. Les applications à observer et le service sont clairement découplés. L'intégration peut alors être faite de façon transparente. Nous montrons que le coût des mécanismes réflexifs est faible par rapport aux coûts globaux de communication dans un environnement distribué CORBA. Dans un deuxième axe, nous nous focalisons sur les techniques à base d'aspect. Nous présentons JAC (Java Aspect Components) qui est une plate-forme pour la programmation d'applications orientées aspect. JAC propose la notion de tissage dynamique qui permet d'adapter au cours de l'exécution une application en ajoutant ou en retirant des aspects. En terme d'intergiciel et de répartition, JAC apporte la notion de conteneur ouvert à objets et à aspects et la notion de coupe distribuée. Finalement, nous abordons les techniques à base de composant. L'objectif est de fournir un cadre uniant les styles de développement à base d'aspect et de composant. Une étude préliminaire compare le développement d'un service de partage de documents répliqués avec des frameworks à base de composants (Fractal et Kilim) et un framework AOP (JAC). Nous montrons les forces et les faiblesses de chacun des styles et en tirons des conclusions pour étendre le modèle de composants Fractal en lui adjoignant la notion d'aspect. Dans un second temps, nous montrons que les aspects peuvent également être bénéfiques à l'ingénierie du modèle de composant lui-même. Nous aboutissons ainsi à une solution dans laquelle les aspects contribuent à la fois à la mise en oeuvre des mécanismes internes du modèle et à son interface de programmation externe.

La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.

L'intelligence ambiante est un domaine hautement interdisciplinaire et implique de nombreux domaines de recherche. C'est pourquoi les avancées dans ce domaine sont conditionnées par l'interaction et l'intégration entre ces nombreuses disciplines. Ce manuscrit s'intéresse à la problématique de capitalisation des travaux existants, ainsi qu'à l'intégration dynamique de logiciels et d'appareils développés indépendamment les uns des autres. Nous proposons une intergiciel à services et une interface graphique utilisables et extensibles par les différents spécialistes. En étendant les approches à services et les principes du web sémantique, nous proposons une méthode de conception facilitant l'intégration dynamique et la composition de services. Cette méthode se base sur le concept nouveau d'usines à services : un service capable d'en instancier d'autres sur demande. Nous proposons aussi un langage de description pour ce langage.

Les Systèmes d'Information (SI) de même domaine d'activité gèrent de nombreux concepts similaires. Ces concepts peuvent être analysés et généralisés dans des abstractions informatiques qui seront réutilisées lors de nouveaux développements. De telles abstractions sont appelées Composants Métier (CM). Cependant, il est souvent difficile d'expliciter des critères clairs de réutilisation, en particulier la manière dont on peut identifier, spécifier, organiser et en grande partie automatiser la réutilisation de ces CM. Les contributions de cette thèse adressent cette problématique et s'articulent autour de trois principaux résultats. La première contribution concerne un modèle de CM de nature processus appelé « CMP ». Ce modèle est centré sur les propriétés fonctionnelles des composants. L'accent est mis sur la complétude et la variabilité de la solution exprimée sous la forme de quatre vues complémentaires intégrant des points de variation. Le travail réalisé sur les mécanismes de spécification de la variabilité a abouti à un profil UML pouvant être utilisé pour modéliser non seulement des processus réutilisables mais aussi des processus flexibles. Une deuxième contribution s'inscrit dans le cadre de la proposition d'un processus permettant la spécification d'un CMP selon le modèle proposé. Dans ce processus, nous définissons un ensemble de règles de construction, de traduction et de cohérence qui assurent la traçabilité des artefacts produits tout au long du cycle de développement. Une troisième contribution concerne la proposition de directives qui assistent l'ingénieur de SI lors de la réutilisation de CMP. L'accent est particulièrement mis sur la proposition d'un formalisme de documentation et de classification de CMP validé dans le cadre d'un environnement de stockage de composants. Nous proposons également un processus d'imitation intégré à la méthode de développement Symphony et permettant de tirer partie de la spécification d'un CMP lors de la conception d'un SI. L'ensemble des propositions est accompagné d'outils et d'expérimentations utilisateurs servant de supports de validation et de mise en œuvre des travaux réalisés.

Les applications ubiquitaires évoluent dans des environnements plus hétérogènes et plus dynamiques que ceux des systèmes distribués traditionnels. La criticité des domaines applicatifs impliqués et la vocation non intrusive de l'informatique ubiquitaire exigent de garantir la robustesse des applications avant et pendant leur déploiement en situation réelle. Les solutions proposant de gérer la dynamicité des environnements ubiquitaires offrent des canevas de programmation dont la généricité ne permet pas de garantir la fiabilité des applications développées. D'autres solutions permettent davantage de vérifications en assurant, par exemple, l'intégrité des communications. Cependant, ces vérifications, telles que proposées dans ces solutions, empêchent la prise en compte de la dynamicité, indispensable à la mise en oeuvre d'applications ubiquitaires. Dans cette thèse, nous proposons un canevas logiciel visant à concevoir, développer, vérifier et tester les applications ubiquitaires avant leur déploiement en environnements réels. Notre approche repose sur des spécifications haut niveau des applications cibles. Chaque spécification, écrites dans le langage DIASPEC, est analysée, vérifiée et compilée par le compilateur DIASPEC qui génère un canevas logiciel dédié, incluant un canevas de programmation et un canevas de simulation. Les canevas de programmation générés fournissent du support pour la programmation d'applications ubiquitaires. Ils garantissent l'intégrité des communications tout en permettant la gestion de la dynamicité des environnements ubiquitaires. Les canevas de simulation générés fournissent du support pour le test des applications ainsi développées. Les contributions de cette thèse sont les suivantes :<br />– Nous proposons l'approche DIAGEN qui permet, à partir de spécifications d'architectures logicielles ubiquitaires, de générer du support de programmation et un ensemble de vérifications dédiés au développement d'applications ubiquitaires. Ces spécifications reposent sur un langage déclaratif, appelé DIASPEC, qui permet de décrire les types de services composant les applications ubiquitaires cibles. Le compilateur DIASPEC vérifie la cohérence des spécifications et génère, à partir de celles-ci, des canevas de programmation dédiés. Les canevas de programmation générés garantissent l'intégrité des communications d'applications dynamiques.<br />– Nous avons développé DIASIM, un simulateur pour tester à l'exécution, le comportement des applications développées avec l'approche DIAGEN. DIASIM permet de tester les applications sans les modifier et d'intégrer incrémentalement des services réels dans les scénarios de simulation.<br />– Nous avons montré que l'approche DIAGEN permet davantage de vérifications statiques tout en gérant la dynamicité des environnements ubiquitaires et en permettant une plus grande concision des applications développées. Nous avons analysé les canevas de programmation générés pour la gestion de réunion, l'immotique et la téléphonie.

Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il présente, étudie et justifie les choix faits dans le système Coq.