Intégrer La Prépa des INP
Intégrer une école
S'inscrire
Livret d'accueil
Composante
ENSEIRB-MATMECA
Code interne
EI9IF311
Description
Spécification et modélisation formelles du logiciel. Le model-checking comme outil de preuve.
Heures d'enseignement
- CICours Intégré24h
- TITravaux Individuels24h
Pré-requis obligatoires
Automates finis, logique, algorithmes de graphes.
Syllabus
- 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
Bibliographie
Présentations et exercices (voir cours en ligne)
Modalités de contrôle des connaissances
Évaluation initiale / Session principale - Épreuves
| Type d'évaluation | Nature de l'épreuve | Durée (en minutes) | Nombre d'épreuves | Coefficient de l'épreuve | Note éliminatoire de l'épreuve | Remarques |
|---|---|---|---|---|---|---|
| Epreuve Terminale | Ecrit | 90 | 0.6 | sans document sans calculatrice | ||
| Contrôle Continu | Contrôle Continu | 0.4 |
Seconde chance / Session de rattrapage - Épreuves
| Type d'évaluation | Nature de l'épreuve | Durée (en minutes) | Nombre d'épreuves | Coefficient de l'épreuve | Note éliminatoire de l'épreuve | Remarques |
|---|---|---|---|---|---|---|
| Epreuve terminale | Oral | 30 | 0.6 | sans document sans calculatrice |