UE MVFA

Modélisation et Vérification Formelle par Automates

Objectifs

Ce cours 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.

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.

Responsable

Sophie Pinchinat (Sophie [dot] Pinchinatatirisa [dot] fr)