Vous êtes ici : FIL > Portail > Master Informatique > M1S2 > SVL

Spécification et Validation du Logiciel - SVL

Cette option se déroule au S6 du Master 1 informatique.

Intervenants

Mirabelle Nebut

Volume horaire

L'unité comporte une séance de cours-TD hebdomadaire de 1h30 et une séance de TD-machine hebdomadaire de 2h.

Pré-requis

Pour apprécier cette UE, un attrait pour la conception OO du logiciel et pour les aspects formels de l'informatique est souhaitée. Si le pattern d'injection des dépendances (pour le test) ou les formules logiques (pour les méthodes formelles) vous donnent de l'urticaire, il vaut mieux choisir une autre option (même si vous pensez faire plus tard un master IAGL).

Compétences requises:

  • pour la partie test : la programmation et des notions de conception objet (la connaissance de Python n'est pas requise).
  • pour la partie approches formelles : les bases de la théorie des ensembles et de la logique du premier ordre.

Crédits

5 ECTS
Mirabelle Nebut
dernière modification : 26/11/2016 à 17:05:03

Objectifs

L'UE vise à sensibiliser les étudiants aux méthodes permettant de développer des programmes fiables et de qualité. L'UE se décompose en 2 parties de 6 semaines, au contenu volontairement très différent:
  • test unitaire du logiciel;
  • approche formelle pour la vérification de modèles du logiciel.
On commencera d'abord par le test (plus intuitif et proche de ce que les étudiants connaissent) avant de passer au formel (nettement plus dépaysant):
  • le test du logiciel, indispensable en entreprise, fait partie de la sphère quotidienne du développeur : pas de logiciel de qualité sans suites de test qui passent ! La pratique du test est une école de la rigueur, qui oblige à repenser les processus de développement, et produit des applications testables donc mieux conçues, et testées donc plus fiables;
  • les méthodes formelles de validation du logiciel sont beaucoup moins utilisées au quotidien que le test. Certaines (comme le model-checking) sont le plus souvent réservées aux applications critiques ou spécifiques, comme les protocoles de communication. D'autres s'appliquent à la conception et au développement du logiciel mais effraient les concepteurs et les développeurs à cause du formalisme qui nécessite un apprentissage. En tout état de cause il est utile d'en avoir entendu parler pour savoir quoi en attendre.

Contenu

Test

Le contenu de cette partie sera modulé en fonction des compétences préalables des étudiants participant au module.

L'UE présente différents aspects du test de programmes : place et importance du test dans le développement logiciel, automatisation des tests, stratégies de test unitaire, notion de couverture de test, test d'acceptation. On insiste sur les méthodes de développement "pensez au test en premier" en pratiquant le Test Driven Development.

On utilisera le langage Python mais les principes (méthodes, outillage) présentés dans l'UE valent pour n'importe quel langage de programmation objet. La connaissance de Python n'est pas un pré-requis (il suffit de maîtriser un langage objet), par contre un attrait pour la conception 00 du logiciel est souhaitable. Le travail personnel portera principalement sur la pratique : en plus des TPs d'apprentissage, les étudiants seront fortement incités à réutiliser leurs compétences dans les autres UEs et projets du semestre.

À l'issue de l'UE, les étudiants doivent:

  • être conscients de la nécessité de tester le code qu'ils écrivent, quel que soit son contexte;
  • pouvoir discuter des intérêts de l'approche dirigée par les tests (TDD), savoir spécifier un programme par ses tests;
  • connaître les concepts du test unitaire/d'interaction, être capables d'utiliser une bibliothèque dédiée pour un langage objet;
  • connaître quelques critères de couverture de code, être conscients de leurs limites, être capables d'utiliser une bibliothèque de calcul de couverture;
  • savoir appliquer la notion de test aux limites;
  • connaître les principes du test d'acceptation, savoir utiliser un outil de test d'acceptation pour application web;
  • être conscients des limites intrinsèques du test.

On utilisera tout ou partie des outils suivants: unittest et nose pour les tests unitaires, sphinx et doctest pour la documentation, mockito pour les tests d'interaction, coverage pour la couverture de code, selenium et cherrypy pour le test d'acceptation, cucumber pour le "développement dirigé par les comportements" (behavioral-driven development ou BDD), Hypothesis pour le property-based testing.

Approches formelles

Le but de cette partie plus théorique est de faire découvrir aux étudiants le monde des spécifications et des approches formelles. L'UE ne se spécialisera pas sur une méthode en particulier (changement par rapport aux années passées), mais présentera plusieurs approches, sans prétendre à l'exhaustivité, et en restant proche du développement et de la conception logiciels. L'idée est que les étudiants sachent ce qu'on peut attendre d'une méthode formelle (quelles propriétés d'un programme peut-on prouver ?), et aient une idée de l'effort à fournir pour y parvenir.

