Haben formale Methoden der Programmverfikation einen Platz in der Industrie?

StackOverflow https://stackoverflow.com/questions/1196803

Frage

Ich habe einen Blick darauf geworfen Hoare Logik im College. Was wir getan haben, war wirklich einfach. Das meiste, was ich getan habe while Schleifen, if Aussagen und Anweisungen, aber nichts weiter. Diese Methoden scheinen sehr nützlich zu sein!

Werden formale Methoden in der Industrie weit verbreitet?

Werden diese Methoden verwendet, um eine missionskritische Software zu beweisen?

War es hilfreich?

Lösung

Dies ist eine Frage, die mir am Herzen liegt (ich bin ein Forscher in der Softwareverifizierung unter Verwendung formaler Logik), daher werden Sie wahrscheinlich nicht überrascht sein, wenn ich sage, dass diese Techniken einen nützlichen Ort haben und noch nicht genug verwendet werden. Industrie.

Es gibt viele Ebenen von "formalen Methoden", also gehe ich davon aus, dass Sie diejenigen meinen, die auf einer strengen mathematischen Basis ruhen (im Gegensatz zu beispielsweise nach einem 6-Sigma-Stilprozess). Einige Arten von formalen Methoden hatten großen Erfolg - Typsysteme sind ein Beispiel. Auch statische Analyse-Tools, die auf der Datenflussanalyse basieren, sind ebenfalls beliebt, die Modellprüfung ist bei Hardwaredesign nahezu allgegenwärtig, und Computermodelle wie Pi-Kalkulus und CCs scheinen eine echte Veränderung des praktischen Sprachdesigns für die Parallelität zu inspirieren. Die Terminierungsanalyse hat in letzter Zeit viel Presse - das SDV -Projekt bei Microsoft und Arbeit von Byron Cook sind aktuelle Beispiele für Forschungs-/Praxis -Crossover bei formalen Methoden.

Hoare -Argumentation hat in der Branche bisher nicht große Einführung erzielt - dies ist aus mehr Gründen, als ich auflisten kann, aber ich vermute, dass es hauptsächlich um die Komplexität des Schreibens geht und dann Spezifikationen für echte Programme beweist (sie bekommen dazu, zu bekommen groß, und keine Eigenschaften vieler realer Weltumgebungen ausdrücken). Verschiedene Unterfelder in dieser Art von Argumentation machen nun einen großen Einfluss auf diese Probleme - die Trennungslogik ist eins.

Dies ist teilweise die Natur der laufenden (harten) Forschung. Aber ich muss gestehen, dass wir als Theoretiker die Branche völlig versäumt haben, warum unsere Techniken nützlich sind, um sie für die Industrieanforderungen relevant zu halten und sie für Softwareentwickler zugänglich zu machen. In gewisser Hinsicht ist das nicht unser Problem - wir sind Forscher, oft Mathematiker, und der praktische Gebrauch ist in unseren Köpfen nicht vor allem. Außerdem sind die Techniken, die entwickelt werden, häufig zu embryonal, um in großen Systemen verwendet zu werden. Wir arbeiten an kleinen Programmen, an vereinfachten Systemen, lassen sich mathematisch arbeiten und gehen weiter. Ich kaufe diese Ausreden jedoch nicht viel - wir sollten uns aktiver für unsere Ideen und eine Feedback -Schleife zwischen der Branche und unserer Arbeit machen (einer der Hauptgründe, warum ich wieder recherchiert habe).

Es ist wahrscheinlich eine gute Idee für mich, mein Weblog wiederzubeleben und weitere Beiträge zu diesem Zeug zu machen ...

Andere Tipps

Nun, Sir Tony Hoare kam vor ungefähr 10 Jahren zu Microsoft Research, und eines der Dinge, die er begann, war eine formelle Überprüfung des Windows NT -Kernels. In der Tat war dies einer der Gründe für die lange Verzögerung von Windows Vista: beginnend mit Vista, großen Teilen des Kernels sind Eigentlich formell überprüft WRT. Für bestimmte Eigenschaften wie das Fehlen von Deadlocks, Abwesenheit von Informationslecks usw.

Dies ist sicherlich nicht typisch, aber es ist wahrscheinlich die wichtigste Anwendung der formalen Programmüberprüfung in Bezug auf seine Auswirkungen (schließlich ist fast jeder Mensch in irgendeiner Weise, Form oder Form, die von einem Computer betroffen ist).

