Introduction à la validation
1. Pourquoi Valider ?
Un programme / un algorithme est un objet complexe, dont il est difficile d'estimer la validité, exactement comme c'est le cas pour un théorème de mathématiques, un postulat en physique, etc.
2. Comment valider ?
A. Ailleurs... :
1. Validation d'un modèle physique
On regarde certains faits et on vérifie s'ils sont en adéquation avec le modèle :
- Tous les faits en adéquation semblent confirmer le modèle ;
- Un seul fait en contradiction montre que le modèle est erroné.
2. Validation d'un théorème en mathématiques
On essaie de prouver le théorème :
- Si la preuve aboutit (et qu'elle est juste...) alors le théorème est vrai ;
- Sinon : soit on ne sait pas faire la preuve, soit le théorème est faux.
3. Validation d'une solution technique
"Preuve de concept" : On fait une expérience où un bout de la solution technique est réalisé :
- tout le monde est d'accord sur l'expérience : on a bien compris la même chose ;
- ça semble marcher : il semble que l'on soit sur la bonne voie.
B. En informatique
1. Test
On essaie notre algorithmes sur différentes valeurs d'entrée, et on regarde si le résultat produit par notre algorithme (notre "modèle") est conforme à nos attentes (la "réalité").
→ analogie avec la validation d'un modèle physique
2. Preuve
On essaie de vérifier formellement que notre algorithme fonctionne dans tous les cas.
→ analogie avec la validation d'un théorème mathématique
3. Prototypage
On écrit une fonction qui simule ce que devrait calculer l'algorithme.
→ analogie avec la preuve de concept
C. Comparaison entre les 3 principes de validation ci-dessus
| Ce qui est vérifié | Cible | Avantage | Inconvénient | |
|---|---|---|---|---|
| Protypage | La bonne compréhension du problème | Développeurs | Intervient très tôt | Aucune garantie sur le résultat final |
| Test | Un fonctionnement correct dans des cas bien précis | Programme exécuté | Facilité de mise en oeuvre, nombreux outils | Intervient à la fin, loin d'être exhaustif |
| Preuve | La correction par rapport aux propriétés spécifiées formellement | Code et/ou conception | Garantie obtenue | Lourd à mettre en place |
III. Le cas particulier du model checking
A. Principe
Model checking = test exhaustif
B. Avantages
- Facile à mettre en oeuvre
- Garantie obtenue
- Nombreux outils
C. Inconvénients
- Temps de calcul
- Pas toujours possible : le système doit être fini et de taille raisonnable, ou doit pouvoir se ramener à un tel système
- Interprétation des résultats difficiles en cas d'échec : un bug se traduit par de nombreuses traces d'exécution "en échec", traces qui sont souvent difficiles à interpréter.