Search

My research focuses on distributed programming models, more precisely using ob jects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction: active ob jects, algorithmic skeletons, components. To verify correction of the behaviour of an application, I have contributed to the creation of tools for specifying and verifying behavioural distributed applications. My work aims to provide a strong model of programming languages, libraries, and runtime environments provided to the developer, and to guarantee the safe behaviour of distributed applications. During my thesis, I developed the ASP calculus for modelling the behaviour of active ob jects and futures. Since, we created a functional version of this calculus and formalised it in Isabelle/HOL. I also strongly contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. Finally, I contributed to the specification and behavioural verification of programs based on active ob jects and components, in order to ensure their safe execution. Currently we are working both on a multi-threaded extension of the active ob ject model, better suited for multi-core machine, and on the use of formal methods to design and prove the correction of an algorithm for broadcast on CAN-like peer-to-peer networks (Content Addressable Network). This manuscript provides an overview of all these works.; 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.

My research focuses on distributed programming models, more precisely using ob jects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction: active ob jects, algorithmic skeletons, components. To verify correction of the behaviour of an application, I have contributed to the creation of tools for specifying and verifying behavioural distributed applications. My work aims to provide a strong model of programming languages, libraries, and runtime environments provided to the developer, and to guarantee the safe behaviour of distributed applications. During my thesis, I developed the ASP calculus for modelling the behaviour of active ob jects and futures. Since, we created a functional version of this calculus and formalised it in Isabelle/HOL. I also strongly contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. Finally, I contributed to the specification and behavioural verification of programs based on active ob jects and components, in order to ensure their safe execution. Currently we are working both on a multi-threaded extension of the active ob ject model, better suited for multi-core machine, and on the use of formal methods to design and prove the correction of an algorithm for broadcast on CAN-like peer-to-peer networks (Content Addressable Network). This manuscript provides an overview of all these works.; 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.

Composition of Applications and their User Interfaces driven by the Functional Composition Software reuse is not a recent issue. Many approaches have been proposed in the literature enabling the reuse of part or complete application including its functionalities and User Interface (UI). At the functional level, based on the appearance of services and components, these approaches ease the process of building and extending applications by composing independent functionalities. At the UI level, they offer solution to create new UI by the composition of existing ones. Several approaches focus on the application composition. However, they only propose to realize simple composition. Also focusing on the application composition, the approach presented in this thesis eases better the whole composition process. It allows software developer to design new application by reusing all components of existing applications including functionalities, UIs and interaction between functionalities and UIs. Our approach enables software developer to use existing industrial tools serving for functionality composition. Thus, through this process, desirable widgets can be identified and reused to create the resulting application. The proposed approach is based on a meta-model called AliasComponent that provides a componentbased architecture to describe applications by distinguishing the functional part, UIs and interactions between them, and functional composition. This metamodel focuses only on important information captured from existing applications, and functional composition. A formalization has been described to validate the intermediate results during the composition process. With this formalization, any useful widgets are selected, in case of multiple widgets, a list of possible ones is show, helping the developer to make a choice and finally create the resulting application. In this formalization, we define some properties that application and composition result must respect and ensure that the resulting application is useful. The metamodel and formalization are integrated in a composition tool which validites the approach presented in this thesis.; La réutilisation d'applications n'est pas un problème récent et de nombreux travaux ont étudié différentes façons de réutiliser tout ou partie d'une application. L'apparition des services et des composants au niveau fonctionnel facilite la construction et l'extension d'applications par composition de fonctionnalités indépendantes. En parallèle, des travaux sur les Interfaces Homme-Machine (IHM) proposent des solutions pour créer des IHM par composition d'IHM existantes. Mais ce n'est que récemment que des travaux se sont intéressés à composer l'ensemble d'une application. Malgré cela, ils ne proposent que des compositions simples tant au niveau des IHM que fonctionnel. Ces travaux de thèse proposent une approche pour faciliter le travail du développeur en lui permettant de réutiliser l'intégralité des applications à composer, c'est-à-dire, la partie fonctionnelle, l'IHM et les interactions entre l'IHM et la partie fonctionnelle. La proposition faite dans cette thèse lui permet de continuer d'utiliser les outils industriels dont il dispose pour composer les parties fonctionnelles des applications. Ainsi, c'est au travers de cette composition fonctionnelle ainsi que des interactions entre la partie fonctionnelle et l'IHM présentes dans les applications que se fera l'identification des éléments d'IHM à conserver et la création de l'application résultante. Cette approche repose sur un méta-modèle AliasComponent qui fournit une architecture à base de composants permettant de décrire à la fois les applications (en distinguant la partie fonctionnelle, les IHM et les interactions entre les deux) et la composition fonctionnelle. Ce méta-modèle permet ainsi d'extraire des applications existantes et de la composition fonctionnelle l'ensemble des informations essentielles à la réalisation de la composition des applications. Elle s'appuie aussi sur une formalisation qui permet la réalisation de la composition, c'est-à-dire, la déduction des éléments d'IHM à conserver, la détection de doublons non identiques (lorsque plusieurs widgets différents peuvent convenir), l'aide à la résolution de ceux-ci et la création de l'application résultante de la composition. Cette formalisation pose également les propriétés que doivent respecter les applications et le résultat de la composition assurant ainsi une application résultante fonctionnelle. Le méta-modèle et la formalisation sont intégrés au sein d'un processus d'aide à la composition. La solution proposée a, quant à elle, été mise en oeuvre au sein d'un atelier d'aide à la composition qui a permis de valider l'approche.

