info459 - Spécification et vérification du logiciel

Nombre de crédits

5

Pré-requis

(Licence mention informatique)

Parcours

• optionnelle pour la mention informatique du master science

Objectifs

Comprendre comment améliorer la fiabilité et la qualité des programmes par :

• l'utilisation de spécifications ;
• la validation d'un programme vis à vis de sa spécification.

Mettre en pratique les notions acquises en utilisant essentiellement des outils existants de spécification et test pour Java.

Organisation

semaine

1

2

3

4

5

6

7

8

9

10

11

12

13

C (1h30)

×

×

×

×

×

×

×

×

×

×

×

×

TD (1h30)

×

×

×

×

×

×

×

×

×

×

×

×

TP (2h)

×

×

×

×

×

Volume de travail personnel étudiant estimé

environ 50h

Contrôle et validation des connaissances

• pour les UE sans TP : sup ( Ex, (2Ex + CC)/3)
• pour les UE avec TP obligatoires : (2TP + 3 sup(Ex, (2Ex + CC)/3))/5

Description du contenu

Spécification de programmes : programmation par contrats (Design By Contract) :

• principes : définition des différents types d'assertion
• application à UML (avec OCL) et Java (avec JML)

Validation de programmes :

• test de programmes :
  • principes et généralités
  • applications à Java : tests unitaires, tests fonctionnels, couverture de test, automatisation ...
• éventuellement utilisation de l'outil ESC-Java (spécifications JML)

Responsable(s)

Mirabelle Nebut, Arnaud Bailly

fichier source pour édition/modification