Principles of Model Checking

Sophie Pinchinat

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.