Syllabus 2012/2013
 
Extrait PDF Anglais
 Français
 index
Module : IF311
Titre :
Conception formelle
Volumes horaires :
Cours Intégré : 24.00 h
Travail Individuel : 24.00 h
Crédits ECTS :
2.00
Enseignant(s) :
HERBRETEAU Frédéric - Responsable
WALUKIEWICZ Igor
Niveau :
module de troisième année
Résumé :
Spécification et modélisation formelles du logiciel. Le model-checking comme outil de preuve.
Plan :
    • Introduction aux enjeux des logiciels critiques
    • Modélisation formelle: systèmes de transitions et langage de haut niveau PlusCal
    • Spécification formelle en Logique Temporelle Linéaire (LTL)
    • Spécification avancée en TLA+
    • Modélisation des systèmes concurrents: atomicité et équité
    • Algorithmes de model-checking
    • Abstraction et raffinement

      Exercices basés sur la plateforme TLA/TLC de Leslie Lamport
Prérequis :
    • Automates finis (IF114)
    • Logique, preuve de programmes (IF105)
Évaluation :
Projet + soutenance en anglais
Document(s) :
Distribué en séance
Mot(s) clé(s) :
Spécification, Modélisation, Vérification, Conception formelle
Cours en ligne :
http://www.enseirb.fr/~herbrete/IF311/