 | Programme d’études 2025-2026 | English | |
 | Projet en méthodes formelles | ||
Unité d’enseignement du programme de Master en enseignement section 4 : mathématiques (MONS) (Horaire jour) à l"Ecole de Formation des Enseignants |
| Code | Type | Responsable | Coordonnées du service | Enseignant(s) |
|---|---|---|---|---|
| UF-M1-MEMAT4-015-M | UE optionnelle | RANDOUR Mickaël | S820 - Mathématiques effectives |
|
| Langue d’enseignement | Langue d’évaluation | HT(*) | HTPE(*) | HTPS(*) | HR(*) | HD(*) | Crédits | Pondération | Période d’enseignement |
|---|---|---|---|---|---|---|---|---|---|
| Français | 30 | 18 | 72 | 0 | 0 | 10 | 10.00 | Année |
| Code(s) d’AA | Activité(s) d’apprentissage (AA) | HT(*) | HTPE(*) | HTPS(*) | HR(*) | HD(*) | Période d’enseignement | Pondération |
|---|---|---|---|---|---|---|---|---|
| S-MATH-043 | Méthodes formelles : Introduction | 10 | 0 | 0 | 0 | 0 | Q1 | |
| S-MATH-051 | Méthodes formelles : Fondements | 20 | 18 | 12 | 0 | 0 | Q1 | |
| S-MATH-056 | Méthodes formelles : Applications | 0 | 0 | 60 | 0 | 0 | Q2 |
| Unité d'enseignement |
|---|
Objectifs par rapport aux acquis d'apprentissage du programme
- Les compétences de l'organisateur et accompagnateur d'apprentissages dans une dynamique évolutive.
- Maitriser les contenus disciplinaires, leurs fondements épistémologiques, leur évolution scientifique et technologique, leur didactique et la méthodologie de leur enseignement
Acquis d'apprentissage de l'UE
Comprendre en profondeur les concepts fondateurs des méthodes formelles, maîtriser leurs fondements mathématiques, savoir les mettre en pratique dans des cas concrets à l'aide d'outils logiciels, pouvoir intégrer les méthodes formelles dans un processus de développement logiciel, être capable d'aborder des travaux avancés dans le domaine.
Contenu de l'UE : descriptif et cohérence pédagogique
Théorie : Introduction aux méthodes formelles, Modélisation de systèmes, Linear temporal logic, Computation tree logic, Model checking symbolique, Vérification de systèmes probabilistes (et quantitatifs), Synthèse de systèmes probabilistes (et quantitatifs), Synthèse via la théorie des jeux. Présentations d'outils logiciels par les étudiants. Lecture et présentation de travaux avancés en vérification et synthèse de systèmes informatiques. Projet : conception d'un système à l'aide de méthodes formelles.
Compétences préalables
Notions de base d'algorithmique, programmation, complexité, logique.
Type(s) et mode(s) d'évaluation Q1 pour l'UE
- Examen oral - En présentiel
- Présentation orale - En présentiel
Commentaire sur les évaluations Q1 de l'UE
Examen oral sur la théorie et les exercices (Evaluation E1). Présentation d'outils par les étudiants (Evaluation E2).
Méthode de calcul de la note globale pour l'évaluation Q1 de l'UE
Evaluations individuelles uniquement. Note globale au Q2.
Type(s) et mode(s) d'évaluation rattrapage Q1 (BAB1) pour l'UE
- Néant - Néant
Commentaire sur les évaluations rattrapage Q1 (BAB1) de l'UE
Sans objet.
Méthode de calcul de la note globale pour l'évaluation rattrapage Q1 (BAB1) de l'UE
Sans objet.
Type(s) et mode(s) d'évaluations Q2 pour l'UE
- Production (travail écrit, rapport, essai, collection, produit…) à déposer - En présentiel
- Examen oral - En présentiel
- Présentation orale - En présentiel
- Epreuve pratique - En présentiel
Commentaire sur les évaluations Q2 de l'UE
Présentations de travaux avancés sur base d'articles ou de livres (Evaluation E3). Projet (potentiellement en groupe) (Evaluation E4). Note finale de l'UE. Si une des évaluations est inférieure à 8, la note finale est égale à l'évaluation minimale. Sinon, la pondération suivante est appliquée : E1 (40%), E2 (10%), E3 (20%), E4 (30%).
Méthode de calcul de la note globale pour l'évaluation Q2 de l'UE
Présentations de travaux avancés sur base d'articles ou de livres (Evaluation E3). Projet (potentiellement en groupe) (Evaluation E4). Note finale de l'UE. Si une des évaluations est inférieure à 8, la note finale est égale à l'évaluation minimale. Sinon, la pondération suivante est appliquée : E1 (40%), E2 (10%), E3 (20%), E4 (30%).
Type(s) et mode(s) d'évaluations Q3 pour l'UE
- Production (travail écrit, rapport, essai, collection, produit…) à déposer - En présentiel
- Examen oral - En présentiel
- Présentation orale - En présentiel
- Epreuve pratique - En présentiel
Commentaire sur les évaluations Q3 de l'UE
Mêmes règles qu'aux Q1/Q2. Toute évaluation en-dessous de 10 doit être repassée au Q3.
Méthode de calcul de la note globale pour l'évaluation Q3 de l'UE
Mêmes règles qu'aux Q1/Q2. Toute évaluation en-dessous de 10 doit être repassée au Q3.
Types d'activités
| AA | Types d'activités |
|---|---|
| S-MATH-043 |
|
| S-MATH-051 |
|
| S-MATH-056 |
|
Mode d'enseignement
| AA | Mode d'enseignement |
|---|---|
| S-MATH-043 |
|
| S-MATH-051 |
|
| S-MATH-056 |
|
Supports principaux non reproductibles
| AA | Supports principaux non reproductibles |
|---|---|
| S-MATH-043 | Supports principaux disponibles sur Moodle. |
| S-MATH-051 | Supports principaux disponibles sur Moodle. |
| S-MATH-056 | Supports principaux disponibles sur Moodle. |
Supports complémentaires non reproductibles
| AA | Support complémentaires non reproductibles |
|---|---|
| S-MATH-043 | Sans objet. |
| S-MATH-051 | Sans objet. |
| S-MATH-056 | Sans objet. |
Autres références conseillées
| AA | Autres références conseillées |
|---|---|
| S-MATH-043 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |
| S-MATH-051 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |
| S-MATH-056 | C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. |