Programme d’études 2018-2019 | English | ||
Méthodes formelles pour la conception de systèmes : fondements | |||
Unité d’enseignement du programme de Master en sciences informatiques à la Faculté des Sciences |
Code | Type | Responsable | Coordonnées du service | Enseignant(s) |
---|---|---|---|---|
US-M1-SCINFO-067-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 | 40 | 15 | 5 | 0 | 0 | 6 | 6.00 | 1er quadrimestre |
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 | 30 | 15 | 5 | 0 | 0 | Q1 |
Unité d'enseignement |
---|
Objectifs par rapport aux acquis d'apprentissage du programme
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
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
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
Commentaire sur les évaluations rattr. Q1 de l'UE
Sans objet.
Types d'activités
AA | Types d'activités |
---|---|
S-MATH-043 |
|
S-MATH-051 |
|
Mode d'enseignement
AA | Mode d'enseignement |
---|---|
S-MATH-043 |
|
S-MATH-051 |
|
Supports principaux
AA | |
---|---|
S-MATH-043 | |
S-MATH-051 |
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. |
Supports complémentaires
AA | |
---|---|
S-MATH-043 | |
S-MATH-051 |
Supports complémentaires non reproductibles
AA | Support complémentaires non reproductibles |
---|---|
S-MATH-043 | Sans objet |
S-MATH-051 | 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. |