Vérification formelle des programmes en pratique

Jessaierai de donner une réponse succincte à certaines de vos questions.Veuillez garder à lesprit que ce nest pas strictement mon domaine de recherche, donc certaines de mes informations peuvent être obsolètes / incorrectes.

1. De nombreux outils sont spécifiquement conçus pour prouver formellement les propriétés de Java et C ++.

   Cependant, je dois faire une petite digression ici: que signifie prouver lexactitude dun programme? Le vérificateur de type Java prouve une propriété formelle dun programme Java, à savoir que certaines erreurs, comme lajout dun float et dun int, ne peuvent jamais se produire! Jimagine que vous êtes intéressé par des propriétés beaucoup plus fortes, à savoir que votre programme ne peut jamais entrer dans un état indésirable, ou que la sortie dune certaine fonction est conforme à une certaine spécification mathématique. En bref, il existe un large gradient de ce que peut signifier «prouver quun programme est correct», allant de simples propriétés de sécurité à une preuve complète que le programme répond à une spécification détaillée.

   Maintenant, je vais supposer que vous êtes intéressé par la démonstration des propriétés fortes de vos programmes. Si vous êtes intéressé par les propriétés de sécurité (votre programme ne peut pas atteindre un certain état), alors en général, il semble que la meilleure approche soit vérification du modèle . Cependant, si vous souhaitez spécifier complètement le comportement dun programme Java, le mieux est dutiliser un langage de spécification pour ce langage, par exemple JML . Il existe de tels langages pour spécifier le comportement des programmes C, par exemple ACSL , mais je ne sais pas C ++.

2. Une fois que vous avez vos spécifications, vous devez prouver que le programme est conforme à ces spécifications.

   Pour cela, vous avez besoin dun outil qui a un compréhension formelle des deux votre spécification et la sémantique opérationnelle de votre langage (Java ou C ++) pour exprimer le théorème dadéquation , à savoir que lexécution du programme respecte la spécification.

   Cet outil devrait également vous permettre de formuler ou de générer la preuve de ce théorème. Maintenant, ces deux tâches (spécifier et prouver) sont assez difficiles, elles sont donc souvent séparées en deux:

   • Un outil qui analyse le code, la spécification et génère le théorème dadéquation. Comme Frank la mentionné, Krakatoa est un exemple dun tel outil.

   • Un outil qui prouve le théorème ( s), automatiquement ou interactivement. Coq interagit avec Krakatoa de cette manière, et il existe de puissants outils automatisés comme Z3 qui peuvent également être utilisés.

   Un point (mineur): il y a des théorèmes qui sont beaucoup trop difficiles à prouver avec des méthodes automatisées, et les prouveurs automatiques de théorèmes sont connus pour avoir parfois des bogues de validité qui les rendent moins fiables. Cest un domaine où Coq brille en comparaison (mais ce nest pas automatique!).

3. Si vous voulez générer du code Ocaml, alors écrivez dabord en Coq (Gallina), puis extrayez le code. Cependant, Coq est terrible pour générer du C ++ ou Java, si cest même possible.

4. Les outils ci-dessus peuvent-ils gérer les problèmes de threads et de performances? Probablement pas, les problèmes de performances et de threading sont mieux traités par des outils spécialement conçus, car ce sont des problèmes particulièrement difficiles. Je ne suis pas sûr davoir des outils à recommander ici, bien que le projet PolyNI de Martin Hofmann semble intéressant.

En conclusion: la vérification formelle des programmes Java et C ++ « du monde réel » est un domaine vaste et bien développé, et Coq convient à certaines parties de cette tâche. Vous pouvez trouver un aperçu de haut niveau ici par exemple.

Commentaires

