Programme d’études 2018-2019English
Projet en méthodes formelles pour la conception de systèmes
Unité d’enseignement du programme de Master en sciences mathématiques à 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çais401565001212.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 : Fondements3015500Q1
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 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

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.

Types d'évaluations Q1 pour l'UE

  • Présentation et/ou travaux
  • Examen oral

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

Types d'évaluations Q2 pour l'UE

  • Présentation et/ou travaux
  • Examen oral

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). <b>Note finale de l'UE. </b>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%).

Types d'évaluation Q3 pour l'UE

  • Présentation et/ou travaux
  • Examen oral

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.

Types d'évaluation rattrapage BAB1 (Q1) pour l'UE

  • Néant

Commentaire sur les évaluations rattr. Q1 de l'UE

Sans objet.

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
  • Face à face
S-MATH-051
  • Face à face
S-MATH-056
  • Face à face

Supports principaux

AA
S-MATH-043
S-MATH-051
S-MATH-056

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

AA
S-MATH-043
S-MATH-051
S-MATH-056

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 génération : 02/05/2019
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111
Courriel: info.mons@umons.ac.be