Cette thèse appartient au domaine des méthodes formelles. Nous nous concentrons sur leur application à une méthodologie spécifique pour le développement de logiciels: l'ingénierie à base de composants. Le Grid Component Model (GCM) suit cette méthodologie en fournissant tous les moyens pour définir, composer, et dynamiquement reconfigurer les applications distribuées à base de composants. Dans cette thèse, nous abordons la spécification formelle, la vérification et le déploiement d'applications GCM reconfigurables et distribuées. Notre première contribution est un cas d'étude industriel sur la spécification comportementale et la vérification d'une application distribuée et reconfigurable: L'HyperManager. Notre deuxième contribution est une plate-forme, élaborée avec l'assistant de preuve Coq, pour le raisonnement sur les architectures logicielles: Mefresa. Cela comprend la mécanisation de la spécification du GCM, et les moyens pour raisonner sur les architectures reconfigurables GCM. En outre, nous adressons les aspects comportementaux en formalisant une sémantique basée sur les traces d'exécution de systèmes de transitions synchronisées. Enfin, notre troisième contribution est un nouveau langage de description d'architecture (ADL): Painless. En outre, nous discutons son intégration avec ProActive, un intergiciel Java pour la programmation concurrente et distribuée, et l'implantation de référence du GCM. / This thesis belongs to the domain of formal methods. We focus their application on a specific methodology for the development of software: component-based engineering.The Grid Component Model (GCM) endorses this approach by providing all the means to define, compose and dynamically reconfigure component-based distributed applications. In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties. Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Further, we discuss its proof-of-concept integration with ProActive, a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM.

Au cours de la dernière décennie, la complexité des applications a considérablement évolué afin de répondre aux besoins métiers émergeants. Leur conception implique une composition distribuée de composants logiciels. Ces applications fournissent des services à travers les interactions métiers maintenues par leurs composants. De telles applications sont intrinsèquement en évolution dynamique en raison de la dynamicité de leurs contextes. En effet, elles évoluent dans des environnements qui changent tout en présentant des conditions très dynamiques durant leur cycle de vie d’exécution. De tels contextes représentent une lourde charge pour les développeurs aussi bien pour leurs tâches de conception que de gestion. Cela a motivé́ le besoin de renforcer l’autonomie de gestion des applications pour les rendre moins dépendantes de l’intervention humaine en utilisant les principes de l’Informatique Autonomique. Les Systèmes Informatiques Autonomes (SIA) impliquent l’utilisation des boucles autonomiques, dédiées aux systèmes afin de les aider à accomplir leurs tâches de gestion. Ces boucles ont pour objectif d’adapter leurs systèmes à la dynamicité de leurs contextes, en se basant sur une logique d’adaptation intégrée. Cette logique est souvent donnée par des règles statiques codées manuellement. La construction de ces règles demande beaucoup de temps tout en exigeant une bonne expertise. En fait, elles nécessitent une compréhension approfondie de la dynamicité du système afin de prédire les adaptations précises à apporter à celui-ci. Par ailleurs, une telle logique ne peut envisager tous les scénarios d’adaptation possibles, donc, ne sera pas en mesure de prendre en compte des adaptations pour des situations précédemment inconnues. Les SIA devraient donc être assez sophistiqués afin de pouvoir faire face à la nature dynamique de leurs contextes et de pouvoir apprendre par eux-mêmes afin d’agir correctement dans des situations inconnues. Les SIA devraient également être capables d’apprendre de leur propre expérience passée afin de modifier leur logique d’adaptation en fonction de la dynamicité de leurs contextes. Dans ce manuscrit, nous abordons les lacunes décrites en utilisant les techniques d’Apprentissage par Renforcement (AR) afin de construire notre logique d’adaptation. Cependant, les approches fondées sur l’AR sont connues pour leur mauvaise performance lors des premières phases d’apprentissage. Cette mauvaise performance entrave leur utilisation dans le monde réel des systèmes déployés. Par conséquent, nous avons amélioré cette logique d’adaptation avec des capacités d’apprentissage plus performantes avec une approche AR en multi-pas. Notre objectif est d’optimiser la performance de l’apprentissage et de le rendre plus efficace et plus rapide, en particulier durant les premières phases d’apprentissage. Nous avons aussi proposé́ un cadriciel générique visant à aider les développeurs dans la construction d’applications auto-adaptatives. Nous avons donc proposé de transformer des applications existantes en ajoutant des capacités d’autonomie et d’apprentissage à leurs composants. La transformation consiste en l’encapsulation des composants dans des conteneurs autonomiques pour les doter du comportement auto-adaptatif nécessaire. Notre objectif est d’alléger la charge des tâches de gestion des développeurs et de leur permettre de se concentrer plus sur la logique métier de leurs applications. Les solutions proposées sont destinées à être génériques, granulaires et basées sur un standard connu, à savoir l’Architecture de Composant de Service. Enfin, nos propositions ont été évaluées et validées avec des résultats expérimentaux. Ils ont démontré leur efficacité en montrant un ajustement dynamique des applications transformées face aux dynamicités de leurs contextes en un temps beaucoup plus court comparé aux approches existantes / During the past decade, the complexity of applications has significantly scaled to satisfy the emerging business needs. Their design entails a composition of distributed and interacting software components. They provide services by means of the business interactions maintained by their components. Such applications are inherently in a dynamic evolution due to their context dynamics. Indeed, they evolve in changing environments while exhibiting highly dynamic conditions during their execution life-cycle (e.g., their load, availability, performance, etc.). Such contexts have burdened the applications developers with their design and management tasks. Subsequently, motivated the need to enforce the autonomy of their management to be less dependent on human interventions with the Autonomic Computing principles. Autonomic Computing Systems (ACS) implies the usage of autonomic loops, dedicated to help the system to achieve its management tasks. These loops main role is to adapt their associated systems to the dynamic of their contexts by acting upon an embedded adaptation logic. Most of time, this logic is given by static hand-coded rules, often concern-specific and potentially error-prone. It is undoubtedly time and effort-consuming while demanding a costly expertise. Actually, it requires a thorough understanding of the system design and dynamics to predict the accurate adaptations to bring to the system. Furthermore, such logic cannot envisage all the possible adaptation scenarios, hence, not able to take appropriate adaptations for previously unknown situations. ACS should be sophisticated enough to cope with the dynamic nature of their contexts and be able to learn on their own to properly act in unknown situations. They should also be able to learn from their past experiences and modify their adaptation logic according to their context dynamics. In this thesis manuscript, we address the described shortcomings by using Reinforcement Learning (RL) techniques to build our adaptation logic. Nevertheless, RL-based approaches are known for their poor performance during the early stages of learning. This poor performance hinders their usage in real-world deployed systems. Accordingly, we enhanced the adaptation logic with sophisticated and better-performing learning abilities with a multi-step RL approach. Our main objective is to optimize the learning performance and render it timely-efficient which considerably improves the ACS performance even during the beginning of learning phase. Thereafter, we pushed further our work by proposing a generic framework aimed to support the application developers in building self-adaptive applications. We proposed to transform existing applications by dynamically adding autonomic and learning abilities to their components. The transformation entails the encapsulation of components into autonomic containers to provide them with the needed self-adaptive behavior. The objective is to alleviate the burden of management tasks on the developers and let them focus on the business logic of their applications. The proposed solutions are intended to be generic, granular and based on a well known standard (i.e., Service Component Architecture). Finally, our proposals were evaluated and validated with experimental results. They demonstrated their effectiveness by showing a dynamic adjustment to the transformed application to its context changes in a shorter time as compared to existing approaches