Le but du cours est de fournir aux étudiants les outils qui peuvent aider à concevoir des systèmes logiciels ou matériels corrects. Le cours introduit les fondements théoriques de ces méthodes, facilitant le raisonnement et la preuve et introduit aussi l'utilisation pratique des outils associés.
Techniques d'enseignement et d'apprentissage : Leçons et séances de Travaux Pratiques (TPs).
Règles du cours: La participation aux TPs est obligatoire.
Bibliographie: Il n'y a aucun manuel pour le cours.
Livre recommandé pour les sessions de TPs:
«The B-book : assigning programs to meanings»
Abrial, Jean-Raymond ; Hoare, A ; Chapron, Pierre
Aucun prérequis. Ce cours est ouvert à tous les étudiants.
Modélisation et analyse formelles des systèmes : les étudiants apprendront les principes de base de la logique classique, le raisonnement déductif, des preuves de théorèmes, la théorie d'automates, la logique temporelle et la vérification de modèles.Utilisation pratique de méthodes formelles : les étudiants appliqueront les méthodes formelles à différents systèmes dans divers domaines pour prouver leurs corrections.
Résultats d'apprentissage :
- Modélisation et Spécification des systèmes et de leurs propriétés.
- Raisonnement sur des modèles pour établir la preuve de correction.
- Utilisation pratique d'outils pour mener la modélisation et la preuve.
Nombre d'Heures: 21.00, dont 3 séances de TPs.
Evaluation : TPs (30%), Examen final (70%)
