Cours 2020-2021

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

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

Méthodes d'enseignement

Les modalités d'enseignement et d'évaluation des unités d'enseignement ont été rédigées en fonction de la situation à la rentrée académique 2020-2021. Cependant, ces modalités pourraient faire l'objet de modifications en fonction de l'évolution de la crise sanitaire liée à la covid-19. Les étudiants seront informés de toute modification de la situation générale (passage à l'enseignement à distance partiel ou complet) par les autorités de l'UNamur tandis que les modifications propres à chaque unité d'enseignement leur seront communiquées par les enseignants, via webcampus

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

Les modalités d'enseignement et d'évaluation des unités d'enseignement ont été rédigées en fonction de la situation à la rentrée académique 2020-2021. Cependant, ces modalités pourraient faire l'objet de modifications en fonction de l'évolution de la crise sanitaire liée à la covid-19. Les étudiants seront informés de toute modification de la situation générale (passage à l'enseignement à distance partiel ou complet) par les autorités de l'UNamur tandis que les modifications propres à chaque unité d'enseignement leur seront communiquées par les enseignants, via webcampus

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