Algèbres de processus [INFOM441]

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.

 

Disciplines

Enseignement des sciences de l'ingénieur
Analyse de systèmes informatiques
Informatique générale
Enseignement des sciences exactes et naturelles