Programme d’études 2024-2025English
Projet en méthodes formelles pour la conception de systèmes (Liste A)
Unité d’enseignement du programme de Master en sciences mathématiques (MONS) (Horaire jour) à la Faculté des Sciences

CodeTypeResponsable Coordonnées
du service
Enseignant(s)
US-M1-SCMATH-048-MUE optionnelleRANDOUR MickaëlS820 - Mathématiques effectives
  • RANDOUR Mickaël

Langue
d’enseignement
Langue
d’évaluation
HT(*) HTPE(*) HTPS(*) HR(*) HD(*) CréditsPondération Période
d’enseignement
  • Français
Français301872001212.00Année

Code(s) d’AAActivité(s) d’apprentissage (AA) HT(*) HTPE(*) HTPS(*) HR(*) HD(*) Période
d’enseignement
Pondération
S-MATH-043Méthodes formelles : Introduction100000Q1
S-MATH-051Méthodes formelles : Fondements20181200Q1
S-MATH-056Méthodes formelles : Applications006000Q2

Note globale : les évaluations de chaque AA donnent lieu à une note globale pour l'unité d'enseignement.
Unité d'enseignement

Objectifs par rapport aux acquis d'apprentissage du programme

  • Posséder des connaissances mathématiques intégrées et pointues
    • -Pouvoir mobiliser les mathématiques de bachelier pour traiter de questions complexes et posséder une expertise profonde de celles-ci, prolongeant celle développée en bachelier.
    • -Être capable d'utiliser ses connaissances antérieures pour apprendre des mathématiques de haut niveau de manière autonome.
    • -Être à même de rechercher la littérature mathématique de manière efficace et pertinente.
    • -Être capable de lire des articles de recherche dans au moins une discipline des mathématiques
  • Être capable de réaliser des projets d'envergure
    • -Avoir l'autonomie nécessaire pour mener à bien un projet d'envergure lié aux mathématiques ou à leurs applications. Ceci implique de pouvoir prendre en compte la complexité du projet, ses objectifs et les ressources disponibles pour le réaliser.
    • -Porter une critique constructive sur la qualité et l'état d'avancement d'un projet.
    • -Être capable de travailler en équipe et en particulier de communiquer efficacement et dans le respect des autres.
    • -Être capable d'utiliser les ressources bibliographiques de manière adaptée au but poursuivi.
    • -Pouvoir présenter oralement et par écrit les objectifs et les résultats d'un projet.
  • Être capable d'innovation pour résoudre une problématique inédite en mathématiques ou dans leurs applications
    • -Pouvoir mobiliser ses connaissances, rechercher et analyser diverses sources d'information afin de proposer des solutions éventuellement innovantes à des problématiques inédites ciblées.
    • -Pouvoir faire usage de l'outil informatique de manière appropriée, au besoin en développant un petit programme.
  • Pouvoir communiquer clairement
    • -Pouvoir communiquer oralement et par écrit des résultats de mathématique ou de domaines connexes en s'adaptant au public.
    • -Être capable de faire une présentation structurée et argumentée du contenu et des principes sous-tendant un travail, des connaissances mobilisées et des conclusions auxquelles il conduit.
    • -Posséder une connaissance suffisante de l'anglais pour une communication scientifique de base.
  • Être capable de s'adapter à différents contextes
    • -Avoir développé un fort degré d'autonomie permettant d'acquérir des savoirs complémentaires et des compétences nouvelles, permettant d'évoluer dans des contextes différents.
    • -Être capable de mener une réflexion critique sur l'impact des mathématiques et sur les implications des projets auxquels ils contribuent
    • -Faire preuve de rigueur, d'autonomie, de créativité, d'honnêteté intellectuelle, de sens éthique et déontologique

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ême 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ême règles qu'aux Q1/Q2. Toute évaluation en-dessous de 10 doit être repassée au Q3.

Types d'activités

AATypes d'activités
S-MATH-043
  • Cours magistraux
S-MATH-051
  • Cours magistraux
  • Exercices dirigés
  • Utilisation de logiciels
  • Démonstrations
  • Préparations, travaux, recherches d'information
S-MATH-056
  • Préparations, travaux, recherches d'information

Mode d'enseignement

AAMode d'enseignement
S-MATH-043
  • En présentiel
S-MATH-051
  • En présentiel
S-MATH-056
  • En présentiel

Supports principaux non reproductibles

AASupports principaux non reproductibles
S-MATH-043Supports principaux disponibles sur Moodle.
S-MATH-051Supports principaux disponibles sur Moodle.
S-MATH-056Supports principaux disponibles sur Moodle.

Supports complémentaires non reproductibles

AASupport complémentaires non reproductibles
S-MATH-043Sans objet.
S-MATH-051Sans objet.
S-MATH-056Sans objet.

Autres références conseillées

AAAutres références conseillées
S-MATH-043C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
S-MATH-051C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
S-MATH-056C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
(*) HT : Heures théoriques - HTPE : Heures de travaux pratiques encadrés - HTPS : Heures de travaux pratiques supervisés - HD : Heures diverses - HR : Heures de remédiation - Dans la colonne Pér. (Période), A=Année, Q1=1er quadrimestre et Q2=2e quadrimestre
Date de dernière mise à jour de la fiche ECTS par l'enseignant : 25/04/2024
Date de dernière génération automatique de la page : 07/12/2024
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111
Courriel: info.mons@umons.ac.be