Titre
|
Introduction au Model checking
|
Sigle
|
IMC
|
Enseignant
|
Alexandre Duret-Lutz
|
Période
|
S5, Ing3
|
Public
|
Majeure, RDI
|
Contrôle
|
QCM
|
Durée
|
14h
|
Optionnel
|
non
|
Module
|
Sciences Générales
|
Prérequis
|
ALGO
|
Objectifs
|
Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets.
|
Plan
|
- Introduction de la vérification formelle et du model checking* Diagrammes de décision binaires (BDD)* Logique temporelle à temps arborescent (CTL) et vérification à l'aide de BDD* Diagrammes de décision hiérarchiques (SDD)* Logique temporelle à temps linéaire (LTL) et passage vers les automates de Büchi* Test de vacuité d'un automate de Büchi* Lutte contre l'explosion combinatoire de l'espace d'état* Hypothèses d'équité et automates de Streett* Introduction à Spin.
|
Documentation
|
- Model Checking. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. MIT Press.
- The Spin Model Checker: Primer and Reference Manual. Gerard J. Holzmann. Addison-Wesley.
|
Support
|
|
Journaux
|
|