A Descriptif des cours de niveau 2

1

A.1 Concurrence (C-2-03)

Responsables

Catuscia Palamidessi (INRIA Futurs), Roberto Amadio (PPS, Paris 7) et Jean-Jacques Levy (INRIA Rocquencourt).

Motivations et objectifs du cours

Ce cours est une introduction aux calculs de processus, c’est-à-dire à des systèmes formels qui permettent de raisonner sur les propriétés des programmes concurrents et possiblement répartis.

Les calculs de processus représentent à un niveau abstrait la création et l’exécution de processus et leurs mécanismes de synchronisation élémentaire : mémoire partagée, communication par canaux, etc. Ces calculs élémentaires sont, pour les processus concurrents, l’analogue du lambda calcul pour les programmes séquentiels.

Pendant le cours, nous donnerons des exemples d’application de ces formalismes à la conception de langages de programmation et à la spécification et vérification de systèmes répartis. Nous montrerons en outre quelques exemples récents de leur utilisation dans le traitement formel de problèmes de sécurité.

Plan du cours

1. Introduction et motivations (1h)

2. Calcul des Systèmes Communicants (CCS) (11h) – Syntaxe

– Sémantique Opérationnelle (SOS)

– Arbres de Synchronisation

– Traces

– Bisimulation Forte

– Bisimulation Faible

– Théorie de l’Egalité

– Logique Hennessy-Milner

– Model Checking

– Exemples de spécification et vérification en CCS

3. Le π-calcul (9h)

– Syntaxe

– Sémantique late et early

– Le π-calcul asynchrone

– Types

– Théorie de l’égalité

– Exemples de spécifications dans le π-calcul

– Autres approches à la mobilité

4. Calculs de processus probabilistes et applications (15h) – Expressivité des calculs. Rôle de la randomisation.

– Automates probabilistes et calculs de processus probabilistes.

– Application : solution randomisée de problèmes d’algorithmique répartie.

– Application : Confidentialité et Anonymat.

5. Notions avancées (12h) – Déterminisme et Confluence.

– Synchronie.

– Types et Ressources en Concurrence.

– Application à l’analyse du Flot d’Information

Pré-requis

Pas de pré-requis.

Bibliographie

[1] Robin Milner Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

[2] Robin Milner. The π-calculus. Cambridge University Press, 1999.

[3] Davide Sangiorgi and David Walker. The π-calculus : a Theory of Mobile Processes. Springer, 1991.

Intervenants possibles

Nom  Grade Établissement Laboratoire
R. Amadio  PR Paris 7  PPS
P.-L. Curien  PR Paris 7  PPS
E. Goubault  DR CEA  Saclay
J.-J. Lévy  DR INRIA  Rocquencourt
J. Leifer  CR INRIA  Rocquencourt
C. Palamidessi  DR INRIA  Futurs
F. Valencia  CR Paris 7  PPS
F. Zappa Nardelli CR INRIA  Rocquencourt