Intégrer La Prépa des INP
Intégrer une école
S'inscrire
Livret d'accueil
École / Prépa
ENSEIRB-MATMECA
Code interne
EIN9-IFON2
Description
Ce cours a pour but d'apprendre à utiliser la modélisation formelle comme outil de détection de bugs et de preuve de systèmes ou programmes informatiques.
Heures d'enseignement
- CICours Intégrés24h
- 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
| Type d'évaluation | Nature de l'évaluation | Durée (en minutes) | Nombre d'épreuves | Coefficient de l'évaluation | Note éliminatoire de l'évaluation | Remarques |
|---|
Seconde chance / Session de rattrapage
| Type d'évaluation | Nature de l'évaluation | Durée (en minutes) | Nombre d'épreuves | Coefficient de l'évaluation | Note éliminatoire de l'évaluation | Remarques |
|---|