Cours 2020-2021

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.

A partir de 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS), et, si le temps le permet, l'outil UPPAAL pour les automates temporisés.

Table des matières

  1. System Verification 1

  2. Modelling Concurrent Systems 19

  3.   Linear-Time Properties 89

  4. Regular Properties 151

  5. Linear Temporal Logic 229

  6. Computation Tree Logic 313

  7. Timed Automata 673

     

 


Méthodes d'enseignement

Les modalités d'enseignement et d'évaluation des unités d'enseignement ont été rédigées en fonction de la situation à la rentrée académique 2020-2021. Cependant, ces modalités pourraient faire l'objet de modifications en fonction de l'évolution de la crise sanitaire liée à la covid-19. Les étudiants seront informés de toute modification de la situation générale (passage à l'enseignement à distance partiel ou complet) par les autorités de l'UNamur tandis que les modifications propres à chaque unité d'enseignement leur seront communiquées par les enseignants, via webcampus

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

A partir de 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS), et, si le temps le permet, l'outil UPPAAL pour les automates temporisés.

Mode d'évaluation

Les modalités d'enseignement et d'évaluation des unités d'enseignement ont été rédigées en fonction de la situation à la rentrée académique 2020-2021. Cependant, ces modalités pourraient faire l'objet de modifications en fonction de l'évolution de la crise sanitaire liée à la covid-19. Les étudiants seront informés de toute modification de la situation générale (passage à l'enseignement à distance partiel ou complet) par les autorités de l'UNamur tandis que les modifications propres à chaque unité d'enseignement leur seront communiquées par les enseignants, via webcampus

67% Examen oral à livre ouvert y compris des exercices

33% 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).

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

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