FR
EN
Vérification formelleEA Sécurité Fondamentale (STI)
Vérification formelle
Unité d'enseignement Informatique Fondamentale · AS07_IF1 | Code EC AS07_IF1-6
7ECTS (UE)
1Coefficient
21:20Heures
Séquencement
Objectifs pédagogiques
- Maîtriser et comprendre une technique de vérification
- Modéliser en logique les propriétés attendues d’un système.
Pré-requis
| Module | Unité d'enseignement | Semestre |
|---|---|---|
| Logique | Principes de la programmation | S5 |
| Théorie des Langages | Principes de la programmation | S5 |
Programme
- 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)
Modalités d'évaluation
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.
Références bibliographiques
-
Le polycopié : lien.
-
Schnoebelen, Philippe, "Vérification de logiciels : techniques et outils du model-checking", Vuibert
Compétences
4| Réf. | 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 |
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) | ||||