Membres – Publications

Cette équipe organise ses travaux de recherche autour de quatre grands axes de recherche :

Cet axe focalise ses recherches sur

1. la modélisation des systèmes complexes par des réseaux de files d’attente et des automates temporisés et/ou probabilistes, des méthodes de comparaison stochastique ou des solutions à forme-produit,
2. la spécification et la vérification de ces systèmes en utilisant des logiques temporelles et/ou probabilistes ou des logiques de premier ordre sur les réels, et
3. l’évaluation des performances, de dimensionnement et de qualité de service par simulation à événements discrets, appliquées à l’analyse des modèles de sûreté de fonctionnement.

Cet axe se concentre sur

1. l’étude et les applications de formalismes basés sur des algèbres de réseaux de Petri colorés (M-nets, S-nets, ABCD, . . .),
2. la conception et la réalisation de la mobilité d’agents en tant que principe de base d’une architecture logicielle, et
3. la modélisation, la spécification, la vérification et la synthèse des systèmes concurrents et multi-agents, en utilisant des modèles de jeux à information complète ou incomplète et à conditions de réussite généralisées et des combinaisons de logiques temporelles et épistémiques puissantes.

Les travaux de cet axe portent sur

1. la modélisation des exigences et leur utilisation pour la construction de spécifications formelles,
2. l’étude des combinaisons de paradigmes formels et graphiques, et
3. la modélisation formelle de politiques de contrôle d’accès dans les systèmes d’information.

Cet axe est orienté sur l’étude de la programmation data-parallèle de haut niveau, du point de vue des langages (en particulier le développement du langage de programmation de haut-niveau orienté fonctionnel appelé BSML), du lien sémantique-performance, de son adaptation aux nouvelles plate-formes matérielles (GPU, multi-coeurs, grappes dans le Cloud etc.), de la vérification de programmes BSP en utilisant la logique de Hoare ou CTL∗, et de leurs applications, en particulier le thème des masses de données autour du traitement en flux et en parallèle des requêtes sur documents XML.