De mon point de vue, en tant qu'utilisateur quotidien d'Esterel, utilisateur avéré de son module de preuve formelle, utilisateur d'autres modules de preuve formelle et utilisateur de validation par stimuli pseudo-aléatoires sous force brute, la validation par preuve formelle est complémentaire à toute autre forme de validation. Aucune n'est à négliger. Un court retour d'expérience s'impose.
Dans le projet dont je m'occupe, la preuve formelle a permis de trouver certains bugs fonctionnels bien avant tout autre forme de validation et a en outre le net avantage de proposer un contre exemple de taille minimale, ce qui facilite le travail des designers.
La preuve formelle, telle qu'intégrée à Esterel permet aussi, avec peu d'effort, soit de trouver des contre-exemples pour les cas d'émission multiples de signaux, les cas de lecture avant écriture, les cas de dépassement... soit de prouver que l'implémentation est sure de ce point de vue - ce qui déjà n'est pas négligeable.
Toujours dans ce projet, certains sous-modules qui s'y prêtaient ont été prouvés formellement. Comme souligné plus haut, cela signifie que selon les contraintes d'entrées qui ont été définies, le sous-module ne viole aucune des propriétés décrites. Donc, si l'algorithme de preuve est sur-contraint pour quelque raison que ce soit, certains bugs peuvent ne pas être détectés. C'est arrivé dans ce projet, même les modules prouvés formellement en aval de la validation fonctionnelle usuelle, se sont vu trouver des bugs par la validation par stimulus pseudo-aléatoire. Mais force est de constater que ces modules prouvés formellement ont eu proportionnellement moins de bugs trouvés par la validation fonctionnelle que les autres en regard de leur complexité.
Enfin, de mon point de vue, l'atout maître de la preuve formelle, est la preuve d'équivalence lors de l'optimisation d'un module. Elle permet de prouver que deux implémentations sont formellement équivalentes, et donc de remplacer en confiance l'implémentation naïve initiale, qui a le mérite d'être claire et lisible, par la version optimisée.
En conclusion, la preuve formelle c'est un nouvel outil pour la validation de code. C'est un outil puissant, complémentaire aux autres formes de validation, et, comme tout outil, il faut savoir l'utiliser à bon escient et en connaître les limites.
[^] # Re: mouais
Posté par EzDaYo . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 7.
Dans le projet dont je m'occupe, la preuve formelle a permis de trouver certains bugs fonctionnels bien avant tout autre forme de validation et a en outre le net avantage de proposer un contre exemple de taille minimale, ce qui facilite le travail des designers.
La preuve formelle, telle qu'intégrée à Esterel permet aussi, avec peu d'effort, soit de trouver des contre-exemples pour les cas d'émission multiples de signaux, les cas de lecture avant écriture, les cas de dépassement... soit de prouver que l'implémentation est sure de ce point de vue - ce qui déjà n'est pas négligeable.
Toujours dans ce projet, certains sous-modules qui s'y prêtaient ont été prouvés formellement. Comme souligné plus haut, cela signifie que selon les contraintes d'entrées qui ont été définies, le sous-module ne viole aucune des propriétés décrites. Donc, si l'algorithme de preuve est sur-contraint pour quelque raison que ce soit, certains bugs peuvent ne pas être détectés. C'est arrivé dans ce projet, même les modules prouvés formellement en aval de la validation fonctionnelle usuelle, se sont vu trouver des bugs par la validation par stimulus pseudo-aléatoire. Mais force est de constater que ces modules prouvés formellement ont eu proportionnellement moins de bugs trouvés par la validation fonctionnelle que les autres en regard de leur complexité.
Enfin, de mon point de vue, l'atout maître de la preuve formelle, est la preuve d'équivalence lors de l'optimisation d'un module. Elle permet de prouver que deux implémentations sont formellement équivalentes, et donc de remplacer en confiance l'implémentation naïve initiale, qui a le mérite d'être claire et lisible, par la version optimisée.
En conclusion, la preuve formelle c'est un nouvel outil pour la validation de code. C'est un outil puissant, complémentaire aux autres formes de validation, et, comme tout outil, il faut savoir l'utiliser à bon escient et en connaître les limites.