Se connecter
Logo

Fiche Module

FISE FISA

STI

Sécurité et Technologies Informatiques


Unité d'Enseignement :


Semestre : 7
Crédits ECTS : 6

Informatique Fondamentale

Elément Constitutif :


Coefficient : 1

Outils de preuve et vérification

Tronc Commun



L'UE Informatique Fondamentale : 5


Chaînes de Markov
Compilation
Fondements théoriques des bases de données
Modélisation et Théorie des graphes
Outils de preuve et vérification


Volume horaire : 21:20

Type Nombre Durée
Cours 8 01:20
TD 8 01:20


Evaluations : 1

Type Coefficient
Examen Final 1


Enseignants : 2

Enseignant Type
Hugot Vincent Responsable
Hugot Vincent Intervenant


Lien vers ce module sur celene


  • Maîtriser et comprendre une technique de vérification
  • Modéliser en logique les propriétés attendues d’un système.
Pré-requis :

UE Semestre Module
Principes de la programmation 5 Logique
Principes de la programmation 5 Théorie des Langages


  1. Modélisation de systèmes et structure de Kripke,
  2. Logique temporelle linéaire (LTL) et automates sur les mots infinis,
  3. Logiques temporelle arborescente (CTL) et calcul de point fixe.
  4. Implémentation et résolution en Python (en utilisant les outils fournis)

Examen final:

Document autorisé: Un feuille A4 R/V physiquement manuscrite individuelle.

Les documents produits sur tablette et imprimés sont acceptables uniquement si la densité d'information est similaire à ce qui aurait été obtenu avec papier et crayon.

Interros surprises / contrôle continu:

Toute séance de cours/TD/TP peut donner lieu à un contrôle noté. Absence non justifiée => 0/20.

  • Le polycopié : lien.

  • Schnoebelen, Philippe, "Vérification de logiciels : techniques et outils du model-checking", Vuibert


Compétences SecNumEdu:

Compétence Heures Cours Heures Pratique Niveau Entrée Niveau Sortie
Fondamentaux 4 4 0 1
Eléments de sûreté de fonctionnement du point de vue de l'analyse formelle: comprendre, exprimer, et formaliser absence de conflits critiques, famines, et autres propriétés de sûreté
Développement logiciel et ingénierie logicielle (sous l’angle de la sécurité) 4 4 0 2
Analyse formelle de programmes concurrents: modéliser des systèmes, exprimer des spécifications, et prouver des propriétés de sûreté et sécurité (Model-checking CTL, LTL)
Compétences :

Ref. Verbe Description Niveau
C1_1 reconnaître les problème modélisables 1
C1_1 calculer les comportements possibles du système 2
C1_2 décrire formellement le système 2
C2_1 prouver la correction d'un système 3