C'est quoi un langage de vérification ?

• [^]Re: C'est quoi un langage de vérification ?

  Posté par Troy McClure (page perso, ) le 27/11/2001 à 09:26. (lien). Évalué à 1.

  Je m'apprêtais à poser la même question... En lisant la homepage, j'ai même trouvé un indice: "Jeda is a C-like programming language for hardware design verification." .. mouais...
  
  Ça aurait quand même été bien d'être un poil plus explicatif dans la news.

• [^]Re: C'est quoi un langage de vérification ?

  Posté par Johann Deneux (page perso, ) le 27/11/2001 à 10:38. (lien). Évalué à 1.

  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.

jeda ?

• [^]Re: jeda ?

  Posté par jean-philippe p (page perso, ) le 27/11/2001 à 15:24. (lien). Évalué à 1.

  -- May the Source be with You --

  • [^]Re: jeda ?

    Posté par kadreg () le 27/11/2001 à 15:37. (lien). Évalué à 1.

    Signalons le également :
    "Quand un chevalier Jedi est fatigué, il devient un chevalier jebi"