Guider et contrôler les reconfigurations de systèmes à composants: Reconfigurations dynamiques: modélisation formelle et validation automatique

Our main goal is to allow the usage of temporal properties within an adaptation policy while taking into account runtime verification specificities.In order to reach it, we define a component-based system model that supports dynamic reconfigurations. We introduce guarded reconfigurations in order to use primitive operations as "building blocks" to craft more elaborated reconfigurations involving, not only sequential, but also, alternate and repetitive constructs while ensuring the system's configurations consistency.Furthermore, we extend (to external events) the temporal logic previously used to express architectural constraints on configurations. Using, so called, progressive semantics, we can, in most of the cases, evaluate (in a centralised or decentralised fashion) a temporal expression for a given configuration using evaluations performed only at the previous configuration. We use this logic within adaptation policies enabling the steering and control of dynamic reconfigurations at runtime.Finally, we implemented such adaptation policies in various case studies using frameworks such as Fractal and FraSCAti. We also use behavioural fuzzing to test various specific aspects of a given adaptation policy.Notre objectif principal est de permettre l'utilisation de propriétés temporelles dans une politique d'adaptation en tenant compte des spécificités de la vérification à l'exécution.Pour y répondre, nous définissons un modèle de système à composants supportant les reconfigurations dynamiques. Nous introduisons les reconfigurations gardées qui nous permettent d'utiliser des opérations primitives en tant que "briques" pour construire des reconfigurations plus élaborées impliquant des constructions, non seulement, séquentielles, mais aussi alternatives ou répétitives, tout en garantissant la consistance des configurations du système.En outre, nous étendons (aux événements externes) la logique temporelle utilisée précédemment pour exprimer des contraintes architecturales sur des configurations. Avec une sémantique, dite progressive, nous pouvons, dans la plupart des cas, évaluer (de façon centralisée ou décentralisée) une expression temporelle pour une configuration donnée à partir d'évaluations déjà réalisées à la seule configuration précédente. Nous utilisons cette logique dans des politiques d'adaptation permettant de guider et contrôler les reconfigurations de systèmes à composants à l'exécution. Enfin, l'implémentation de politiques d'adaptation a été expérimentée dans divers cas d'études sur les plateformes Fractal et FraSCAti. Nous utilisons notamment le fuzzing comportemental afin de pouvoir tester des aspects spécifiques d'une politique d'adaptation