Programme d’études 2019-2020English
Méthodes formelles pour la conception de systèmes : fondements
Unité d’enseignement du programme de Master en sciences informatiques à la Faculté des Sciences
CodeTypeResponsable Coordonnées
du service
Enseignant(s)
US-M1-SCINFO-067-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çais401550066.001er quadrimestre

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

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

  • Avoir acquis des connaissances hautement spécialisées et intégrées et des compétences larges dans les diverses disciplines des sciences informatiques, qui font suite à celles relevant du niveau de bachelier en sciences informatiques
  • Gérer des projets de développement informatique d'envergure
    • -Etre capable d'appliquer, de mobiliser, d'articuler et de valoriser les connaissances et les compétences acquises en vue de contribuer à la conduite et à la réalisation d'un projet
    • -Etre capable de mener un projet à son terme en maîtrisant sa complexité et en tenant compte des objectifs, des ressources allouées et des contraintes qui le caractérisent
    • -Faire preuve d'autonomie et être capable de travailler seul ou en équipe
  • Gérer des travaux de recherche, de développement ou d'innovation
    • -Etre capable d'appréhender une problématique inédite relevant des sciences informatiques et de ses applications
    • -Pouvoir organiser et mener à son terme un travail de recherche, de développement ou d'innovation
    • -Rechercher de façon méthodique des informations scientifiquement valides, mener une analyse critique, proposer et argumenter des solutions éventuellement innovantes à des problématiques ciblées
  • Maîtriser les techniques de communication
    • -Pouvoir communiquer de façon claire, structurée et argumentée, tant à l'oral qu'à l'écrit, ses conclusions, ses propositions originales ainsi que les connaissances et principes sous-jacents
    • -Etre capable d'adapter sa communication à des publics divers
    • -Le cas échéant, être capable de communiquer dans une langue étrangère
  • Développer et intégrer un fort degré d'autonomie
    • -Etre capable d'acquérir seul de nouveaux savoirs
    • -Poursuivre sa formation et développer de nouvelles compétences de façon autonome
    • -Développer et intégrer un fort degré d'autonomie pour pouvoir évoluer dans de nouveaux contextes
  • Appliquer une méthodologie scientifique
    • -Avoir la capacité de mener une réflexion critique sur l'impact de l'informatique en général et, en particulier, lors de la contribution à des projets
    • -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, être capable d'approfondir ces concepts pour une utilisation réelle.

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.

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). <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 (80%), E2 (20%).

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'au Q1. 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

Mode d'enseignement

AAMode d'enseignement
S-MATH-043
  • Face à face
S-MATH-051
  • Face à face

Supports principaux

AA
S-MATH-043
S-MATH-051

Supports principaux non reproductibles

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

Supports complémentaires

AA
S-MATH-043
S-MATH-051

Supports complémentaires non reproductibles

AASupport complémentaires non reproductibles
S-MATH-043Sans objet
S-MATH-051Sans 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.
(*) 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 : 14/09/2019
20, place du Parc, B7000 Mons - Belgique
Tél: +32 (0)65 373111
Courriel: info.mons@umons.ac.be