La verification a pour but de produire des programmes comprenant moins de bugs.
Le schema de developpement d'un logiciel actuel est le suivant:
1. Etude des besoins
2. Conception du logiciel
3. Implementation
4. Tests
5. Suivant les resultats des tests, retour en 2 ou 3.
Avec verification:
1. Etude des besoins
2. Conception informelle
3. Ecriture d'une specification formelle
4. Implementation
5. Verification
6. Retour en 4.
Le point important est l'etape 3. On ecrit dans un langage mathematique ce que le code doit faire. A partir de ca, on peut verifier que l'implementation respecte la specification.
Dans le cas de jeda, ce n'est pas de la verification qui est faite, mais plutot du test. A partir de la specification, on genere les tests pour tester que le programme est correct.
Un petit exemple: Specification: f est un fonction de N dans N tel que: pour tout n>0, f(n) est pair. Implementation:
int f(int n) {
return 2*n;
}
Tester revient a regarder la valeur de f(n) pour 1000 n differents (par exemple).
Une verification analyse le code source, et prouve que toute valeur retournee par f est pair. Ici c'est "evident", vu qu'un entier positif multiplie par 2 est toujours pair (il y a un piege, cependant, la fonction ne manipule qu'un sous-ensemble des entiers)
Traditionnellement (pour la plupart des LL, par exemple), aucune specification n'est ecrite. On passe directement a l'implementation, et on fait confiance aux utilisateurs pour decouvrir les bugs et les corriger.
Les outils de verification formelle peuvent etre tres utiles pour les systemes paralleles et temps reel. On peut ainsi verifier des proprietes telles que:
- La requete de X est toujours satisfaite avant 20 secondes
- Un dead-lock ne peut jamais survenir
- Toute requete est satisfaite en un temps fini
Notez bien que l'on verifie, c'est plus puissant qu'un test. Verifier revient a tester toutes les possibilites.
Un peu de pub: http://www.uppaal.com/(...) Uppaal Un outil de verification de systemes temps reels concurrents http://www.atelierb.societe.com/(...) Atelier B Une methode et des outils pour generer du code correct http://www.afm.sbu.ac.uk/(...) Formal methods Pour ceux qui veulent en savoir plus sur les methodes formelles. C'est un domaine de recherche tres actif en ce moment.
[^] # Re: C'est quoi un langage de vérification ?
Posté par Johann Deneux . En réponse à la dépêche Jeda: langage de vérification open source. Évalué à 1.
Le schema de developpement d'un logiciel actuel est le suivant:
1. Etude des besoins
2. Conception du logiciel
3. Implementation
4. Tests
5. Suivant les resultats des tests, retour en 2 ou 3.
Avec verification:
1. Etude des besoins
2. Conception informelle
3. Ecriture d'une specification formelle
4. Implementation
5. Verification
6. Retour en 4.
Le point important est l'etape 3. On ecrit dans un langage mathematique ce que le code doit faire. A partir de ca, on peut verifier que l'implementation respecte la specification.
Dans le cas de jeda, ce n'est pas de la verification qui est faite, mais plutot du test. A partir de la specification, on genere les tests pour tester que le programme est correct.
Un petit exemple:
Specification: f est un fonction de N dans N tel que: pour tout n>0, f(n) est pair.
Implementation:
int f(int n) {
return 2*n;
}
Tester revient a regarder la valeur de f(n) pour 1000 n differents (par exemple).
Une verification analyse le code source, et prouve que toute valeur retournee par f est pair. Ici c'est "evident", vu qu'un entier positif multiplie par 2 est toujours pair (il y a un piege, cependant, la fonction ne manipule qu'un sous-ensemble des entiers)
Traditionnellement (pour la plupart des LL, par exemple), aucune specification n'est ecrite. On passe directement a l'implementation, et on fait confiance aux utilisateurs pour decouvrir les bugs et les corriger.
Les outils de verification formelle peuvent etre tres utiles pour les systemes paralleles et temps reel. On peut ainsi verifier des proprietes telles que:
- La requete de X est toujours satisfaite avant 20 secondes
- Un dead-lock ne peut jamais survenir
- Toute requete est satisfaite en un temps fini
Notez bien que l'on verifie, c'est plus puissant qu'un test. Verifier revient a tester toutes les possibilites.
Un peu de pub:
http://www.uppaal.com/(...) Uppaal Un outil de verification de systemes temps reels concurrents
http://www.atelierb.societe.com/(...) Atelier B Une methode et des outils pour generer du code correct
http://www.afm.sbu.ac.uk/(...) Formal methods Pour ceux qui veulent en savoir plus sur les methodes formelles. C'est un domaine de recherche tres actif en ce moment.