Acquis d'apprentissage

L'utilité des sémantiques formelles comme modèles servant de base à la compréhension et au raisonnement de programmes est largement admise. Parmi ces sémantiques, les algèbres de processus constituent une théorie largement utilisée. Au terme du cours, l'étudiant maîtrisera les concepts et techniques de base des algèbres de processus et sera capable de les appliquer pour modéliser et raisonner sur des applications concurrentes et distribuées.

Par ailleurs, l'étudiant sera amené durant le cours à modéliser différents problèmes, ce qui le forcera à développer deux soft skills : la créativité et la résolution de problèmes.

 

Objectifs

L'objectif du cours est d'exposer les concepts et techniques de base des algèbres de processus, une théorie largement utilisée pour modéliser et raisonner sur des applications concurrentes et distribuées.

Contenu

Le cours est axé sur l'étude d'algèbres de processus concurrents communicants sur base de deux différentes sémantiques: (i) les sémantiques opérationnelles décrivant les exécutions de programmes en termes de transitions et (ii) les sémantiques algébriques décrivant les exécutions par le biais d'égalités.

Plus concrètement le cours développe progressivement une famille d'algèbre de processus. Il débute par une algèbre formée d'actions de base, composées séquentiellement ainsi que par un opérateur de choix non déterministe. Bien que simple cette algèbre permet déjà de mettre en évidence une série de concepts, telles que l'équivalence de processus, les traces, la bi-simulation, et de compléter leur caractérisation opérationnelle par une caractérisation basée sur des équations algébriques. Le cours intègre ensuite dans cette algèbre de base différents mécanismes comme la composition parallèle, l'abstraction, l'encapsulation ou encore les descriptions récursives. On montre que ces extensions sont conservatives, en particulier en ce qui concerne la caractérisation algébrique.

Le cours met l'accent sur les applications et l'utilisation d'outils. On montre ainsi comment les protocoles de communication peuvent être décrits et analysés par les algèbres de processus. Dans ce cadre, le cours introduit la logique de Hennessy-Milner ainsi que l'outil mcrl. De nombreux exemples d'applications sont proposées dans le cours allant du domaine des télécommunications à celui de la sécurité en passant par la modélisation de systèmes concurrents simples.

 

Méthodes d'enseignement

Le cours est organisé en une série d'exposés ex-cathedra couplés à une série de séance de travaux pratiques. La théorie est enseignée aux cours et est exemplifiée par des exercices. L'accent est ainsi mis sur les concepts et leurs applications. Les séances d'exercices pratiques permettent d'illustrer la théorie dans le cadre d'autres exercices et applications ainsi que d'utiliser des outils et d'approfondir les langages CCS et CSP.

Méthode d'évaluation

L'examen consiste en deux parties: d'une part, l'exposé d'un article choisi par l'étudiant ou d'un travail réalisé par l'étudiant et, d'autre part, la résolution d'un exercice mettant en oeuvre la théorie vue au cours.

Sources, références et supports éventuels

Wan Fokkink, Introduction to Process Algebra, Springer-Verlag, 1999.

Langue d'instruction