Sémantique de la Concurrence et de la Mobilité
sacc

Les problèmes de concurrence sont au coeur des systèmes informatiques modernes, en particulier les systèmes répartis (ex. www, pair-à-pair, jeux video) et les systèmes parallèles (ex. : grilles de calcul).

D’un point de vue théorique, nous étudions les formalismes permettant la spécification précise des systèmes concurrents ainsi que l’analyse formelle de leurs propriétés.

D’un point de vue pratique, les liens avec la programmation concurrente (ex. threads java) et la vérification automatique de modèle (model-checking) sont établis.

Dans une deuxième partie, nous abordons la problématique de mobilité, en particulier sous l’angle des réseaux mobiles ad-hoc, c’est-à-dire les systèmes dont l’infrastructure de communication évolue au cour du temps (déconnexion intempestives, reconnexions automatiques, etc.). Nous utilisons le Pi-calcul, extension de CCS adapté à la spécification de tels systèmes dynamiques.

Plan du cours

  1. Introduction à Micro-Pi, syntaxe formelle et sémantique informelle
  2. Sémantique opérationnelle structurée de Micro-Pi
  3. Equivalences comportementales (traces, bisimilarité)
  4. Passage de valeur et passage de nom
  5. Implémentation et outils (Travaux pratiques)
  6. Equivalences observationnelles (traces, bisimilarité faible)
  7. Logiques temporelles (mu-calcul modal)

Documents : Aller sur cette page

Mini-projets : Aller sur cette page

Annales : Aller sur cette page

Espace de discussion : Aller sur cette page

Bibliographie : Aller sur cette page