Systèmes de transition

Ce module introduit les fondements de la modélisation formelle des systèmes informatiques isolés/autonome à travers la notion de système de transitions, permettant de représenter rigoureusement leurs états et leurs exécutions. Les étudiants apprendront à spécifier les propriétés comportementales de ces systèmes au moyen de logiques temporelles, puis à analyser la relation de raffinement entre spécification abstraite et implantation concrète à l’aide du concept de module. L’ensemble de ces notions sera mis en pratique grâce à l’utilisation de l’outil TLA+, qui permettra de modéliser formellement des systèmes, d’exprimer leurs propriétés et de vérifier automatiquement leur conformité.

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

Logique. Automates. Systèmes Concurrents.