Systèmes de transition
- Langue d'enseignement : Français
- Méthode d'enseignement : En présence
- Code : N8EN08A
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
Outils Mathématiques pour l'Informatique. Systèmes Concurrents. Automates. Logique et raisonnement.
Session 1 ou session unique - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de transitions |
Session 2 - Contrôle des connaissances
| Modalité | Nature | Coefficient | Remarques |
|---|---|---|---|
| CT (contrôle terminal) | Oral/Ecrit | 100% | Examen Systèmes de transitions |
Contact(s)
QUEINNEC PHILIPPELieu(x)
- Toulouse
