Cours 2019-2020

Vérification de modèles [INFOM471]

  • 5 crédits
  • 30h+15h
  • 1er quadrimestre
Langue d'enseignement: Français
Enseignant: Schobbens Pierre

Acquis d'apprentissage

Maitriser la construction de modèles et leurs techniques de vérification.

Contenu

Le cours théorique couvre les modèles par machines à états, l'expression de propriétés par des machines d'observation, la traduction de logique temporelle en machine d'observation.

En 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS).


Méthodes d'enseignement

Cours théorique + exercices en salle + travaux pratiques avec outil.

En 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS).

Mode d'évaluation

Examen oral y compris des exercices + evaluation du projet par un rapport (1/3 des points).

Sources, références et supports éventuels

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, The MIT Press (2008).

Plus pratique: Principles of the Spin Model Checker by M. Ben-Ari

The SPIN Model Checker: Primer and Reference by Gerard J. Holzmann

Systems and Software Verification: Model-Checking Techniques and Tools by B. Berard, M. Bidoit, A. Finkel, and F. Laroussinie

More theoretical: Model Checking by E. M. Clarke et al.

Langue d'enseignement

Français

Lieu de l'activité

NAMUR

Faculté organisatrice

Faculté d'informatique
rue Grandgagnage 21
5000 NAMUR
T. 081725252
F. 081724967
secretariat.info@unamur.be

Cycle

Etudes de 2ème cycle