Université du Québec en Outaouais Département d'informatique et d'ingénierie
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 :

Objectifs

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

Contenu

Spé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.

Descriptif – Annuaire

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