Établissement
INP - ENSEEIHT
Description
La matière est composée de 5 cours magistraux, 5 TD et 5 TP. La matière est évaluée par un examen écrit. Les concepts abordés sont :
- Systèmes de transitions. Traces et exécutions.
- Notion d'équité des exécutions.
- Spécification en logique(s) temporelle(s). Linear Temporal Logic et Computational Tree Logic.
- Introduction aux techniques de vérification de modèles.
Contenu détaillé des séances :
C1 : Définition des systèmes de transitions
C2 : Notion d'équité
C3 : LTL
C4 : CTL
C5 : Vérification par model checking de CTL et LTL + Démonstraion TLAPS
CTD1 et CTD2 : TLA+ actions
CTD3 : TLA+ logique
TD4 et TD5 : modélisation d'algorithmes distribués (Peterson, Jeton circulant, philosophes, allocateur de ressources,...)
TP1 : Résolution de problème (par exemple problème des missionnaires et des cannibales)
TP2 à TP5 : modélisation d'algorithmes distribués (Peterson, Jeton circulant, philosophes, allocateur de ressources,...)