• Merci pour ce post et les références que vous avez ajoutées. À mon humble avis, lobjectif des ingénieurs en logiciel est de pouvoir publier rapidement des systèmes qui 1) fourniront toujours des résultats corrects, 2) néchoueront jamais. Je pourrais voir un problème de régression ici, où vous voudrez peut-être prouver que la spécification elle-même est  » sans bogue  » 🙂 comme essayer de définir  » proposition vraie dun langage  » avec un méta-langage, puis avoir besoin dun autre méta-langage pour cela, puis dun autre un …
• Le problème est que ce que lutilisateur  » veut  » nest généralement pas exprimé de manière formelle Langue! Il ny a généralement pas de réponse formelle à la question:  » cette spécification formelle est-elle conforme à mon idée informelle? « . Il est ‘ possible de tester une spécification formelle et de prouver qu’elle possède certaines propriétés mathématiques, mais en fin de compte, vous devez relier les mathématiques au monde réel, qui est un processus non formel.
• Oui bien sûr – jai toujours réalisé que les méthodes formelles ne pouvaient commencer quà partir dun point bien défini.Si cette spécification est conforme ou non aux besoins conscients / inconscients / non découverts des utilisateurs réels est un autre problème, non adressable avec des méthodes formelles (mais certainement un problème pour les ingénieurs).
• Un théorème est par définition un proposition prouvée. Donc, vous ne voulez probablement pas  » prouver le théorème « .
• @nbro Wikipédia semble daccord avec toi. Mathworld, cependant, définit un théorème comme une proposition dont  » peut être démontrée comme vraie par des opérations mathématiques acceptées « . Dans ce cas, donner des preuves de théorèmes est non seulement possible, mais nécessaire pour justifier de les appeler ainsi! 🙂 (ceci est une contrequibble, bien sûr)

Je voudrais mentionner trois applications remarquables des méthodes formelles / outils de vérification formelle dans lindustrie ou des systèmes réels non triviaux. Notez que jai peu dexpérience sur ce sujet et que je ne les apprends quen lisant des articles.

1. Loutil open-source Java Pathfinder (JPF en abrégé) publié par la NASA en 2005 est un système permettant de vérifier les programmes exécutables en bytecode Java (voir Java Pathfinder @ wiki ). Il a été utilisé pour détecter les incohérences dans le logiciel exécutif du K9 Rover à la NASA Ames.

2. Ce document: Utilisation de la vérification du modèle pour rechercher des erreurs graves du système de fichiers @ OSDI « 04 montre comment utiliser vérification du modèle pour trouver des erreurs graves dans les systèmes de fichiers. Un système appelé FiSC est appliqué à trois systèmes de fichiers largement utilisés et largement testés: ext3, JFS et ReiserFS, et 32 bogues graves sont détectés. Il a remporté le prix du meilleur article.

3. Ce document: Comment Amazon Web Services utilise des méthodes formelles @ CACM « 15 décrit comment AWS applique des méthodes formelles à ses produits comme S3, DynamoDB, EBS et gestionnaire de serrures distribuées interne. Il se concentre sur loutil TLA + de Lamport « . À propos, Lamport a utilisé intensivement sa propre boîte à outils TLA. Il donne souvent une vérification formelle (assez complète) dans TLA des algorithmes / théorèmes proposés par lui-même (ainsi que par ses coauteurs) dans les annexes des articles.

La vérification formelle est désormais possible pour les programmes écrits dans un sous-ensemble de C ++ conçu pour les systèmes embarqués critiques pour la sécurité. Voir http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt pour une courte présentation et http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf pour larticle complet.

Commentaires

• Merci pour les liens. Au moins un bref aperçu de leur contenu serait utile, pour se prémunir contre la pourriture des liens, dautant plus que vos liens sont vers un site Web dentreprise: ceux-ci ont tendance à être réorganisés périodiquement, supprimant tous les liens vers le site.

Un formel la spécification dun programme est (plus ou moins) un programme écrit dans un autre langage de programmation. En conséquence, la spécification inclura certainement ses propres bogues.

Lavantage de la vérification formelle est que, comme le programme et la spécification sont deux implémentations distinctes, leurs bogues seront différents. Mais pas toujours: une source commune de bogues, les cas négligés, correspondra souvent. Ainsi, la vérification formelle nest pas une panacée: elle peut encore manquer un nombre non négligeable de bogues.

Un inconvénient de la vérification formelle est quelle peut imposer quelque chose comme le double du coût dimplémentation, probablement plus (il vous faut un spécialiste de la spécification formelle, et vous devez utiliser les outils plus ou moins expérimentaux qui vont avec; cela ne sera pas bon marché).

Je devinerais mettre en place des cas de test et des échafaudages pour les exécuter automatiquement serait une meilleure utilisation de votre temps.

Commentaires

• L avantage de la vérification formelle est que … . Un deuxième inconvénient de la vérification formelle est que … Cest déroutant.
• Je pense que linadéquation entre la spécification et la tâche informelle est un problème danalyse des exigences logicielles et non un problème de programmation.

