Cette thèse propose une Démarche de Vérification Formelle d'Architectures Logicielles : DVFAL. La démarche DVFAL supporte divers formalismes de description d'architectures logicielles tels que : les ADL (langages de description d'architectures), UML2.0, Symphony et des profils UML2.0 dédiés au domaine des architectures logicielles. La démarche DVFAL préconise l'ADL Wright en tant que langage formel pivot permettant de représenter des architectures logicielles décrites dans les divers formalismes. En outre, elle propose des transformations de modèles sous forme des traducteurs (Wright vers CSP de Hoare et Wright vers Ada) pour bénéficier des outils de vérification des propriétés supportant CSP et Ada tels que FDR et FLAVERS. Enfin, la démarche DVFAL propose un profil UML2.0-Wright jouant le rôle d'un langage intermédiaire entre les formalismes à base d'UML et Wright.

L'architecture logicielle est devenue un thème scientifique majeur de l'informatique. En effet, l'architecture logicielle fournit l'abstraction qui permet de développer rigoureusement et de faire évoluer des systèmes logiciels complexes au vu des besoins tant fonctionnels que non fonctionnels. Afin de modéliser les architectures logicielles, un nouveau type de langage est apparu : les langages de description d'architectures (ADL, Architecture Description Language). Divers ADL ont été proposés dans la littérature, mais ces ADL sont restreints à la modélisation d'architectures abstraites, indépendantes des plateformes d'implémentation. Lors de l'implémentation, l'architecture n'est plus représentée. Cette thèse s'inscrit dans le domaine des ADL et porte sur la définition et la mise en œuvre d'un langage pour la concrétisation, c'est-à-dire l'implémentation explicite, d'architectures logicielles. Elle adresse le problème de la construction d'un tel langage et son système d'exécution. Pour cela elle aborde le problème d'un point de vue nouveau : la construction d'un langage centré sur l'architecture logicielle. Assis sur des bases formelles, notamment sur le π-calcul et π-ADL, ces travaux ont donné lieu à un langage formel pour décrire et garantir l'intégrité architecturale d'un système au niveau de sa spécification, de son implémentation et de ses évolutions ultérieures. La machine virtuelle et le compilateur associé sont enfouis dans la plateforme .NET.

L'évolution constante des applications et le besoin toujours croissant de performances imposent le développement de nouvelles architectures compétitives et évolutives au sein de systèmes reconfigurables dynamiquement sur puces. Ces contraintes ont amené à une complexification des architectures, de leurs mécanismes de reconfiguration et de leur conception. De manière à répondre efficacement à ce problème, des plate-formes de développement ont été conçues et permettent ainsi d'automatiser certains processus constituant la chaîne de conception d'une architecture. Cela est rendu possible par l'intermédiaire d'un langage de description haut niveau (ADL) qui permet, par une spécification rapide de certains paramètres matériels, de procéder rapidement à la génération d'une architecture et de ses outils de développement adaptés tels que des outils de simulation, de compilation ou encore de synthèse. Cette thèse se place dans le contexte de la modélisation haut niveau des architectures ainsi que dans le contexte de l'aide à la conception et à l'exploration d'architectures reconfigurables dynamiquement. Ce document présente la plate-forme de développement Mozaïc dont l'objectif est de permettre la conception d'architectures reconfigurables dynamiquement par l'introduction automatique de ressources matérielles dédiées et adaptées. Dans une première partie, nous détaillons les concepts de reconfiguration dynamique qui ont été développés et mis en oeuvre dans Mozaïc. Dans une deuxième partie, nous présentons le langage de description haut niveau xMAML qui permet la spécification de l'architecture et de l'exploitation efficace des mécanismes précédemment présentés. Ce langage est basé sur l'ADL MAML développé à l'université d'Erlangen, auquel nous avons ajouté certains paramètres de spécifications nécessaires à la mise en oeuvre de la reconfiguration dynamique ainsi qu'à la spécification d'architectures hétérogènes. Enfin, dans un dernier chapitre, nous présentons les différentes phases de développement, et les outils associés, de deux architectures reconfigurables dynamiquement que sont les FPGAs et le processeur reconfigurable DART. Cette présentation inclut les phases d'exploration et l'implémentation d'un décodeur WCDMA par reconfiguration dynamique sur le FPGA modélisé par xMAML.