Partager cette page :
Discipline(s) : Infomatique et télécommunications

Principes du model checking

Semestre Semestre 1
Type Facultatif
Nature UE

Pré-requis

Connaissances de base en théorie des langages

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.

Contenu

Cours et travaux dirigés

  • 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
Travaux pratiques

Les travaux pratiques consisteront à utiliser deux model checkers classiques : SPIN et SMV

Contrôles des connaissances

Examen terminal et contrôle continu de travaux pratiques

Mise à jour le 12 avril 2018