Est-ce que les méthodes formelles de programme Verfication ont une place dans l'industrie?
https://stackoverflow.com/questions/1196803
-
20-09-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianQuestion
Je pris un coup d'œil sur Hoare Logic au collège. Ce que nous avons fait était vraiment simple. La plupart de ce que je l'ai fait se révélait l'exactitude des programmes simples de boucles de while, relevés if et séquence d'instructions, mais rien de plus. Ces méthodes semblent très utiles!
Des méthodes formelles utilisées dans l'industrie largement?
sont ces méthodes utilisées pour prouver les logiciels essentiels à la mission?
La solution
Ceci est une question proche de mon coeur (je suis un chercheur dans la vérification du logiciel en utilisant des logiques formelles), de sorte que vous serez probablement pas surpris quand je dis que je pense que ces techniques ont un lieu utile et ne sont pas encore utilisé assez dans l'industrie.
Il y a plusieurs niveaux de « méthodes formelles », donc je suppose que vous voulez dire ceux qui reposent sur une base mathématique rigoureuse (par opposition à, par exemple, après un processus de style 6-Sigma). Certains types de méthodes formelles ont eu un grand succès - les systèmes de type est un exemple. outils d'analyse statique basée sur l'analyse des flux de données sont aussi très populaires, la vérification du modèle est presque omniprésent dans la conception de matériel, et les modèles de calcul comme Pi-calcul et CCS semblent inspirer un changement réel dans la conception pratique de la langue pour la concurrence. analyse de résiliation est celui qui a eu beaucoup de presse récemment -. Le projet de SDV à Microsoft et le travail de Byron Cook sont des exemples récents de la recherche / pratique croisée dans les méthodes formelles
Hoare Raisonnement n'a pas, jusqu'à présent, fait une percée importante dans l'industrie - c'est pour plus de raisons que je ne peux énumérer, mais je soupçonne est la plupart du temps autour de la complexité de l'écriture puis prouvant les spécifications des programmes réels (ils ont tendance à obtenir < em> grand , et ne parviennent pas à exprimer des propriétés de nombreux environnements du monde réel). Divers sous-domaines dans ce type de raisonnement sont en train de faire de grandes avancées dans ces problèmes -. La séparation logique étant un
Ceci est en partie la nature de la recherche en cours (dur). Mais je dois avouer que nous, comme les théoriciens, ont complètement échoué à éduquer l'industrie pourquoi nos techniques sont utiles, pour les garder adaptés aux besoins de l'industrie, et de les rendre accessibles aux développeurs de logiciels. À un certain niveau, ce n'est pas notre problème - nous sommes des chercheurs, souvent mathématiciens, et l'utilisation pratique n'est pas avant tout dans nos esprits. En outre, les techniques en cours d'élaboration sont souvent trop embryonnaires pour une utilisation dans les grands systèmes à grande échelle - nous travaillons sur de petits programmes, sur les systèmes simplifiés, obtenir le travail de mathématiques, et de progresser. Je ne crois pas beaucoup ces excuses si -. Nous devrions être plus actifs à pousser nos idées, et d'obtenir une boucle de rétroaction entre l'industrie et notre travail (l'une des principales raisons pour lesquelles je suis retourné à la recherche)
Il est probablement une bonne idée pour moi de ressusciter mon blog, et faire quelques posts sur ce genre de choses ...
Autres conseils
Eh bien, Sir Tony Hoare a rejoint Microsoft Research il y a environ 10 ans, et l'une des choses qu'il a commencé était une vérification formelle du noyau Windows NT. En effet, ce fut l'une des raisons du retard de Windows Vista: à partir de Vista, une grande partie du noyau sont en fait officiellement vérifié WRT. à certaines propriétés comme absence de blocages, l'absence de fuites d'informations etc.
Ceci est certainement pas typique, mais il est probablement l'application la plus importante de la vérification formelle du programme, en termes de son impact (après tout, presque chaque être humain est en quelque sorte, ou de forme affectée par un ordinateur exécutant Windows ).
Je ne peux pas commenter beaucoup sur les logiciels critiques, bien que je sache que l'industrie avionique utilise une grande variété de techniques de validation des logiciels, y compris les méthodes de style Hoare.
Les méthodes formelles ont souffert parce que les premiers défenseurs comme Edsger Dijkstra ont insisté qu'ils doivent être utilisés partout. Ni les formalismes ni le soutien du logiciel ont été à la hauteur. les défenseurs plus sensibles croient que ces méthodes devraient être utilisées sur les problèmes qui sont difficiles. Ils ne sont pas largement utilisés dans l'industrie, mais l'adoption est en augmentation. Probablement les plus grandes avancées ont été dans l'utilisation des méthodes formelles pour vérifier propriétés de sécurité de logiciels. Certains de mes exemples préférés sont les SPIN modèle vérificateur et le code de validation comptable de George Necula.
L'abandon de la pratique et dans la recherche, Singularity système d'exploitation de Microsoft projet sur l'utilisation des méthodes formelles pour fournir des garanties de sécurité qui nécessitent habituellement un support matériel. Cela conduit à des performances et des garanties plus élevées plus rapidement. Par exemple, dans la singularité, ils ont prouvé que si un pilote de périphérique tiers est autorisé dans le système (ce qui signifie que les conditions de vérification de base ont été prouvé), il ne peut peut-être faire baisser que tout OS-il le pire qu'il peut faire est flexible son propre appareil.
Les méthodes formelles ne sont pas encore largement utilisés dans l'industrie, mais ils sont plus largement utilisés qu'ils ne l'étaient il y a 20 ans, et 20 ans à partir de maintenant, ils seront utilisés plus largement encore. Donc, vous êtes l'avenir imperméabilisé: -)
Oui, ils sont utilisés, mais pas largement dans tous les domaines. Il y a plus de méthodes que la logique juste Hoare, certains sont utilisés plus, d'autres moins, en fonction de l'aptitude à la tâche donnée. Le problème commun est que sofware est biiiiiiig et à vérifier que tout cela est correct est encore trop dur un problème.
Par exemple, le théorème prouveur (un logiciel qui aide les humains à prouver la pertinence du programme) ACL2 a été utilisé pour prouver qu'une certaine unité de traitement à virgule flottante ne dispose pas d'un certain type de bogue. Ce fut une grande tâche, si cette technique est trop commun.
vérification du modèle, un autre type de vérification formelle, est utilisé assez largement de nos jours, par exemple Microsoft fournit un type de vérificateur de modèle dans le kit de développement de pilotes et il peut être utilisé pour vérifier le pilote pour un ensemble de bugs communs. dames modèles sont souvent utilisés pour la vérification des circuits matériels.
Des tests rigoureux peut également être considéré comme une vérification formelle -. Il y a des spécifications formelles dont les chemins de programme devraient être testés et ainsi de suite
"Les méthodes sont-formelles utilisées dans l'industrie?"
Oui.
La déclaration de assert dans de nombreux langages de programmation est liée aux méthodes formelles de vérification d'un programme.
"Des méthodes formelles utilisées dans l'industrie largement?"
Non.
« que ces méthodes sont utilisées pour prouver les logiciels essentiels à la mission? »
Parfois. Le plus souvent, ils sont utilisés pour prouver que le logiciel est sécurisé. Plus formellement, ils sont utilisés pour prouver certaines affirmations relatives à la sécurité sur le logiciel.
Il existe deux approches différentes méthodes formelles dans l'industrie.
Une approche consiste à modifier le processus de développement complètement. La notation Z et la méthode B qui ont été mentionnés sont dans cette première catégorie. B a été appliquée au développement de la ligne de métro sans conducteur 14 à Paris (si vous obtenez une chance, monter dans le wagon avant. Il est rare que vous obtenez une chance de voir les rails devant vous).
Une autre, plus progressive, l'approche est de préserver les processus de développement et de vérification existants et de ne remplacer que l'une des tâches de vérification à la fois par une nouvelle méthode. Ceci est très attrayant, mais cela signifie que le développement d'outils d'analyse statique pour la sortie, les langues utilisées qui sont souvent difficiles à analyser (car ils ne sont pas conçus pour être). Si vous allez à (par exemple)
http: //dblp.uni -trier.de/db/indices/a-tree/d/Delmas:David.html
(désolé, un seul lien hypertexte autorisé pour les nouveaux utilisateurs :()
vous trouverez des instances d'applications pratiques des méthodes formelles pour la vérification des programmes C (avec Astrée analyseurs statiques, caveat, Fluctuat, Frama-C) et le code binaire (avec des outils de AbsInt GmbH).
Par ailleurs, puisque vous avez mentionné la logique de Hoare, dans la liste ci-dessus des outils, seule réserve est basé sur la logique de Hoare (et Frama-C est un plug-in logique Hoare). Les autres reposent sur l'interprétation abstraite, une technique différente avec une approche plus automatique.
Mon domaine d'expertise est l'utilisation des méthodes formelles pour l'analyse de code statique pour montrer que le logiciel est exempt d'erreurs d'exécution. Ceci est mis en œuvre en utilisant une technique de méthodes formelles connues « interprétation abstraite ». La technique permet essentiellement de prouver certaines atributs d'un programme s / p. Par exemple. prouver que a + b ne sera pas déborder ou x / (x-y) ne résultera pas en une division par zéro. Un exemple outil d'analyse statique qui utilise cette technique est Polyspace.
En ce qui concerne votre question: "? Des méthodes formelles utilisées dans l'industrie largement" et "? Que ces méthodes sont utilisées pour prouver les logiciels critiques de mission"
La réponse est oui. Cette opinion est fondée sur mon expérience et le soutien de l'outil Polyspace pour les industries qui dépendent de l'utilisation des logiciels embarqués pour contrôler la sécurité des systèmes critiques tels que l'accélérateur électronique dans une automobile, un système de freinage d'un train, contrôleur de moteur à réaction, pompe à perfusion de l'administration de médicaments, etc. ces industries n'utilisent en effet ces types d'outils de méthodes formelles.
Je ne crois pas que tous les 100% de ces segments de l'industrie utilisent ces outils, mais l'utilisation augmente. Mon opinion est que les industries aéronautique et l'automobile mènent avec l'industrie des dispositifs médicaux montée en puissance rapidement utilisation.
Polyspace est aa (horriblement cher, mais très bon) produit commercial basé sur le programme vérification. Il est assez pragmatique, en ce qu'elle adapte à partir « amélioration des tests unitaires qui probablement quelques bugs » à « les trois prochaines années de votre vie seront dépensés montrant ces 10 fichiers ont zéro défaut ».
Il est basé sur la vérification plus négative ( «ce programme ne sera pas corrompre votre pile) de vérification plutôt positive ( « ce programme va faire précisément ce que ces 50 pages d'équations disent qu'il »).
En plus d'autres approches plus de procédure, la logique de Hoare était dans la base de Conception par contrat , présenté comme une technique orientée objet par Bertrand Meyer dans Eiffel ( voir l'article de Meyer de 1992 , page 4). Bien que la conception par contrat ne sont pas les mêmes que les méthodes de vérification formelles (pour une chose, DBC ne prouver quoi que ce soit jusqu'à ce que le logiciel est exécuté), à mon avis, il fournit une utilisation plus pratique.
