====== Modélisation et spécification (M2) ======


===== Description =====

Ce cours aborde d'une part la construction de modèles formels pour la description du comportement des systèmes informatiques et d'autre part la construction de spécifications (les propriétés attendues) de ces systèmes. 

===== Syllabus =====
==== Sujets centraux ====



  - Modélisation
    * Les systèmes de transitions étiquetés 
    * La composition parallèle
    * Les réseaux de Petri
  - Spécification
    * Logique temporelle LTL 
    * Exemples de propriétés
    * Algorithmes de décision
    * Logique temporelle CTL 
    * Exemples et algorithmes
    * Comparaison d'expressivité
  - Utilisation d'outils de model-checking (PRISM, NuSMV,...)


===== Pré-requis =====

  - Bonne maîtrise de la logique propositionnelle 
  - Automates finis 
  - Algorithmique dans les graphes