Ecole d'ingénieur et centre de recherche en Sciences du numérique

Formal/methods-Spécification et Vérification formelles des systèmes

[FormalMet]
T Enseignement Technique


Résumé

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

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

Préalable Requis

Aucun prérequis. Ce cours est ouvert à tous les étudiants.

Description

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%)

Nombre d'heures: 21.00
Nombre d'heures par semaine: 3.00