La méthode B est un exemple des très nombreuses façons de faire de la vérification formelle (encore que B ne fait pas que de la vérification). Il faut aussi regarder toutes les implémentations de model checking, pour ce qui est de la logique temporelle majoritairement, mais aussi les assistants de preuves comme Coq ou encore les outils de comparaison type boite noire, souvent basés sur de la bissimulation, justement pour montrer qu'un programme est bissimilaire à une spécification. Il existe encore d'autres domaines de vérification formelle, donc c'est très très large et cela ne se réduit pas à la méthode B (qui, d'après ce que j'en ai entendu par un de ses concepteurs, a permis de trouver un bug dans le simulateur utilisé pour valider le programme de la ligne 14).
Pour ce qui est de cette histoire de bug sur le karma (pertinent/inutile), je n'ai rien compris, mais si c'est la question, je n'ai jamais cliqué sur le lien « inutile » de quelque commentaire que ce soit :)
[^] # Re: Vérification formelle
Posté par vlamy . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 2. Dernière modification le 18 avril 2014 à 14:51.
La méthode B est un exemple des très nombreuses façons de faire de la vérification formelle (encore que B ne fait pas que de la vérification). Il faut aussi regarder toutes les implémentations de model checking, pour ce qui est de la logique temporelle majoritairement, mais aussi les assistants de preuves comme Coq ou encore les outils de comparaison type boite noire, souvent basés sur de la bissimulation, justement pour montrer qu'un programme est bissimilaire à une spécification. Il existe encore d'autres domaines de vérification formelle, donc c'est très très large et cela ne se réduit pas à la méthode B (qui, d'après ce que j'en ai entendu par un de ses concepteurs, a permis de trouver un bug dans le simulateur utilisé pour valider le programme de la ligne 14).
Pour ce qui est de cette histoire de bug sur le karma (pertinent/inutile), je n'ai rien compris, mais si c'est la question, je n'ai jamais cliqué sur le lien « inutile » de quelque commentaire que ce soit :)