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.
Modalités pédagogiques : Cours magistraux et séances de travaux pratiques.
Règles du cours: La participation aux séances de travaux pratiques est obligatoire.
Il n'y a aucun manuel pour le cours. Toutefois, ce livre est recommandé pour les séances de travaux pratiques :
- Livre : ABRIAL J-R. The B-book: assigning programs to meanings. Cambridge University Press, 2005, 816p.
Aucun.
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.
Objectifs d'apprentissage :
- Modéliser et spécifier des systèmes et leurs propriétés,
- Raisonner sur des modèles pour établir la preuve de correction,
- Utiliser les outils pour mener la modélisation et la preuve,
- Implanter, analyser et évaluer les performances des outils et techniques étudiés dans divers domaines du traitement de la parole et des signaux audio.
Nombre d'Heures: 21.00, dont 3 séances de travaux pratiques.
Evaluation :
- Rapports de travaux pratiques (30 % de la note finale),
- Examen final (70 % de la note finale)
