Systèmes de transition
- Code : N8AN02A
En bref
Objectifs
- Représenter formellement un système informatique isolé/autonome et ses exécutions à travers la notion de système de transitions.
- Spécifier les propriétés comportementales d'un tel système dans une logique temporelle.
- Comprendre la relation de raffinement entre spécification et implantation, à travers la notion de module.
- Utiliser un outil de modélisation formelle et de vérification automatique (TLA+) afin d'illustrer ces notions et de vérifier les propriétés des systèmes.
Description
- Systèmes de transitions. Traces et exécutions.
- Notion d'équité des exécutions.
- Spécification en logique(s) temporelle(s). Linear Temporal Logic et Computational Tree Logic.
- Introduction aux techniques de vérification de modèles.
Bibliographie
Specifying Systems (L. Lamport - Addison-Wesley)
Pré-requis nécessaires
- Automates
- Logique, Preuve de programme par induction
Session 1 ou session unique - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de Transit°, Mod.Cheking |
Session 2 - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de Transit°, Mod.Cheking |