Ich kann nicht viel zur missionskritischen Software kommentieren, obwohl ich weiß, dass die Avionikindustrie eine Vielzahl von Techniken verwendet, um Software zu validieren, einschließlich Methoden im Hoare-Stil.

Formale Methoden haben gelitten, weil frühe Befürworter wie Edsger Dijkstra darauf bestanden, dass sie überall verwendet werden sollten. Weder die Formalismen noch die Softwareunterstützung legten dem Job zu. Vernünftigere Befürworter glauben, dass diese Methoden für schwierige Probleme angewendet werden sollten. Sie werden in der Industrie nicht weit verbreitet, aber die Akzeptanz nimmt zu. Wahrscheinlich waren die größten Einstiegsroten in der Verwendung formaler Methoden zum Überprüfen Sicherheitseigenschaften von Software. Einige meiner Lieblingsbeispiele sind die DREHEN Model Checker und George Neculas Proof-Tragcode.

Microsoft von der Praxis und in Forschung entfernen Singularität Bei Betriebssystemprojekten geht es darum, formelle Methoden zu verwenden, um Sicherheitsgarantien zu gewährleisten, die normalerweise Hardwareunterstützung erfordern. Dies führt wiederum zu einer schnelleren Leistung und stärkeren Garantien. In der Singularität haben sie beispielsweise bewiesen, dass wenn ein Gerätetreiber von Drittanbietern in das System zugelassen ist (was bedeutet, dass grundlegende Verifizierungsbedingungen nachgewiesen wurden), kann er möglicherweise nicht dieses ganze Betriebssystem senken-das Schlimmste kann es tun, wenn er seine lockern kann. eigenes Gerät.

Formale Methoden werden in der Industrie noch nicht weit verbreitet, aber sie werden weiterhin genutzt als vor 20 Jahren, und in 20 Jahren werden sie noch immer mehr genutzt. Sie sind also zukunftssicher :-)

Ja, sie werden verwendet, aber in allen Bereichen nicht weit verbreitet. Es gibt mehr Methoden als nur Hoare -Logik, einige werden je nach Eignung für eine bestimmte Aufgabe mehr, einige weniger verwendet. Das häufigste Problem ist, dass Sofware biiiiiiig ist und zu überprüfen, ob alles richtig ist, ist immer noch zu schwierig.

Zum Beispiel wurde der Theorem-Prover (eine Software, die Menschen bei der Nachweis der Korrektheit der Programme unterstützt) ACL2 verwendet, um zu beweisen, dass eine bestimmte Verarbeitungseinheit mit Gleitpunkte keine bestimmte Art von Fehler aufweist. Es war eine große Aufgabe, daher ist diese Technik nicht allzu häufig.

Die Modellüberprüfung, eine andere Art von formeller Überprüfung, wird heutzutage eher weit verbreitet. Zum Beispiel bietet Microsoft im Fahrerentwicklungskit eine Art von Modellprüfer und kann verwendet werden, um den Treiber für eine Reihe gemeinsamer Fehler zu überprüfen. Modellprüfer werden auch häufig zur Überprüfung von Hardware -Schaltkreisen verwendet.

Rigorose Tests können auch als formale Überprüfung angesehen werden - es gibt einige formale Spezifikationen, von denen die Programmwege getestet werden sollten und so weiter.

"Werden formale Methoden in der Industrie verwendet?"

Ja.

Das assert Die Aussage in vielen Programmiersprachen bezieht sich auf formale Methoden zur Überprüfung eines Programms.

"Werden formale Methoden in der Industrie weit verbreitet?"

Nein.

"Sind diese Methoden verwendet, um eine missionskritische Software zu beweisen?"

Manchmal. Häufiger werden sie beweisen, dass die Software sicher ist. Formal werden sie bestimmte sicherheitsrelevante Behauptungen über die Software beweisen.

In der Branche gibt es zwei verschiedene Ansätze für formale Methoden.

Ein Ansatz besteht darin, den Entwicklungsprozess vollständig zu ändern. Die Z -Notation und die erwähnte B -Methode befinden sich in dieser ersten Kategorie. B wurde auf die Entwicklung der fahrerlosen U -Bahn -Linie 14 in Paris angewendet (wenn Sie eine Chance haben, klettern Sie in den Vorderwagen. Sie haben nicht oft die Chance, die Schienen vor sich zu sehen).

