Composante
École Nationale Supérieure d'Électrotechnique d'Électronique d'Informatique d'Hydraulique et des Télécommunications
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.
Pré-requis obligatoires
Outils Mathématiques pour l'Informatique. Systèmes Concurrents. Automates. Logique et raisonnement.