Cours 2017-2018

Approches sémantiques [INFOM441]

  • 4 crédits
  • 30h+15h
  • 2e 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 différentes sémantiques: (i) les sémantiques opérationnelles décrivant les exécutions de programmes en termes (abstraits) d'exécutions sur une machine abstraite, (ii) les sémantique dénotationnelles décrivant les programmes d'une façon compositionnelle et sur base de structures mathématiques riches telles que les treillis complets ou les espaces métriques complets, (iii) les sémantiques axiomatiques caractérisant les mécanismes de programmation au moyen de règles d'une théorie de preuve d'une certaine logique et (iv) 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égère 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.

 


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