Lifo - Laboratoire d'Informatique Fondamentale d'orléans Université d'Orléans université d'Orléans ENSI Bourges ENSI Bourges

Lifo > PaMDA : ProgrAmmation, Modélisation et vérification D'Applications parallèles et distribuées

 English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Tel: +33 (0)2 38 41 70 11
Fax: +33 (0)2 38 41 71 37



PaMDA : ProgrAmmation, Modélisation et vérification D'Applications parallèles et distribuées

Professeur

Maître de Conférences HDR

Maître de Conférences

Doctorant

Correspondant

Professeur Emerite

Chercheur - autre statut


Accéder à la page web de l'équipe

L'équipe PaMDA s'intéresse à l'ensemble de toutes les étapes de conception et de développement d'applications parallèles et/ou distribuées. Elle s'intéresse donc à la modélisation d'applications (ou de systèmes) parallèles et distribués  en vue de fournir des outils pour aider à leur conception et leur programmation mais aussi à  l'évaluation de leurs performances et à la vérification de leurs propriétés. Les travaux menés au sein de l'équipe portent à la fois sur

  • les formalismes de modélisation des applications afin d'une part de permettre le développement d'applications parallèles et/ou réparties sûres, de vérifier le comportement de telles applications vis à vis de propriétés attendues que ce soit en termes de sûreté de fonctionnement, de validité des résultats ou de la performance,
  • les applications concrètes de ces outils dans des domaines tels que le calcul scientifique ou la visualisation scientifique interactive.

Les recherches de l'équipe sont articulées autour de deux axes principaux:

Parallélisme structuré

Cet axe s'inscrit dans un objectif général de conception d'outils et d'environnements pour le développement et l'analyse de programmes structurés pour architectures haute performance à mémoire partagée, répartie et architectures infonuagiques. Il comprend:

  • la conception et l'implantation de bibliothèques et langages pour le parallélisme structuré,
  • la vérification (par construction, ou a posteriori) de programmes, bibliothèques et compilateurs pour le parallélisme structuré,
  • l'analyse statique (vérification de propriétés, analyse de performances) de programmes parallèles,
  • la conception et l'implantation d'algorithmes parallèles pour le traitement de masses de données.

Applications distribuées et systèmes répartis

Les travaux de cet axe portent sur les outils et modèles permettant de modéliser des systèmes distribués (ou répartis). Ces modèles sont appliqués à la vérification de systèmes répartis et à la compositio (semi)-automatique d'applications distribuées (services web, applications à base de composants). Cet axe développe des recherches notamment sur

  • des outils logiques pour la modelisation et la vérification de systèmes distribués en se basant notamment sur des formalismes à base de réécriture, d'automates ou de langage d'arbres,
  • la conception de procédures de décision (ou de semi décision) permettant de vérifier des propriétés sur le comportement des systèmes modélisés,
  • la conception d'outils pour faciliter voire automatiser la composition d'applications réparties devant vérifier certaines propriétés,
  • la vérification et évolution de contraintes sur des documents XML.

Logiciels

  • BSML : bibliothèque pour la programmation parallèle BSP extensible et déclarative.
  • SyDPaCC : un environnement pour le développement systématique de programmes parallèles avec l'assistant de preuve Coq.
  • Vitamins : un framework dédié à la construction d'applications modulaires pour l'analyse et la visualisation interactive d'une dynamique moléculaire en post traitement ou au cours d'une simulation.
  • XMLCorrector : l'implantation d'un algorithme permettant la correction d'un document XML par rapport à un schéma exprimé sous la forme d'une DTD. 

Actions de recherche en cours