Cours 2019-2020

Algèbres de processus [INFOM441]

  • 5 crédits
  • 30h+15h
  • 1er quadrimestre
Langue d'enseignement: Français
Enseignant: Jacquet Jean-Marie

Acquis d'apprentissage

L'utilité des sémantiques formelles comme modèles mathématiques servant de base à la compréhension et au raisonnement de programme est largement admise. Ce cours se propose d'étudier, dans le cadre de la programmation d'applications concurrentes et distribuées, les notions mathématiques, les techniques et les concepts qui les sous-tendent ainsi que les exemplifier au travers de l'étude d'applications (tels que certains protocoles de communication).

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 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.

Mode d'évaluation

L'examen consiste en deux parties: d'une part, l'exposé d'un article choisi par l'étudiant et, d'autre part, la résolution d'un exercice.

Sources, références et supports éventuels

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

Langue d'enseignement

Français

Lieu de l'activité

NAMUR

Faculté organisatrice

Faculté d'informatique
rue Grandgagnage 21
5000 NAMUR
T. 081725252
F. 081724967
secretariat.info@unamur.be

Cycle

Etudes de 2ème cycle