Mes travaux de recherche portent sur les modèles de programmation distribuée, principalement par objets et composants. Dans ce domaine, j'ai travaillé à fournir des outils facilitant la programmation d'applications distribuées à large échelle et vérifiant la correction de leur comportement. Pour faciliter la programmation d'applications distribuées je me suis intéressé à la mise au point de langages avec un fort niveau d'abstraction: objets actifs, squelettes algorithmiques, composants. Afin de vérifier la correction du comportement d'une application j'ai collaboré à la mise au point d'outils de spécification et de vérification comportementales d'applications distribuées. Mes travaux ont pour but de fournir un modèle formel des langages de programmations, des bibliothèques, et des environnements d'exécution fournies au programmeur afin de garantir un comportement sûr des applications distribuées. Ma thèse m'a permis de mettre au point le calcul ASP modélisant lecomportement des objets actifs et des futurs. Depuis, nous avons créé une version fonctionnelle de ce calcul que nous avons modélisé en Isabelle/HOL. Aussi j'ai fortement contribué à la définition d'un modèle à composants distribués -- le GCM (Grid Component model)--, à sa formalisation et à son utilisation pour programmer des composants adaptables ou autonomes. Enfin, j'ai contribué à la spécification et la vérification comportementale des programmes utilisant des objets actifs et des composants afin de garantir la sûreté de leur exécution. Actuellement, nous travaillons à la fois à une extension multi-threadée du modèle à objets actifs mieux adaptée aux machines multi-coeurs, et à l'utilisation de méthodes formelles pour mettre au point et prouver la correction d'un algorithme de diffusion pour réseau pair-à-pair de type CAN (Content Adressable Network). Ce manuscrit fournit une vue d'ensemble de tous ces travaux.

Le concept d'objet actif est un modèle de calcul puissant utilisé pour définir des systèmes distribués et concurrents. Dans ce travail, nous étudions un modèle d'objet actif sans type futur explicite et avec 'attente par nécessité', une technique qui déclenche une synchronisation sur la valeur retournée par une invocation lorsque celle-ci est strictement nécessaires. Bien que la concurrence élevée combinée à un haut niveau de transparence conduise à de bonnes performances, elles rendent le système plus propice à des problèmes comme les deadlocks. C'est la raison qui nous a conduit à étudier l'analyse de deadlocks dans ce modèle d'objets actifs. Le développement de notre analyse de les deadloks est divisé en deux travaux principaux. Dans le premier travail, nous nous concentrons sur la synchronisation implicite sur la disponibilité d'une certaine valeur. De cette façon, nous pouvons analyser la synchronisation des flux de données inhérente aux langues qui permettent une attente par nécessité. Dans le deuxième travail, nous présentons une technique d'analyse statique basée sur des effets et des types comportementaux pour dériver des modèles de synchronisation d'objets actifs et confirmant l'absence de deadlock dans ce contexte. Notre système d'effets trace l'accès aux champs d'objet, ce qui nous permet de calculer des types comportementaux qui expriment des modèles de synchronisation de manière précise. En conséquence, nous pouvons vérifier automatiquement l'absence de blocages dans des programmes basés sur des objets actifs avec des synchronisations d'attente par nécessité et des objets actifs dotés d’un état interne. / The active object concept is a powerful computational model for defining distributed and concurrent systems. This model has recently gained prominence, largely thanks to its simplicity and its abstraction level. In this work we study an active object model with no explicit future type and wait-by-necessity synchronisations, a lightweight technique that synchronises invocations when the corresponding values are strictly needed. Although high concurrency combined with a high level of transparency leads to good performances, they also make the system more prone to problems such as deadlocks. This is the reason that led us to study deadlock analysis in this active objects model.The development of our deadlock analysis is divided in two main works. In the first work we focus on the implicit synchronisation on the availability of some value. This way we are able to analyse the data-flow synchronisation inherent to languages that feature wait-by-necessity. In the second work we present a static analysis technique based on effects and behavioural types for deriving synchronisation patterns of stateful active objects and verifying the absence of deadlocks in this context. Our effect system traces the access to object fields, thus allowing us to compute behavioural types that express synchronisation patterns in a precise way. As a consequence we can automatically verify the absence of deadlocks in active object based programs with wait-by-necessity synchronisations and stateful active objects.