Extrait de la newsletter:
"TECHNOLOGY
--Engineer offers open-source verification language--
Atsushi Kasuya, verification engineer at Juniper Networks Inc.,
didn't like any of the existing languages used for verification, so
he wrote his own and is now offering it to the design community on an open-source basis."
Traduction approximative pour les non-anglophones:
"TECHNOLOGIE
-- Un ingénieur offre un langage de vérification open source--
Atsushi Kasuya, un ingénieur vérification à Juniper Networks Inc., n'aimait aucun des langages de vérification existants, alors il a écrit le sien et il l'offre maintenant sous licence open source à la communauté des développeurs [hardware]."
En fait, s'agit du langage de vérification Jeda, actuellement en version 1.0.6 et publié sous license GPL. Ce qui est intéressant dans l'article, c'est que le terme open source est mis en avant.
<mode="rêve on">Après les EDAs fonctionnels gratuits, à quand les EDAs fonctionnels open source?</mode>
Aller plus loin
- L'article (3 clics)
- Jeda, le site (6 clics)
- Application scientifiques sous Linux (3 clics)
# C'est quoi un langage de vérification ?
Posté par bmc . Évalué à 1.
[^] # Re: C'est quoi un langage de vérification ?
Posté par Troy McClure (site web personnel) . Évalué à 1.
Ç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 . É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.
# jeda ?
Posté par Ramón Perez (site web personnel) . Évalué à 1.
[^] # Re: jeda ?
Posté par jpph . Évalué à 1.
[^] # Re: jeda ?
Posté par kadreg . Évalué à 1.
"Quand un chevalier Jedi est fatigué, il devient un chevalier jebi"
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.