L'UE abordera essentiellement la spécification à base de contrats (on fera un petit détour par la programmation par contrat). On verra ensuite comment on peut vérifier qu'un programme est conforme à ses contrats (et si c'est toujours possible). On utilisera notamment des méthodes d'exécution symbolique et des solveurs pour la satisfaisabilité modulo théorie (SMT). On fera le lien avec la partie test en abordant par ex leur génération automatique. Suivant l'avancement du cours on pourra regarder le model-checking avec Spin, la preuve de programme en C# avec Spec# (RiSE), l'interprétation abstraite avec Contracts (RiSE), le model-checking borné avec Alloy.

Le pré-requis est d'avoir un attrait pour les aspects formels de l'informatique, et d'avoir des connaissances de base en automates, logique du premier ordre, théorie des ensembles.

À l'issue de l'UE, les étudiants doivent:

  • savoir énumérer quelques types de méthodes formelles existants, être conscients de leurs avantages et inconvénients (notamment par rapport au test);
  • avoir intégré la nécessité d'une abstraction des programmes, la plupart des méthodes formelles s'appliquant à un modèle du programme et non à son implémentation, trop bas niveau et détaillée;
  • connaître les concepts de la spécification par contrats;
  • avoir compris les notions de logique décidable/indécidable, de complétude et de sûreté d'une analyse.

Mirabelle Nebut
dernière modification : 26/11/2016 à 17:02:58
  • CTD: lundi 8h30-10h M5 A9
  • TP: lundi 10h20 12h20 M5 A15
Mirabelle Nebut
dernière modification : 09/01/2017 à 10:18:07
Séance Cours-TD TP Remarque
1 du 16/01 au 21/01 intro au test, rudiments de test fonctionnel,
demo unittest, doctest
tp1, découvrir l'envt de travail python
2 du 23/01 au 28/01 intro au TDD, démo tp2 : TDD exposés Zune / Ariane 4 / Heartbleed
3 du 30/01 au 04/02 test en isolation,
pratique du TDD,
mocks
TP3 avec mockito exposés patriot / USS yortown / pathfinder
4 du 06/02 au 11/02 architecture dirigée par les tests TP4 : login exposés blackout
5 du 13/02 au 18/02 critères de test structurels TP5 : filtre + ES exposés Toyota / montée en charge / test statique (revue de code etc) / LAM
du 20/02 au 25/02 interruption pédagogique hiver
6 du 27/02 au 04/03 test d'acceptation TP 6 : Selenium et code à refactorer exposés test par mutation / BDD / analyse statique / Therac 25
7 du 06/03 au 11/03
évaluation
test
8 du 13/03 au 18/03 programmation par contrats Hanoï avec openJML CPP mardi 14, 12h salle Delattre
exposés : Eiffel / C# / OCL
9 du 20/03 au 25/03 vérif de programmes sans boucle TP Spec# - Code Contracts exposés : Esterel / Alloy / B
10 du 27/03 au 01/04 property-based testing exposés : model-based testing * 2 / qu'est-ce qu'un assistant de preuve
11 du 03/04 au 08/04 vérif de programmes avec boucles exposés : Facebook / Astrée / Timsort
du 10/04 au 16/04 interruption pédagogique de printemps
du 17/04 au 22/04 interruption pédagogique de printemps
12 du 24/04 au 29/04 model-checking exposés : Amazon / mondex / Storm Surge Barrier
dernière semaine
13 du 01/05 au 06/05 férié férié lundi 1er mai férié
Mirabelle Nebut
dernière modification : 23/03/2017 à 09:59:30

L'évaluation est basée sur un contrôle continu englobant les TPs réalisés et deux interrogations écrites.

Deux interrogations écrites auront lieu:

  • interrogation écrite sur le test à la fin de la partie test, note Itest
  • interrogation sur les approches formelles pendant la prmeière session des examens du M1 S2, note Iformel
Ces interrogations écrites ne seront pas rattrapées (même en cas d'absence ou de note inférieure à la moyenne) avant l'examen de seconde session qui regroupera les parties test et approches formelles.

La note de TP TP, sur 20, inclut les TPs évalués et éventuellement d'autres travaux de type exposé. Les TPs sont rendus sur PROF ou Moodle à la fin de chaque séance de TP, par binôme, et permettent un retour pédagogique régulier. Un TP non rendu sur PROF ou Moodle est un TP non rendu (il est conseillé de faire des dépôts sur PROF au long de la séance). Un étudiant absent lors de la séance doit en avertir l'enseignant, suite à quoi son évaluation sera éventuellement adaptée pour ce TP.

La note finale sur 20 (N) est calculée comme une moyenne pondérée de ces trois notes :

N = SUP(I, (TP + 2*I)/3) avec I = (Itest + Iformel)/2

Lors de la seconde session d'examen la note TP est conservée, la note d'interrogation écrite (I = (Itest + Iformel)/2) est remplacée par la note I2 obtenue lors de la seconde session, le calcul se faisant par:

N = SUP(I2, (TP + 2*I2)/3)

L'unité acquise apporte 5 ECTS.

M. Nebut

exposés:

Sujet de projet.

Cours-TD Test

CTD1 Introduction au test unitaire, test unitaire et documentation avec Python3

CTD2 Introduction au test driven development (TDD)

CTD3 test unitaire, test système, mocks:

CTD4 pratique du TDD, test unitaire, architectures testables:

CTD5 Critères de test structurels, couverture de code:

CTD6 test d'acceptation

Cours-TD Méthodes formelles

CTD7 Introduction à la programmation par contrats

  • slides
  • démo sur les cas "restaurant d'entreprise" et "éclairage" en utilisant Java et JML

CTD8 Introduction à la vérification des programmes sans boucles:

CTD9 Introduction au property-based testing

CTD10 Introduction à la vérification des programmes avec boucles:

CTD11 Introduction très très courte au model-checking

TP

Les TPs se font obligatoirement en binôme selon le principe de la programmation en binôme (l'un a le clavier et propose, l'autre commente), en alternant le clavier par tranches de 25 minutes. On travaillera par tranches de 25 minutes suivies de 5 minutes de pause, sans oublier le rendu sur PROF.

L'archive rendue sur PROF doit être intitulée

TPX_loginetudiant1_loginetudiant2.tgz (ou zip)

sans espaces, en reprenant le login université (de la forme prenom.nom). De même les noms de fichiers ou de répertoire ne doivent pas contenir d'espaces. L'archive contiendra systématiquement un README indiquant le travail réalisé et les éventuelles difficultés rencontrées (notamment si un test ne passe pas !)

TP1: sujet, source tp1.pyc oups ! Ce fichier n'est pas pour la bonne version de python. Prendre /home/enseign/SVL/tp1.pyc

TP2: sujet

TP3: reprendre et terminer le cas "restaurant d'entreprise" en utilisant l'approche par mocks et en développant d'abord Caisse puis Carte. Commencer par des tests unitaires, terminer par un test d'intégration. Et avant toute chose : lister / prioriser les fonctionnalités des classes et les traiter les unes après les autres.

TP4 sujet login.

TP5

TP6 test fonctionnel avec Selenium

TP7 : contrats sur Hanoï, sujet

TP8 : vérification sans boucles avec les outils de RiSE4fun, sujet, archive pour les exemples.

TP9 : property-based testing avec Hypothesis

  • finir le TP8
  • lié au TP8 : en utilisant l'approche vue en cours pour tester les invariants, tester les invariants qui ne passent pas sur votre TP8 (compte avec découvert, buffer circulaire). Dans le cas du compte avec découvert, comprenez-vous le problème maintenant ? Si vous aviez trouvé toute de suite une implem conforme à l'invariant, essayer tout de même avec cette version fausse.
  • pensez-vous que l'utilisation d'Hypothesis assure une couverture de 100% ?
  • est_il possible qu'un test utilisant hypothesis passe certaines fois et d'autres non ?

TP10 : vérification de boucles avec Spec\#, sujet

TP11 : model-checking, PathFinder avec Spin, sujet

Documentation

Python

Nous utiliserons Python3 en SVL:

  • au M5 la version par défaut de Python est la 2.7
  • la version 3.5.2 est accessible par python3
  • si vous rencontrez des problèmes d'encodage, vous êtes peut-être en python2. Pour connaître les différences entre les 2 versions (non compatibles)

Quand on vient du monde Java :

  • le self est obligatoire
  • on ne peut pas utiliser le même nom pour un attribut et une méthode
  • pas de déclarations

Le module unittest alias pyunit

  • la doc
  • dans la doc, les assertions
  • ou help(unittest), help(unittest.TestCase), etc
  • NB sur le assertEqual : contrairement au assertEqualS de JUnit, pas d'ordre imposé sur les paramètres (expected, actual). On choisit un ordre et on s'y tient.
  • unittest ne propose pas de tests paramétrés, voir une extension ici

Le module doctest

  • la doc
  • pour les exceptions : doctest ne prend en compte que la ligne Traceback etc puis la ligne contenant le nom de l'exception et les suivantes. On pourra donc supprimer les autres et utiliser une ellipse (même si l'ellispe n'est pas prise en tant que telle ici):
    >>> s.ajouter_reference("ref1")
    Traceback (most recent call last):
    ...
    ValueError																		    
  • sans utilisation de l'option -v l'exécution de la doctest ne produit aucune sortie si pas d'erreur
  • exécution avec nose : nosetests -v --with-doctest (ne s'exécute pas si le fichier de test est passé en ligne de commande)
  • exécution avec python : terminer le module toto par
    								  
    if __name__ == "__main__":
        import doctest
        doctest.testmod()								  
    
    et lancer python3 -v toto.py
  • autre exécution avec python (shortcut pour testmod qui ne marche pas toujours) : python3 -m doctest -v toto.py

Nose

  • le site officiel. Prévoir de passer à nose2 !
  • nose au M5 : nosetests3 : version 1.3.4 pour python3, nosetests-2.[6|7] : version 1.1.2 pour python2
  • pour installer nose sur votre machine perso, et faire en sorte que nose utilise python3 et non python2, il faut penser à utiliser easy_install-3 (et pas simplement easy-install comme indiqué sur la page d'accueil de nose)
  • les options de nosetests :
    • Nose collecte les fichiers, classes et fonctions/méthodes incluant le mot test ou Test (lancer nosetests). On peut aussi lancer un fichier de test seulement par nosetests test_bidon.py.
    • -v pour afficher le détail des tests qui sont exécutés (affiche la docstring du cas de test si elle existe à la place de son nom).
    • --with-doctest pour tester la documentation (modules, classes, fonctions, méthodes). Attention la doctest ne sera pas exécutée si le fichier de test est passé directement à nose.

JUnit

TDD et méthodes agiles (pro-TDD)

TDD et unit testing: les contres et les nuancés

Dans la série "TDD is dead": Dans la série "Why Most Unit Testing is Waste", chez RBCS:

TDD et mocks

Module python mockito

  • Le site officiel et une petite doc
  • fiche qui résume mockito
  • installé au M5 pour python3
  • pour ceux qui ont des soucis d'installation sur leur machine perso, avec un message ressemblant à ça :
    ...
        Traceback (most recent call last):
          File "./distribute_setup.py", line 143, in use_setuptools
            raise ImportError
        ImportError
    ... could not build the egg.
    
    vous pouvez essayer d'installer cette autre version, par ex avec pip3 install --user mockito-without-hardcoded-distribute-version-0.5.4.tar.gz

Couverture de code avec Nose et coverage

  • Le site officiel du module coverage
  • coverage est installé au M5
  • si sur votre machine perso nose ne voit pas coverage, essayer d'ajouter le répertoire contenant coverage dans le PATH

Pour lancer coverage via nose :
  • nosetests --cover-html --with-coverage --cover-erase --cover-branches --cover-package=bidon test_bidon.py
  • --with-coverage --cover-erase pour lancer coverage sans repartir des résultats précédents, affichage d'un rapport textuel de la forme:

    Name                    Stmts   Miss  Cover   Missing
    -----------------------------------------------------
    restaurant_entreprise      55      4    93%   120, 220-222
    ----------------------------------------------------------------------
    Ran 18 tests in 0.057s
    
  • --cover-package=nom_package pour lancer coverage sur ce module uniquement
  • --cover-branches pour demander la couverture des branches
  • --cover-html pour demander la génération d'un rapport au format html (dans un répertoire cover par défaut, peut-être modifié)

Si la version pour python3 de coverage n'est pas installée, alors l'installer en local:

pip3 install --user nose coverage
crée un répertoire .local à la racine de votre compte s'il n'existe pas déjà. Ensuite utiliser cette version dans votre terminal après avoir entré:
export PATH=$HOME/.local/bin:$PATH
Si ça ne marche pas, essayer avec ça:
export HTTP_PROXY=http://cache-etu.univ-lille1.fr:3128

Selenium

  • le site officiel
  • une readthedocs sur Selenium WebDriver
  • la doc de Selenium IDE
  • pour installer Selenium IDE sur Firefox, depuis la page download, chercher "selenium IDE" pour l'installer depuis addons.mozilla.org
  • pour installer selenium webdriver sur votre machine perso: pip3 install --user --upgrade selenium, installer aussi le driver geckodriver et l'ajouter dans le PATH
  • le driver pour Chrome est à télécharger, l'exécutable chromedriver devant se trouver dans le PATH

Bottle

  • le site officiel
  • install sur votre machine perso: pip3 install --user --upgrade bottle

Behavior Driven Development

  • L'histoire (fictive) d'une équipe qui se met au test d'acceptation / au BDD / à la spécification par l'exemple, écrite par Alistair Scott.
  • une présentation sur le site de Behave (attention les oracles de la classe TestList sont de pures horreurs), inspirée de la page wikipedia ci-dessous
  • sur wikipedia, le BDD comme approche comportementale du test d'acceptation impliquant toutes les parties prenantes d'un projet, y compris (et surtout) les non-informaticiens
  • approches connexes: Acceptance test-driven development, Specification by example
  • BDD et TDD sur le BDDwiki, à lire au moins pour la description faite du TDD
  • une intro détaillée par Dan North, expliquant l'historique du pourquoi du comment et donnant un éclairage intéressant sur le TDD
  • le BDD, certains l'aiment et d'autres non

Outillage pour le BDD

  • Cucumber, l'outil de référence
  • Behave, un portage de Cucumber pour Python
  • sur le site de Behave, une comparaison avec les outils existants
  • pour lancer Behave en ne lançant pas les scenarios "tagués" par todo : behave --tags=-todo

JML : programmation par contrats pour Java

  • JML homepage
  • openJML, une des distributions (qui supporte Java7), et ici
  • openJML sur rise4fun
  • le manuel de référence de JML
  • pour compiler des programmes Java avec openJML:
    java -jar $OPENJML/openjml.jar -rac -racCompileToJavaAssert -d classes src/mon_package/*.java
    
  • pour exécuter des classes Java compilées avec openJML:
    java -ea -cp classes:$OPENJML/openjml.jar:.:$CLASSPATH mon_package.MaClasse

Spec# : contrats en C# et vérification avec Boogie

Contracts: contrats et interprétation abstraite

Microsoft Research in Software Engineering (RiSE)

Logique de Hoare, transformateurs de prédicats de Dijkstra

  • un résumé de la logique de Hoare, sur la page de Fabrice Rossi
  • Hoare et Dijkstra, Forward with Hoare, chapitre de livre écrit pour l'occasion des 40 ans de la logique de Hoare

Hypothesis, property-based testing pour Python

Property-based testing

PyExZ3, exploration de programmes Python par exécution symbolique dynamique

  • pas installé au M5
  • le site sur github, download et doc succinte
  • utilise le prouveur Z3 (installé au M5) pour calculer la satisfaisabilité des expressions logiques
  • l'exécutable z3 doit être dans le PATH et le PYTHONPATH
  • ne marche que pour du Python fonctionnel pur (pas pour Python objet)
  • l'exploration s'arrête si exécution d'une assertion ou levée d'exception
  • un papier qui décrit formellement l'outil
  • python3 pyexz3.py --start=ma_fonction mon_module.py

Z3, un solveur SMT (satisfaisabilité modulo théorie)

  • site officiel
  • RISE4fun pour essayer Z3 en ligne sur Rise for fun, avec tutoriel
  • API pour Python: le module z3

Pex : concolic testing et contrats

  • le site
  • pex for fun, pour essayer en ligne, les bases de Pex for fun (on tombe soit sur une exécution de Pex classique, soit sur un coding duel - trouver grâce à Pex une implem secrète)
  • pex for fun avec code contracts, le mode "contracts" s'active aussi automatiquement avec using System.Diagnostics.Contracts;
  • Pex est devenu IntelliTest, disponible sous Visual Studio depuis 2015, en passant par SmartTest. Voir ici et pour comprendre comment sont générés les tests, et le manuel de référence.

Vérification, divers

  • More than one way (also in verification), un article du blog bugcounting, qui montre sur un ex comment des outils de vérification appartenant à la même mouvance ont leurs particularités et obtiennent des résultats différents.
  • Dimensions in program verification, un article du blog bugcounting, qui classe différentes méthodes selon les 3 axes : correction (soundness, correctness = si l'outil dit que le programme est correct, c'est qu'il l'est vraiment), largeur du spectre des programmes et spécifications couverts (flexibility) et degré d'automatisation
  • théorème de Rice et impact pratique sur wikipedia

Méthodes (très) formelles et success stories

Programmation par contrats

Module contract pour Python

  • description synthétique
  • téléchargement de l'archive
  • le PYTHONPATH doit contenir le chemin d'accès au répertoire qui contient contract.py
  • attention ce module n'est utilisable en l'état que pour python2
  • attention le implies n'est pas paresseux, implies(b, alors, sinon) évalue alors même si b vaut faux.
  • attention ne pas appeler dans un invariant de classe un accesseur de la même classe (sinon la bibliothèque évalue l'invariant en fin d'appel et récursion infinie)

Mockito pour Java

  • le site officiel de mockito
  • l'API de la version courante (lien "documentation" sur le site officiel)
  • le "tutoriel mockito" est la javadoc de la classe Mockito
  • fiche qui résume Mockito

Test et/ou OO en général :

  • la librairie de contraintes hamcrest
  • le site de xUnit patterns
  • Perfecting OO s Small Classes and Short Methods un article sur le sujet
  • un article sur les 10 points qui rendent votre code non testable. Attention, les points 7 et 8 rendent le code testable, les autres points le rendent non testable.
  • un message de blog expliquant comment mal utiliser une bibliothèque de mocks puissante peut renforcer ue mauvaise conception.
  • tenté d'implanter maintenant une fonctionnalité qui ne sera mise en production que plus tard ? le principe de YAGNI expliqué par Martin Fowler.
  • levée d'exception ou non ? Le cas de la validation des données par Martin Fowler
  • More Typing, Less Testing: TDD with Static Types, par Ken Fox, part1 et part2

Concernant Spin :

Autres cours de test

Annales

Les sujets ci-dessous sont partiellement périmés au sens où le contenu du cours change chaque année.

Mirabelle Nebut
dernière modification : 04/05/2017 à 11:13:26