Un framework formel pour les architectures logicielles dynamiques

Software architectures play a significant role in the development of software-intensive systems in order to allow satisfying both functional and non-functional requirements. In particular, dynamic software architectures have emerged to address characteristics of the contemporary systems that operate on dynamic environments and consequently subjected to changes at runtime. Architecture description languages (ADLs) are used to represent software architectures, producing models that can be used at design time and/or runtime. However, most existing ADLs have limitations in several facets: (i) they are focused on structural, topological aspects of the architecture; (ii) they do not provide an adequate support for representing behavioral aspects of the architecture; (iii) they do not allow describing advanced aspects regarding the dynamics of the architecture; (iv) they are limited with respect to the automated verification of architectural properties and constraints; and (v) they are disconnected from the implementation level, thus entailing inconsistencies between architecture and implementation. In order to tackle these problems, this thesis proposes formally founded framework for dynamic software architectures. Such a framework comprises: (i) .-ADL, a formal language for describing software architectures under both structural and behavioral viewpoints; (ii) the specification of programmed dynamic reconfiguration operations; (iii) the automated generation of source code from architecture descriptions; and (iv) an approach based on statistical model checking (SMC) to formally express and verify properties in dynamic software architectures. The main contributions brought by the proposed framework are fourfold. First, the .-ADL language was endowed with architectural-level primitives for describing programmed dynamic reconfigurations. Second, architecture descriptions in .-ADL are translated towards implementation source code in the Go programming language, thereby contributing to minimize architectural drifts. Third, a novel logic, called DynBLTL, is used to formally express properties in dynamic software architectures. Fourth, a toolchain relying on SMC was built to automate the verification of architectural properties while striving to reduce effort, computational resources, and time for performing such a task. In this work, two wireless sensor network-based systems are used to validate the framework elements.Les architectures logicielles ont un rôle important dans le développement de systèmes à logiciel prépondérant afin de permettre la satisfaction tant des exigences fonctionnelles que des exigences extra-fonctionnelles. En particulier, les architectures logicielles dynamiques ont émergé pour faire face aux caractéristiques des systèmes contemporains qui opèrent dans des environnements dynamiques et par conséquent susceptibles de changer en temps d’exécution. Les langages de description architecturale (ADLs) sont utilisés pour représenter les architectures logicielles en produisant des modèles qui peuvent être utilisés pendant la conception ainsi que l’exécution. Cependant, la plupart des ADLs existants sont limités sur plusieurs facettes : (i) ils ne décrivent que les aspects structurels, topologiques de l’architecture ; (ii) ils ne fournissent pas un support adéquat pour représenter les aspects comportementaux de l’architecture ; (iii) ils ne permettent pas de décrire des aspects avancés de la dynamique de l’architecture ; (iv) ils sont limités en ce qui concerne la vérification automatisée des propriétés et des contraintes architecturales ; et (v) ils sont déconnectés du niveau d’implémentation et entraînent souvent des incohérences entre l’architecture et l’implémentation. Pour faire face à ces problèmes, cette thèse propose un framework formel pour les architectures logicielles dynamiques. Ce framework comprend : (i) .-ADL, un langage formel pour décrire des architectures logicielles dynamiques sous les perspectives structurelles et comportementales ; (ii) la spécification des opérations de reconfiguration dynamique programmée ; (iii) la génération automatique de code source à partir des descriptions architecturales ; et (iv) une approche basée sur la vérification statistique pour exprimer et vérifier formellement des propriétés des architectures logicielles dynamiques. Les contributions principales apportées par le framework proposé sont quatre. Premièrement, le langage .-ADL a été doté de primitives de niveau architectural pour décrire des reconfigurations dynamiques programmées. Deuxièmement, les descriptions architecturales dans .-ADL sont transformées vers le code source d’implémentation dans le langage de programmation Go, en contribuant à minimiser les dérives architecturales. Troisièmement, une nouvelle logique appelée DynBLTL est utilisée pour exprimer formellement des propriétés dans les architectures logicielles dynamiques. Quatrièmement, un outil basé sur SMC a été développé pour automatiser la vérification des propriétés architecturales en cherchant à réduire l’effort, les ressources computationnelles, et le temps pour réaliser cette tâche. Dans ce travail, deux systèmes basés sur réseaux de capteurs sans fil sont utilisés pour valider les éléments du framework