Modélisation et Vérification Formelle par Automates (MVFA)
Description
Cette UE fait partie du M1 informatique mais peut être suivie en M2, dans le cas où l'étudiant-e ne l'aurait pas suivi en M1.
Elle vise à former les étudiants à l'utilisation des méthodes de
model checking dont les fondements reposent sur la capacité à
modéliser les systèmes au moyen de systèmes de transitions et à
spécifier les propriétés à vérifier en logique temporelle. Ils
acquièrent aussi une compréhension profonde du fonctionnement des
model checkers qui reposent sur la correspondance entre logiques
temporelles et automates de mots infinis.
Mots-clés
Automates, logique
Prérequis
Connaissances de base en théorie des langages.
Contenu
- Modélisation des systèmes parallèles
- Propriétés du temps linéaire
- Propriétés régulières
- Logique du temps linéaire (LTL)
- Logique du temps arborescent (CTL)
- Model checking symbolique de CTL
- Compléments sur CTL et son extension CTL*
- Équivalences et abstractions
Des travaux pratiques consisteront à utiliser des model checkers classiques.
Compétences acquises
Les étudiants auront désormais la possibilité de recourir à des
preuves de corrections des systèmes qu'ils conçoivent sur la base de
méthodes formelles qui sont plus sûres que les méthodes de test car
elles permettent une vérification exhaustive que les derniers ne
peuvent garantir par nature.
Enseignant
Sophie Pinchinat