Domaines de recherche

  • Formalisation des systèmes distribués
  • Communication assynchrone
  • Courtage de services en calcul scientifique
  • Unification modulo une théorie équationelle
  • Grille de calcul
  • Composition de services
  • Application à l'algèbre linéaire et à l'optimisation

Encadrement

Thèses

  • Thèse de Florent Chevrou
    Co-direction Philippe Queinnec
    Début de thèse : Octobre 2014
    Sujet : "Formalisation des interactions asynchrones."
  • Thèse de Seriel Boussalia
    Co-direction Allaoua Chaoui (Laboratoire MISC Laboratory, université de Constantine 2, Algérie)
    Thèse soutenue en : Juin 2016
    Sujet : "Utilisation des méthodes d'optimisation pour trouver une meilleure solution de composition de services web."

Masters recherche

  • Master Adam Shimi
    Master recherche : Mars 2017 - Septembre 2017
    Sujet : "Impact de la paramétrisation dans les compositions de services."
  • Master Nathanaël Sensfelder
    Master recherche : Mars 2016 - Septembre 2016
    Sujet : "Modèles de communication applicatifs pour la composition de services répartis."
  • Master de Florent Chevrou
    Master recherche : Mars 2014 - Septembre 2014
    Sujet : "Modélisation et vérification de compositions de services répartis dans le monde asynchrone."

Publications

Toutes mes publications sont disponibles ici : [IRIT]
Mais aussi ici : [DBLP].

Projets

  • PARDI
    A parameterized system specification is a specification for a whole class of systems, parameterized by the number of entities and the properties of the interaction, such as the communication model (synchronous/asynchronous, order of delivery of message, application ordering) or the fault model (crash failure, message loss). To be able to verify such systems without explicitly instantiating all the parameters, new theoretical results and dedicated tools are required. Due to the fundamental undecidability of the problem, automatic tools are not powerful enough to verify rich parameterized systems: they are limited in their expressiveness and do not handle the variety of the interaction models. To assist and automate verification without parameter instantiation, PARDI uses two complementary approaches. First, a fully automatic model checker modulo theories is considered. Then, to go beyond the intrinsic limits of parameterized model checking, the project advocates a collaborative approach between proof assistant and model checker. This collaboration is two-ways: in one direction, the model checker is used as an explorer to generate elementary invariants that can be used and combined in interactive verification; in the other direction, a property which is needed by the proof assistant is discharged to the parameterized model checker.
    Cubicle, a model checker for array-based systems, and TLAPS, a proof assistant well-adapted to study distributed algorithms, are the basis of this project. Using case studies, both in parameterized distributed systems and in parameterized workflow-based systems, a theoretical analysis is required to exhibit the relevant parameters and to prove generic results (e.g. substitutability). This analysis is needed to define the richer data structures that will extend the model checker's expressiveness, and to inject these generic results into checkers and provers.
    A first contribution of the project will be the verification of parameterized distributed systems, for an arbitrary number of sites. A library of results for the many communication models and fault models which exist and their integration in the verification tools will be a second contribution. A third contribution will be the design and implementation of a verification toolchain based on a close interaction between a proof assistant and a model checker. A fourth contribution will be a new DSL for parameterized workflow-based systems with rich explicit parameterization features, and its translation into the checker and prover input language.
    PARDI is funded by the ANR, project ANR-16-CE25-0006, 2016-2020.
  • Cocasse
    Le projet vise la conception d’une plateforme qui offre un support de bout en bout pour la composition de services. L’objectif est de construire la composition certifiée de services hétérogènes en intégrant des propriétés fonctionnelles (i.e. comportementales) et non fonctionnelles (qualité de service / Quality of Service).
    Les systèmes logiciels sont souvent construits par composition et intégration de plusieurs sous-systèmes distribués, autonomes et hétérogènes, que l’on appelle services. Il est nécessaire de fournir des spécifications et des méthodes formelles de sorte à permettre de construire cette composition et de la certifier. Ceci soulève plusieurs problématiques, à savoir : 1) sélection multicritère des services, 2) adaptation, et 3) certification, qui seront résolues au sein d’une plateforme partagée..
    1. Pour le premier point, nous nous basons sur BPMN (Business Process Modelling and Notation) pour la spécification des processus métiers abstraits décrivant les besoins en termes de propriétés attendues. Plus spécifiquement, le problème sera abordé suivant deux points de vues complémentaires : analyse comportementale et analyse non fonctionnelle (e.g., analyse temporisée). Une difficulté est que lors d’une collaboration entre services ayant des comportements différents, le comportement temporisé de chaque service peut avoir implicitement un impact sur le comportement des autres services. Ainsi, des conflits aussi bien comportementaux que temporels peuvent surgir. Ceux-ci peuvent être dépendants.
    2. Le deuxième point concerne l’adaptation des services en cas de conflits. L’adaptation des services aide à pallier les problèmes de compatibilité pour construire des compositions et les améliorer. La plateforme déterminera automatiquement le contrat d’adaptation qui décrit comment les incompatibilités peuvent êtres résolues, afin de générer un service intermédiaire (l’adaptateur).
    3. Enfin, le projet vise à certifier que les compositions construites sont correctes. Dans ce but, la plateforme va s’appuyer sur la trace des actions qui ont menées à la génération de la composition pour produire automatiquement une preuve Coq afin que l'assistant de preuve en garantisse la correction.
    Le projet Cocasse a été financé par Toulouse Tech InterLabs
  • GRID-TLSE
  • NAREGI

Séjours à l'étranger

  • Séjour à Hawaii (Janvier - Février 2011)
    Utilisation des outils de machine learning pour évaluer les compositions de services et déterminer laquelle est la meilleure (en terme de temps d'exécution).
  • Séjour dans le Tennessee (Août - Septembre - Octobre 2009)
    Intégration de mon outil de courtage de services au sein de l'intergiciel de grille GridSolve.
  • Postdoc au sein du projet Naregi
    La globalisation des ressources sur les grilles introduit le besoin de mécanismes de matchmaking. Un matchmaker trouve l'ensemble des ressources qui répondent aux besoins de l'utilisateur et les lui renvoie. Dans ce travail, nous proposons un matchmaker basé sur les ontologies. Les exigences de l'utilisateur et les ressources sont décrits grâce à des ontologies. Les exigences de l'utilisateur sont décrites à l'aide d'un workflow complexe (composé de travaux en parallèle, séquences, soumis à condition, boucle, co-alloués,...). Pour chaque travail unitaire, les exigences peuvent porter sur le nombre de CPU, la quantité de mémoire, le type d'OS, l'architecture,... Elles peuvent également être complétées par des contraintes de temps. La description des ressources permet de spécifier les caractéristiques physique des ressources (nombre de CPU, mémoire, réseau,...) mais aussi les applications installées et les politiques d'accès. Le matchmaker prend ces informations en considération pour trouver les systèmes qui correspondent aux besoins de l'utilisateur et qu'il est autorisé à utiliser. Les conditions d'utilisation sont également renvoyées.