Module Sheet

FISE FISA

STI

Sécurité et Technologies Informatiques

Unité d'Enseignement :

Semestre : 7
Crédits ECTS : 6

Informatique Fondamentale

Code UE :

Elément Constitutif :

Coefficient : 1

Vérification formelle

Code EC :

Tronc Commun

L'UE Informatique Fondamentale : 5

Bases de données
Compilation
Modélisation et Théorie des graphes
Outils de déploiement de plateforme
Vérification formelle

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

Celene Link :

Lien vers ce module sur celene

Learning Objectives :

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

Program :

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

Evaluation Methods :

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.

Bibliographic References :

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