Equipe de recherche MEXICO

Modeling and Exploitation of Interaction and Concurrency

Présentation de l'équipe

Dans un environnement où les réseaux sont de plus en plus présents, la fiabilité des applications devient d'autant plus critique que le nombre d'utilisateurs des systèmes de communication, services Web, moyens de transport, etc., augmente constamment. Les travaux de MExICo ont pour motivation une meilleure compréhension et une fiabilité accrue des systèmes distribués asynchrones, et s'intéressent particulièrement à la concurrence et à l'interaction. Avec la taille croissante et le déploiement en réseau des systèmes de communication, des contrôleurs, des services etc. nous sommes confrontés à un très grand degré de parallélisme entre les processus locaux. Dans toutes les formes d'analyse et de contrôle, une vision globale du système conduit à une explosion du nombre d'états et de transitions, qui nuit à la mise en valeur des mécanismes mis en œuvre. À l'inverse, en respectant la concurrence, on évite l'énumération exhaustive des entrelacements, et on peut se concentrer sur les propriétés essentielles des comportements non séquentiels caractérisés par les relations de causalité. Nous voyons la concurrence dans les systèmes distribués comme une opportunité plutôt qu'un obstacle qui conduit à l'explosion du nombre d'états des modèles formels et ralentit les algorithmes.

Axes de recherche

  • Diagnostic et diagnosticabilité. Le problème du diagnostic pour les systèmes à événements discrets est de détecter, à partir d'un flot d'observations, si des erreurs se sont produites dans le système. Les algorithmes de diagnostic doivent s'adapter à un contexte d'observabilité réduite, où de nombreux événements ne sont pas visibles par le superviseur. Vérifier l'observabilité et la crucial et non trivial. MExICo s'intéresse aux aspects suivants :
    • Diagnostic à base de dépliages
    • Observabilité et diagnosticabilité
    • Diagnostic décentralisé
  • Test. Soit une spécification donnée par un modèle formel M et une > implémentation I, supposée conforme à M ; le comportement de I est > influencé par le flot des entrées reçues, et il n'est observable que > via un flot de sorties. Le test de conformité consiste à construire, > quand c'est possible, des flots d'entrées qui permettent de déterminer > si I est conforme à M. MExICo s'intéresse au test des systèmes > distribués asynchrones.
    • Dans le test asynchrone, un testeur centralisé envoie des entrées non séquentielles et observe des sorties sur différents ports sous forme d'ordres partiels.
    • Dans le test local, plusieurs processus envoient des messages de test à leurs voisins et observent localement les réponses ; le problème de test consiste à déterminer la conformance globale à partir des résultats locaux.
  • Synthèse de contrôleurs. Dans un environnement distribué, il s'agit de synthétiser un programme distribué ou des contrôleurs distribués qui communiquent localement avec les composants du système. La principale difficulté vient du fait que les contrôleurs (ou programmes) ont seulement une vue partielle du système. Il est essentiel de spécifier les propriétés directement en termes de causalité en utilisant des modèles d'exécutions fondés sur les ordres partiels comme les MSCs ou les traces de Mazurkiewicz.
  • Adaptation et boîtes grises. Contrairement aux applications monolithiques du passé, on observe que de plus en plus de services ne sont plus fournis par un seul serveur mais par l'interaction et la coopération de plusieurs composants spécialisés. Comme ces composants ont des provenances diverses, on ne peut plus supposer que l'on a accès à leur technologie interne (comme dans le cas des technologies propriétaires). Ainsi, pour composer des services Web, pour déterminer la violation de contrats ou de spécifications, pour adapter des services existants à de nouvelles situations etc., on doit analyser les interactions entre des composants dont on ne connaît que l'interface publique, que l'on décrit comme des « boîtes grises ». On voit apparaître trois points essentiels :
    • l'abstraction
    • la composition
    • l'adaptation
  • Domaines d'application
    • Sécurité routière
    • Adaptation pour la composition des services Web
    • Télécommunications

Relations industrielles et internationales

  • EMoTiCon: Equivalences between Models with Time and Concurrency. Projet de l'institut Farman de l'ENS Cachan avec le LURPA (Laboratoire Universitaire de Recherche en Production Automatisée).
  • SMYLE: EGIDE/DAAD (Procope 2008/2009), avec Munich et Aix-la-Chapelle, sur le passage des spécifications en MSCs aux modèles de conception.
  • Relations et échanges soutenus avec le Chennai Mathematical Institute (CMI), Inde ; ARCUS.
  • Projet ANR DOTS (distributed, open and timed systems) avec l'IRCCyN, l'IRISA, le LaBRI et le LAMSADE.
  • Participation au projet européen Disc (distributed supervisory control of large plants) avec des partenaires académiques et industriels en France, en Italie, aux Pays-Bas, en Belgique, en Allemagne et en République Tchèque.
  • Projet ANR Checkbound avec le LACL, le LAMSADE, le LIG, le LSV, l'INT et le PRISM sur le model-checking pour la « performability » et la sécurité des systèmes informatiques.
  • Nombreuses coopérations académiques avec Leipzig, Duisburg, Padova, Bordeaux, Milan etc.

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social