Mobilité
Cours de recherche (24h de cours, travail
sur des articles scientifiques)
Cours : Daniel Hirschkoff (Daniel.Hirschkoff)
Présentation
Les développements récents de l'informatique en réseau à grande
échelle confrontent le domaine de l'analyse et de la vérification des
systèmes parallèles à des questions nouvelles et difficiles. Un
concept qui se trouve au coeur de cette évolution est celui de
mobilité (mobilité du code, et plus généralement du calcul, sur
un réseau dont la géométrie se reconfigure continuellement).
Ce cours présente des méthodes pour la description et l'analyse des
systèmes distribués et mobiles. L'objectif de ce type de démarche est
la compréhension de la sémantique de tels systèmes, qui peut être
utile pour la conception de langages de programmation et de
spécification, ainsi que pour la démonstration formelle de propriétés
portant sur ces systèmes.
On introduira des algèbres de processus pour la mobilité,
notamment le p-calcul et les Mobile Ambients, en présentant des
critères permettant d'évaluer les modèles (simplicité, expressivité,
encodages, enrichissements). On développera ensuite des techniques
pour raisonner sur ces modèles ou pour les adapter à des
problématiques spécifiques (systèmes de types, preuves de
bisimulation, logiques). On essaiera également d'illustrer comment cet
axe de recherche peut inspirer des travaux plus proches des
applications (conception de langages de programmation, systèmes pour
la preuve automatique ou interactive, analyse de questions liées à la
sécurité).
Thèmes abordés
- Modèles pour la mobilité
- algèbres de processus: p-calcul,
Mobile Ambients
- Évaluer le modèle
- questions d'expressivité, encodages,
variantes des calculs; langages de spécification et langages de
programmation.
- Exploiter le modèle -- raisonner sur les systèmes parallèles
-
équivalences comportementales, bisimulation, techniques de preuve;
systèmes de types; approche logique, logiques modales, logiques
spatiales.
- Mise en oeuvre
- vérification de systèmes parallèles et
approches automatiques; preuve interactive et représentation de la
mobilité; questions de sécurité, protocoles cryptographiques et
authentification, Spi-calcul, p-calcul et biologie.
Bibliographie