Acquis d'apprentissage

  1. Maitriser les concepts permettant de comprendre et formaliser le comportement d'un système informatique.
  2. Maitriser la construction d'algorithmes permettant de répondre automatiquement à des questions (propriétés) sur ce comportement.
  3. Modéliser des systèmes informatiques réels sur base des acquis ci-dessus.
 
 
 

Objectifs

  1. Distinguer les différents types de propriétés: linéaires, branchantes, hyperpropriétés; propriétés de sûreté, de vivacité, d'équité; régulières, hors-contexte.
  2. Connaitres les automates finis à mots infinis :
    1. Automates de Büchi
    2. Automates de Rabin
    3. Automates à chaines de Rabin alias automates de parité
 
 

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.

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

(The numbers below refer to the pages in the book of Baier&Katoen)

  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

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

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.

 
 
 

Méthode d'évaluation

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.

Muhammad Atif, Jan Friso Groote: Understanding Behaviour of Distributed Systems Using mCRL. Springer 2023, ISBN 978-3-031-23007-3

 
 

Langue d'instruction