Ein weiterer, inkrementellerer Ansatz besteht darin, die vorhandenen Entwicklungs- und Überprüfungsprozesse zu erhalten und nur eine der Überprüfungsaufgaben durch eine neue Methode zu ersetzen. Dies ist sehr attraktiv, bedeutet jedoch, statische Analyse -Tools zum Ausgangssprachen zu entwickeln, die häufig nicht einfach zu analysieren sind (weil sie nicht ausgelegt waren). Wenn Sie zu (zum Beispiel) gehen

http://dblp.uni-trier.de/db/indices/a-- tree/d/delmas:david.html

(Entschuldigung, nur ein Hyperlink erlaubte neue Benutzer :()

Sie finden Beispiele für praktische Anwendungen formeller Methoden zur Überprüfung von C-Programmen (mit statischen Analysatoren Astée, Vorbehalt, Fluktuat, Frama-C) und Binärcode (mit Tools aus Absint GmbH).

Da Sie Hoare Logic erwähnt haben, basiert in der obigen Liste der Tools nur der Vorbehalt auf Hoare-Logik (und Frama-C verfügt über ein Hoare-Logik-Plug-In). Die anderen verlassen sich auf abstrakte Interpretation, eine andere Technik mit einem automatischeren Ansatz.

Mein Fachgebiet ist die Verwendung formaler Methoden für die statische Codeanalyse, um zu zeigen, dass Software frei von Laufzeitfehlern ist. Dies wird unter Verwendung einer formalen Methodentechnik implementiert, die "abstrakte Interpretation" bekannt ist. Die Technik ermöglicht es Ihnen im Wesentlichen, bestimmte Atributes des AS/W -Programms zu beweisen. ZB beweisen, dass A+B nicht überflutet oder x/(xy) nicht zu einer Kluft um Null führt. Ein Beispiel für statisches Analyse, das diese Technik verwendet, ist Polyspace.

In Bezug auf Ihre Frage: "Werden formale Methoden in der Industrie weit verbreitet?" und "Sind diese Methoden verwendet, um eine missionskritische Software zu beweisen?"

Die Antwort ist ja. Diese Meinung basiert auf meiner Erfahrung und der Unterstützung des Polyspace -Tools für Branchen, die sich auf die Verwendung von eingebetteter Software verlassen, um sicherheitskritische Systeme wie elektronische Gas in einem Automobil, Bremssystem für einen Zug, Jet Engine -Controller, Infusionspumpe für Arzneimittelablieferung zu steuern, Infusionspumpe. usw. Diese Branchen verwenden in der Tat diese Arten von Tools für formale Methoden.

Ich glaube nicht, dass alle 100% dieser Branchensegmente diese Tools verwenden, aber die Verwendung nimmt zu. Ich bin der Meinung, dass die Luft- und Raumfahrt- und Automobilindustrie mit der Medizinproduktbranche die Verwendung schnell erhöhen.

Polyspace ist AA (schrecklich teuer, aber sehr gut) kommerzielles Produkt basierend auf der Programmüberprüfung. Es ist ziemlich pragmatisch, da es sich von "erweiterten Unit -Tests, die wahrscheinlich einige Fehler finden" bis zu "Die nächsten drei Jahre Ihres Lebens finden, verbracht werden, die gezeigt werden, dass diese 10 Dateien keine Defekte haben".

Es basiert mehr auf der negativen Überprüfung ('Dieses Programm wird Ihren Stapel nicht verfälscht) statt einer positiven Überprüfung (' dieses Programm wird genau das tun, was diese 50 Seiten von Gleichungen sagen, ').

Zu Jorgs ergänzen Antworten, Hier ist ein Interview mit Tony Hoare. Die Tools, auf die Jorg bezieht, sind meiner Meinung nach voreinsteuert und Präfix. Sehen hier für mehr Informationen.

Neben anderen prozeduraleren Ansätzen lag die Hoare -Logik in der Grundlage von Entwurf durch Vertrag, eingeführt als objektorientierte Technik von Bertrand Meyer in Eiffel (Siehe Meyers Artikel von 1992, Seite 4). Während das Design durch Vertrag nicht gleich ist wie formale Überprüfungsmethoden (zum einen, nicht die DBC nicht beweisen Alles, bis die Software ausgeführt wird), bietet sie meiner Meinung nach eine praktischere Verwendung.

Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit StackOverflow
scroll top