Syllabus 2014/2015
 
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.50
Évaluation :
S1: ET(1h30,E,sd,sc) x0.6 + CC x0.4; S2: ET(30m,O,sd,sc) x0.6 + rep(S1) x0.4   Détail de la nomenclature employée pour la création du code d'évaluation
Enseignant(s) :
HERBRETEAU Frédéric - Responsable
WALUKIEWICZ Igor
Partagé par l'UE (les UEs) :
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)
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/