| ||||
Sigle : INF6203 Gr. 01 Titre : Méthodes formelles pour le développement de logiciels Session : Hiver 2019 Horaire et local Professeur : Logrippo, Luigi | ||||
1. Description du cours paraissant à l'annuaire : | ||||
ObjectifsPermettre aux étudiants de maîtriser le processus de développement rigoureux et formel du logiciel. Lui permettre d’approfondir les techniques de spécification, validation et test formels du logiciel. ContenuSpécification et validation de besoins. Spécification de programmes séquentiels. Spécification de modules. Conception interne de modules et fonction d'abstraction. Étude et application de quelques langages formels. Spécification de programmes concurrents. Documentation produite à chaque étape du développement du logiciel. Étude et utilisation d’outils logiciels pour le développement formel du logiciel. Méthodes formelles de test. Méthodes formelles et méthodes informelles de validation de logiciels. | ||||
2. Objectifs spécifiques du cours : | ||||
Connaissance approfondie des principales méthodes de spécification, validation et tests formels des logiciels. Recherche spécialisée sur un sujet choisi en accord avec l’enseignant. Présentation de résultats. | ||||
3. Stratégies pédagogiques : | ||||
Cours magistral, avec présentations de projets d’étudiants. | ||||
4. Heures de disponibilité ou modalités pour rendez-vous : | ||||
Après chaque cours ou par rendez-vous. | ||||
5. Plan détaillé du cours sur 15 semaines : | ||||
Semaine | Thèmes | Dates | ||
1 |
Les méthodes formelles dans l’ingénierie du logiciel, leur développement historique, leur importance théorique et pratique, leur applicabilité. Présentation d’expériences récentes. |
08 jan. 2019 | ||
2 |
Les différents types de sémantique des langages de programmation. La logique comme langage formel pour la spécification et la validation des besoins et des programmes. Concepts de base de la logique formelle et de la théorie de la validation et preuve. |
15 jan. 2019 | ||
3 |
Spécification et validation formelle de programmes séquentiels. Validité partielle. |
22 jan. 2019 | ||
4 |
Exemples et cas d’étude de validation formelle de programmes séquentiels. Validité totale. |
29 jan. 2019 | ||
5 |
Spécification et preuve formelle de programmes concurrents. Protocoles de communication. |
05 fév. 2019 | ||
6 |
Exemples et cas d’étude de validation formelle de programmes concurrents et protocoles. |
12 fév. 2019 | ||
7 |
Présentations préliminaires de projets étudiants. |
19 fév. 2019 | ||
8 |
La vérification des modèles : Logique temporelle linéaire LTL. |
26 fév. 2019 | ||
9 |
Semaine d’études |
05 mars 2019 | ||
10 |
La vérification de modèles : logique temporelle à branchements CTL. |
12 mars 2019 | ||
11 |
Méthodes formelles de test et leur application : principes. |
19 mars 2019 | ||
12 |
Méthodes formelles de test et leur application : exemples. |
26 mars 2019 | ||
13 |
Les méthodes formelles dans le développement du logiciel. Aspects de documentation. Compléments et conclusions. |
02 avr. 2019 | ||
14 |
Présentations finales de projets étudiants. |
09 avr. 2019 | ||
15 |
Examen final |
16 avr. 2019 | ||
6. Évaluation du cours : | ||||
Rapport préliminaire et présentation préliminaire : 10 % Rapport final et présentation finale : 30 % Évaluation de vos présentations par vos collègues : 5 % Devoirs écrits : 15 % Examen final : 40 % | ||||
7. Politiques départementales et institutionnelles : | ||||
| ||||
8. Principales références : | ||||
M. Huth, M. Ryan. Logic in Computer Science 2nd edition. Cambridge University Press, 2014. Page Web : https://www.cs.bham.ac.uk/research/projects/lics/index.html J.-F. Monin. Introduction aux méthodes formelles. 2e édition. Eyrolles, 2000. Matériaux d’étude et notes de cours fournis dans Moodle. | ||||
9. Page Web du cours : | ||||
https://moodle.uqo.ca |