Semestre 8 – Option – Vérification de systèmes

Objectifs

L’objectif de ce cours est d’introduire la problématique de la vérification logicielle et de l’expérimenter par l’utilisation d’outils. Les étudiants devront être capables de mettre en œuvre les notions acquises dans la modélisation d’un système concret et sa vérification à l’aide d’un des outils présentés.

Prérequis

Voir la description des prérequis du M1.

Contenu pédagogique de l’UE

  • Vérification de systèmes temporisés
    • modèle et propriétés
    • l’outil UppAal
    • vérifier des propriétés complexes avec UppAal
  • Vérification de systèmes probabilistes :
    • modèle et propriétés
    • l’outil PRISM
    • complémentarité des vérifications numérique et statistique