Nos travaux de recherche portent sur la composition fiable d'activités logicielles. Ils s'inscrivent dans le cadre général du génie logiciel, et concernent les étapes de conception, implantation et adaptations d'applications logicielles réparties. Le thème central développé est la modélisation des activités et leur composition tout en garantissant différentes propriétés. La spécificité de ce travail et son originalité est d'avoir suivi une approche de la composition non pas dirigée par les langages mais par les éléments clefs de la composition indépendamment de mises en œuvres spécifiques. En fondant ce travail sur une approche formelle, nous proposons une vision unifiée d'un procédé de composition, et caractérisons les différences en terme d'interprétations. En étayant cette formalisation par plusieurs mises en œuvre à la fois en terme d'environnement de programmation et d'applications nous ancrons cette approche dans une réalité fonctionnelle. Les principales applications de ce travail portent sur la composition d'interactions entre composants hétérogènes et la composition de Workflows.

Medical images analysis today requires high end computing infrastructures to face the growing need for computing power and distributed medical data management. Medical applications increasingly require the federation of large data sets distributed over the image acquisition centers and their processing (e.g. for epidemiological studies, statistical construction of atlas, medical image analysis procedures validation...). We are interested in the use of production grids which represent affordable computing infrastructures, externalized for the non-specialized clinical centers. Furthermore, grids foster collaborative work by easing the sharing of data, processing, data analysis procedures, and so on. Exploiting grid infrastructures for medical data analysis require to fulfill specific requirements associated to medical image processing such as data protection, large data sets manipulation and easy set up of multiple data analysis procedures. In this defense, we will show how we came from medical image analysis procedures validation to the exploitation of grid infrastructures. We will analyze the needs related to this application area. The work we are doing to interface clinical storage with grid data management systems and to represent and efficiently process data-driven application workflows on a grid infrastructure will then be presented. Probabilistic modeling of the grid execution will be proposed and strategies to schedule and efficiently execute data-intensive workflows on a grid will be derived. Results will be shown on the Bronze Standard, an application to medical image registration algorithms assessment, exploiting both the EGEE production grid infrastructure and the Grid5000 National experimental grid.; Non disponible

Medical images analysis today requires high end computing infrastructures to face the growing need for computing power and distributed medical data management. Medical applications increasingly require the federation of large data sets distributed over the image acquisition centers and their processing (e.g. for epidemiological studies, statistical construction of atlas, medical image analysis procedures validation...). We are interested in the use of production grids which represent affordable computing infrastructures, externalized for the non-specialized clinical centers. Furthermore, grids foster collaborative work by easing the sharing of data, processing, data analysis procedures, and so on. Exploiting grid infrastructures for medical data analysis require to fulfill specific requirements associated to medical image processing such as data protection, large data sets manipulation and easy set up of multiple data analysis procedures. In this defense, we will show how we came from medical image analysis procedures validation to the exploitation of grid infrastructures. We will analyze the needs related to this application area. The work we are doing to interface clinical storage with grid data management systems and to represent and efficiently process data-driven application workflows on a grid infrastructure will then be presented. Probabilistic modeling of the grid execution will be proposed and strategies to schedule and efficiently execute data-intensive workflows on a grid will be derived. Results will be shown on the Bronze Standard, an application to medical image registration algorithms assessment, exploiting both the EGEE production grid infrastructure and the Grid5000 National experimental grid.; Non disponible

This thesis presents the results of the Coopeer research project about collaborative design. This work provides a way of building a peer-to-peer architecture for computer-aided design (CAD) associated to an automatic and optimistic conflict resolution method for replicated data consistency. This method is based on a timestamp with double identification and on a simultaneity management based on priorities. Workgroup management and fault tolerance are also addressed. The method is applicable to CAD systems, but also to any kind of complex collaborative software., Cette thèse présente les résultats du projet de recherche Coopeer sur le thème de la conception collaborative. Ce travail a permis de mettre en place une architecture d'égal à égal pour la conception assistée par ordinateur (CAO) associée à une méthode optimiste de résolution automatique des conflits pour assurer la cohérence des données répliquées. Cette méthode s'appuie sur une estampille à double identification et sur une gestion de la simultanéité basée sur des priorités. La gestion du groupe de travail et la tolérance aux pannes y sont également adressées. La méthode est applicable à la CAO, mais aussi à tout type d'application collaborative complexe.