Vous posez quelques questions différentes. Je conviens quil semble que les méthodes de vérification formelles pour les applications industrielles / commerciales ne soient pas si courantes. il faut toutefois se rendre compte que de nombreux principes de «vérification formelle» sont intégrés aux compilateurs pour déterminer lexactitude du programme! donc dune certaine manière, si vous utilisez un compilateur moderne, vous « utilisez une grande partie de létat de lart en matière de vérification formelle.

Vous dites » jen ai marre des tests « mais une vérification formelle ne remplace pas vraiment les tests. en quelque sorte, cest une variation sur les tests.

Vous mentionnez Java.il existe de nombreuses méthodes de vérification formelles avancées intégrées dans un programme de vérification Java appelé FindBugs qui peuvent en effet être exécutés sur de grandes bases de code. Notez quil affichera à la fois des «faux positifs et des faux négatifs» et que les résultats doivent être examinés / analysés par un développeur humain. Mais notez que même si cela ne présente pas de vrais défauts fonctionnels, cela révèle généralement des « antipatterns » qui devraient de toute façon être évités dans le code.

Vous ne faites plus mention de votre application particulière autre que « industrielle » . La vérification formelle dans la pratique tend à dépendre de lapplication particulière.

Les techniques de vérification formelle semblent être largement utilisées en EE pour prouver lexactitude des circuits, par exemple dans la conception de microprocesseurs.

Voici un exemple denquête sur les outils de vérification formels dans le domaine EE par Lars Philipson .

Commentaires

• Il ‘ est trompeur de dire que  » a beaucoup de principes de  » vérification formelle  » sont intégrés dans les compilateurs pour déterminer lexactitude du programme « . Ce à quoi vous faites référence est la vérification de type statique, ce que font certains compilateurs, mais les propriétés vérifiées de cette façon sont plutôt simples, par exemple. éviter dajouter un nombre et une chaîne. Ceci est utile, mais loin de ce qui est généralement compris par la  » vérification formelle « .
• ne la pas fait se référer spécifiquement à la vérification de type statique, bien que ce soit un exemple simple / courant. Les techniques doptimisation du compilateur imho, qui sont répandues et avancées, sont à peu près similaires aux principes de vérification formelle, car elles impliquent des techniques avancées pour déterminer / montrer léquivalence des variantes de programme optimisées. il semble donc important déviter le problème de  » mobile goalposts  » ici et de ne pas supposer que simplement parce quun compilateur le fait ou le construit dans le compilateur, ce nest pas une vérification formelle.
• convient que ce nest pas une compréhension commune. les techniques doptimisation créent grosso modo un modèle de comportement de programme, par exemple dune boucle ou dun sous-programme, et optimisent ce modèle, puis génèrent un nouveau code dont léquivalent est prouvé. donc certaines de ces optimisations sont assez sophistiquées pour réorganiser le code & pour moi, elles utilisent des principes de vérification formels. il semble y avoir de nombreux autres exemples de méthodes de vérification formelles dans le compilateur … la question dorigine posait de nombreuses questions différentes comme beaucoup lont noté, je ne tente pas de répondre à toutes les questions qui y sont contenues.
• par le façon quil semble y avoir des principes de vérification formels également utilisés dans le JRE, le moteur dexécution Java, par exemple loptimisation dynamique, etc …
• cest-à-dire  » le rêve de vérification formelle  » mentionnée par filmus ci-dessus, à mon humble avis, une abstraction chimérique, et lindustrie pragmatique / utilitaire / réaliste la reconnaît largement comme telle. les grandes bases de code sont connues depuis des décennies pour avoir intrinsèquement $ x $ bogues / défauts par $ y $ K-lignes de code et cela ne changera jamais peu importe les progrès de la théorie / technologie, cest un fait de nature humaine . et en fait les théorèmes mathématiques créés par lhomme ont les mêmes propriétés, bien que cela ne soit pas largement apprécié!

Peut-être quun vérificateur de modèle peut être utile.

http://alloytools.org/documentation.html Alloy est un vérificateur de modèle .

Une belle présentation expliquant le concept de vérification de modèle avec Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Dans la même famille doutils, il y a les « tests basés sur les propriétés », ils essaient tous de trouver un contre-exemple pour le modèle de spécification donné de votre logiciel.