L'informatique ubiquitaire envahit de plus en plus nos activités quotidiennes. Cela a pour effet que nous sommes de plus en plus demandeurs de services réagissant dynamiquement au contexte dans lequel nous évoluons. Ces services doivent alors s'adapter à l'environnement dans lequel ils sont utilisés, si possible de façon automatique. Ces dernières années, d'importantes avancées dans le développement de systèmes auto-adaptables ont été faites et ont pu être intégrées dans les logiciels. Néanmoins, il est nécessaire d'étudier des modèles formels et les outils associés pour définir au mieux l'auto-adaptation en vue de garantir la fiabilité, l'extensibilité et la réutilisabilité de ces systèmes, ceci dans un objectif de proposer des artefacts communs et bien définis pour les processus de conception de des applications auto-adaptables. La plupart des approches existantes se concentrent sur l'un des artefacts de ces systèmes auto-adaptables, habituellement sous forme d'un mécanisme ad-hoc. De plus, la communauté manque de standards de comparaison permettant l'évaluation de ces mécanismes d'adaptation et leur fiabilité. Dans cette thèse, pour faire face à ces problématiques, nous proposons un modèle formel permettant de préserver la qualité de service (QoS pour Quality of Service en anglais) à l'aide de contrats dans des applications reconfigurables à base de composants à l'exécution. Notre contribution comprend deux parties. Tout d'abord, nous proposons une solution complète allant de la définition d'un modèle formel de reconfiguration d'un système auto-adaptable fiable jusqu'à l'expérimentation, en démontrant l'applicabilité de l'approche dans une plate-forme à composants reconfigurables. Finalement, nous identifions et définissons des propriétés propres aux logiciels auto-adaptables permettant de les évaluer et de les comparer. Dans notre première contribution, nous identifions quatre éléments principaux : un modèle formel, une architecture de l'approche, une implémentation, et une évaluation sur deux expériences. Notre modèle formel définit un modèle de boucle de contrôle autonome permettant des reconfigurations autonomes. Le modèle propose des propriétés de fiabilité et se base sur la théorie de transformation des graphes typés attribués. Nous utilisons ce type de graphes et de transformations pour définir la structure des applications à base de composants, les contrats de QoS, et les règles de reconfiguration. Ces éléments sont définis par des structures typées qui garantissent que les instances correspondantes sont conformes au modèle. De plus, nous spécifions un ensemble d'opérations pour la reconfiguration dynamique en utilisant ces définitions. Notre approche bénéficie des théorèmes utilisés dans la transformation de graphes, pour garantir que le processus de reconfiguration soit résiliable, atomique, et vérifiable avec les règles structurelles définies dans les applications à base de composants. Pour faire face à l'imprévisibilité inhérente au changement de contexte, nous définissons une machine à états finis que gère à la fois les contrats qui sont respectés ainsi que ceux qui ne le sont pas. Nous développons une architecture pour mettre en œuvre notre modèle formel par l'intermédiaire d'une représentation, au moment de l'exécution, de l'application et des contrats de QoS associés sous forme de graphes. De plus, cette représentation permet la mise en place d'une liaison causale entre les graphes et l'application dont la cohérence est maintenue et garantie à l'aide de fonctions. Nous mettons en œuvre cette architecture sous la forme de composants SCA (Service Component Architecture pour son acronyme en anglais) à l'aide du cadre logiciel F RA SCATI, une plate-forme intergicielle multi-échelle définie dans l'équipe ADAM. Finalement, nous présentons une évaluation de notre expérience par un test de performance (benchmark) sur deux cas d'étude. Les résultats obtenus nous permettent de conclure l'applicabilité de l'approche proposée. Avec notre deuxième contribution, notre objectif est de faire face au manque actuel de méthodes de vérification des instances du modèle de boucle de contrôle de type MAPE-K (Monitor, Analysis, Planning, Execution et Knowledge par son acronyme en anglais). Ce modèle a été proposé sans qu'aucune propriété standardisée ne soit définie et qui pourrait permettre la comparaison des réalisations de cette boucle de contrôle. Nous avons identifié, à partir d'une étude bibliographique conséquente, un ensemble de propriétés inhérentes aux systèmes auto-adaptables. Nous avons proposé un ensemble de propriétés associées à cette étude. Parmi les propriétés identifiées les plus importantes, nous pouvons citer l'adaptation atomique, le temps de configuration (settling-time), la terminaison, la cohérence structurelle, la robustesse, le dépassement de ressources et la stabilité. Pour valider notre approche, nous avons analysé et vérifié les hypothèses pour les cinq premières propriétés. Avec notre première contribution, nous proposons des avancées dans le domaine de l'ingénierie logicielle pour les applications auto-adaptables. Avec notre deuxième contribution, nous apportons des éléments tangibles pour la standardisation des propriétés pour l'évaluation des systèmes auto-adaptables.