Formation d'ingénieurs RICM 2ème année
à Polytech'Grenoble
Filière Réseau & Communication
Ingéniérie des protocoles
  • Systèmes communiquants : sémantique, modèles d'exécution, concurrence, communication, synchronisation
  • Propriétés des systèmes : propriétés des états: atteignabilité, invariance ; propriété de traces: inclusion, équivalences
  • Techniques de vérification : preuves formelles en logique de Hoare, model-checking, abstraction, (bi)simulation

  • Modélisation : description de systèmes concurrents et de leurs propriétés
  • Étude de cas : Bakery protocol, Bit alterné, Sliding window, Diffusion atomique, Leader election (Lelann), Exclusion mutuelle auto-stabilisante (Disjktra)
  • Utilisation industrielle : présentation d'outils de vérification utilisés dans l'industrie

Fonctionnement

Chaque semaine
un cours + un exposé en TD + un DM
 
Le cour présente les résultats de 4 prix Turing sur la vérification de programmes: Floyd, Hoare, Pnueli, Clark-Emerson-Sifakis
Les travaux dirigés
Chaque semaine une étude de cas est présentée par deux étudiants
 
La présentation d'une application du cours à une étude de cas est aussi l'occasion d'apprendre à faire un exposé technique
Travail personnel
Terminer chaque étude de cas
 
Évaluation
Durée 2h00, sans document
 
mars : Devoir surveillé
mai : Examen
juin : Seconde session
Note finale
(1 Exposé + 1 DS + 2 Examen) / 4
 
Responsables IP : Laurent MOUNIER, Michaël PÉRIN