Courses/IMC

From LRDE

Titre

Introduction au Model checking

Sigle

IMC

Enseignant

Alexandre Duret-Lutz

Période

S5, Ing3

Public

Majeure, CSI

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