Formale Programmüberprüfung in der Praxis

Ich werde versuchen, einige Ihrer Fragen kurz und bündig zu beantworten.Bitte beachten Sie, dass dies nicht ausschließlich mein Forschungsgebiet ist, sodass einige meiner Informationen möglicherweise veraltet / falsch sind.

1. Es gibt viele Tools, die speziell zum formalen Nachweis von Eigenschaften entwickelt wurden von Java und C ++.

   Allerdings muss ich hier einen kleinen Exkurs machen: Was bedeutet es, die Richtigkeit eines Programms zu beweisen? Die Java-Typprüfung beweist eine formale Eigenschaft eines Java-Programms, nämlich dass bestimmte Fehler, wie das Hinzufügen einer float und einer int, niemals auftreten können auftreten! Ich stelle mir vor, Sie interessieren sich für viel stärkere Eigenschaften, nämlich dass Ihr Programm niemals in einen unerwünschten Zustand eintreten kann oder dass die Ausgabe einer bestimmten Funktion einer bestimmten mathematischen Spezifikation entspricht. Kurz gesagt, es gibt einen großen Gradienten dessen, was „ein Programm als korrekt beweisen“ bedeuten kann, von einfachen Sicherheitseigenschaften bis zu einem vollständigen Beweis, dass das Programm eine detaillierte Spezifikation erfüllt.

   Nun gehe ich davon aus Sie sind daran interessiert, starke Eigenschaften Ihrer Programme zu beweisen. Wenn Sie an Sicherheitseigenschaften interessiert sind (Ihr Programm kann einen bestimmten Status nicht erreichen), scheint im Allgemeinen der beste Ansatz Modellprüfung . Wenn Sie jedoch das Verhalten eines Java-Programms vollständig spezifizieren möchten, verwenden Sie am besten eine Spezifikationssprache für diese Sprache, z. B. JML . Es gibt solche Sprachen zum Spezifizieren des Verhaltens von C-Programmen, zum Beispiel ACSL , aber ich weiß nichts darüber C ++.

2. Sobald Sie Ihre Spezifikationen haben, müssen Sie nachweisen, dass das Programm dieser Spezifikation entspricht.

   Dazu benötigen Sie ein Tool mit einem formales Verständnis von beiden Ihre Spezifikation und die operative Semantik Ihrer Sprache (Java oder C ++), um den -Angemessenheitssatz auszudrücken, nämlich die Ausführung des Programms berücksichtigt die Spezifikation.

   Mit diesem Tool sollten Sie auch den Beweis dieses Satzes formulieren oder generieren können. Jetzt sind diese beiden Aufgaben (Spezifizieren und Beweisen) ziemlich schwierig, so dass sie oft in zwei Teile unterteilt sind:

   • Ein Tool, das den Code analysiert, die Spezifikation und den Angemessenheitssatz generiert. Wie Frank erwähnte, ist Krakatoa ein Beispiel für ein solches Werkzeug.

   • Ein Werkzeug, das den Satz beweist ( s) automatisch oder interaktiv. Coq interagiert auf diese Weise mit Krakatoa, und es gibt einige leistungsstarke automatisierte Tools wie Z3 , die ebenfalls verwendet werden können.

   Ein (kleiner) Punkt: Es gibt einige Theoreme, die viel zu schwer mit automatisierten Methoden zu beweisen sind, und es ist bekannt, dass automatische Theoremprüfer gelegentlich Soliditätsfehler aufweisen, die sie weniger vertrauenswürdig machen. Dies ist ein Bereich, in dem Coq im Vergleich glänzt (aber nicht automatisch!).

3. Wenn Sie Ocaml-Code generieren möchten, schreiben Sie auf jeden Fall zuerst in Coq (Gallina). Extrahieren Sie dann den Code. Coq ist jedoch schrecklich darin, C ++ oder Java zu generieren, wenn es überhaupt möglich ist.

4. Können die oben genannten Tools Threading- und Leistungsprobleme lösen? Wahrscheinlich nicht. Leistungs- und Threadingprobleme werden am besten von speziell entwickelten Tools gelöst, da sie besonders schwierige Probleme darstellen. Ich bin mir nicht sicher, ob ich hier Tools empfehlen kann, obwohl Martin Hofmanns PolyNI -Projekt interessant erscheint.

Fazit: Die formale Überprüfung von Java- und C ++ – Programmen in der „realen Welt“ ist ein großes und gut entwickeltes Feld, und Coq eignet sich für Teile dieser Aufgabe. Eine allgemeine Übersicht finden Sie hier zum Beispiel.

Kommentare

• Danke für diesen Beitrag und die Referenzen, die Sie hinzugefügt haben. Meiner Meinung nach besteht das Ziel für Softwareentwickler darin, Systeme, die 1) immer korrekte Ergebnisse liefern, 2) niemals versagen, schnell freizugeben. Ich könnte hier ein Regressionsproblem sehen, bei dem Sie möglicherweise beweisen möchten, dass die Spezifikation selbst “ fehlerfrei “ 🙂 ist wie der Versuch, “ wahrer Satz einer Sprache “ mit einer Metasprache zu definieren und dann eine andere Metasprache dafür zu benötigen, dann eine andere one …
• Das Problem ist, dass das, was der Benutzer “ “ möchte, normalerweise nicht formell ausgedrückt wird Sprache! Es gibt im Allgemeinen keine formale Antwort auf die Frage: “ Entspricht diese formale Spezifikation meiner informellen Idee? „. ‚ ist es möglich, eine formale Spezifikation zu testen und zu beweisen, dass sie bestimmte mathematische Eigenschaften hat, aber letztendlich müssen Sie die Mathematik mit der realen Welt in Beziehung setzen. Das ist ein nicht formaler Prozess.
• Ja natürlich – ich habe immer erkannt, dass die formalen Methoden nur an einem genau definierten Punkt beginnen können.Ob diese Spezifikation den bewussten / unbewussten / unentdeckten Bedürfnissen realer Benutzer entspricht oder nicht, ist ein weiteres Problem, das mit formalen Methoden nicht angegangen werden kann (aber sicherlich ein Problem für Ingenieure).
• Ein Theorem ist per Definition a bewiesener Vorschlag. Sie wollen also wahrscheinlich nicht “ den Satz “ beweisen.
• @nbro Wikipedia scheint dem zuzustimmen mit dir. Mathworld definiert einen Satz jedoch als einen Satz, von dem “ durch akzeptierte mathematische Operationen „. In diesem Fall ist es nicht nur möglich, Beweise für Theoreme zu liefern, sondern auch notwendig, um sie so zu nennen! 🙂 (dies ist natürlich ein Gegenproblem)

Ich möchte drei bemerkenswerte Anwendungen erwähnen von formalen Methoden / formalen Verifizierungswerkzeugen in der Industrie oder nicht trivialen realen Systemen. Beachten Sie, dass ich wenig Erfahrung mit diesem Thema habe und sie nur durch das Lesen von Artikeln lerne.

1. Das Open-Source-Tool Java Pathfinder (kurz JPF) , veröffentlicht von der NASA im Jahr 2005 ist ein System zur Überprüfung ausführbarer Java-Bytecode-Programme (siehe Java Pathfinder @ wiki ). Es wurde verwendet, um Inkonsistenzen in der Executive-Software für den K9 Rover bei der NASA Ames zu erkennen.

2. Dieses Dokument: Verwenden der Modellprüfung zum Auffinden schwerwiegender Dateisystemfehler @ OSDI „04 zeigt die Verwendung Modellprüfung, um schwerwiegende Fehler in Dateisystemen zu finden. Ein System namens FiSC wird auf drei weit verbreitete, stark getestete Dateisysteme angewendet: ext3, JFS und ReiserFS. Es wurden 32 schwerwiegende Fehler gefunden. Es wurde mit dem Best Paper Award ausgezeichnet / p>

3. In diesem Dokument: Wie Amazon Web Services formale Methoden @ CACM verwendet „15 wird beschrieben, wie AWS formale Methoden anwendet seine Produkte wie S3, DynamoDB, EBS und Internal Distributed Lock Manager. Es konzentriert sich auf das TLA + -Tool von Lamport. Übrigens hat Lamport seine eigene TLA-Toolbox intensiv genutzt. In TLA gibt er häufig eine (ziemlich vollständige) formale Überprüfung der von ihm (sowie den Mitautoren) in den Anhängen zu den Abhandlungen vorgeschlagenen Algorithmen / Theoreme.

Eine formelle Die Spezifikation eines Programms ist (mehr oder weniger) ein Programm, das in einer anderen Programmiersprache geschrieben ist. Infolgedessen enthält die Spezifikation sicherlich ihre eigenen Fehler.

Der Vorteil der formalen Überprüfung besteht darin, dass das Programm und die Spezifikation zwei separate Implementierungen sind und ihre Fehler unterschiedlich sind. Aber nicht immer: Eine häufige Fehlerquelle, übersehene Fälle, wird häufig übereinstimmen. Daher ist die formale Überprüfung kein Allheilmittel: Sie kann immer noch eine nicht triviale Anzahl von Fehlern übersehen.

Ein Nachteil der formalen Überprüfung besteht darin, dass sie etwa das Doppelte der Implementierungskosten verursachen kann, wahrscheinlich mehr (Sie benötigen) Sie sind ein Spezialist für formale Spezifikationen, und Sie müssen die mehr oder weniger experimentellen Werkzeuge verwenden, die mitgeliefert werden (die nicht billig sind).

Ich würde vermuten, Testfälle und Gerüste einzurichten, um sie auszuführen automatisch wäre eine bessere Nutzung Ihrer Zeit.

Kommentare

• Der Vorteil der formalen Überprüfung ist, dass … Ein zweiter Nachteil der formalen Überprüfung besteht darin, dass … dies verwirrend ist.
• Ich denke, dass die Nichtübereinstimmung zwischen Spezifikation und informeller Aufgabe ein Problem der Softwareanforderungsanalyse und kein Programmierproblem ist.

Sie stellen einige verschiedene Fragen. Ich stimme zu, dass formale Überprüfungsmethoden für industrielle / kommerzielle Anwendungen anscheinend nicht so häufig sind. Man sollte jedoch erkennen, dass viele „formale Verifizierungs“ -Prinzipien in Compiler eingebaut sind, um die Programmkorrektheit zu bestimmen! Wenn Sie also einen modernen Compiler verwenden, verwenden Sie in gewisser Weise einen Großteil des Standes der Technik bei der formalen Verifizierung.

Sie sagen „Ich bin es leid zu testen“, aber die formale Verifizierung ist nicht wirklich ein Ersatz für das Testen. In gewisser Weise ist es eine Variation beim Testen.

Sie erwähnen Java.Es gibt viele erweiterte formale Überprüfungsmethoden, die in ein Java-Überprüfungsprogramm namens FindBugs integriert sind und tatsächlich über große Codebasen ausgeführt werden können. Beachten Sie, dass sowohl „falsch positive als auch falsch negative“ angezeigt werden und die Ergebnisse von einem menschlichen Entwickler überprüft / analysiert werden müssen. Beachten Sie jedoch, dass selbst wenn keine echten Funktionsfehler auftreten, im Allgemeinen „Antimuster“ auftreten, die im Code ohnehin vermieden werden sollten.

Sie erwähnen Ihre spezielle Anwendung nur „industriell“. . Die formale Verifikation hängt in der Praxis tendenziell von der jeweiligen Anwendung ab.

Formale Verifikationstechniken scheinen in EE weit verbreitet zu sein, um die Schaltungskorrektheit zu beweisen, z. im Mikroprozessor-Design.

Hier ist ein Beispiel für eine Übersicht über formale Verifizierungswerkzeuge im EE-Bereich durch Lars Philipson .

Kommentare

• ‚ ist irreführend zu sagen, dass “ a Viele “ formale Überprüfung “ Prinzipien sind in Compiler integriert, um die Programmkorrektheit zu bestimmen „. Sie beziehen sich auf die statische Typprüfung, die einige Compiler durchführen, aber die auf diese Weise verifizierten Eigenschaften sind ziemlich einfach, z. Vermeiden Sie das Hinzufügen einer Zahl und einer Zeichenfolge. Dies ist hilfreich, aber weit entfernt von dem, was normalerweise von “ formale Überprüfung “ verstanden wird.
• nicht Beziehen Sie sich speziell auf die statische Typprüfung, obwohl dies ein einfaches / allgemeines Beispiel ist. Imho-Compiler-Optimierungstechniken, die weit verbreitet und fortgeschritten sind, ähneln in etwa den formalen Verifizierungsprinzipien, da sie fortgeschrittene Techniken umfassen, um die Gleichwertigkeit optimierter Programmvarianten zu bestimmen / zu zeigen. Daher scheint es wichtig zu sein, das Problem “ bewegliche Torpfosten “ hier zu vermeiden und dies nicht anzunehmen, nur weil ein Compiler es tut oder es erstellt in den Compiler, seine nicht formale Überprüfung.
• stimmte zu, dass dies kein allgemeines Verständnis ist. Die Optimierungstechniken erstellen grob ein Modell des Programmverhaltens, z. B. einer Schleife oder eines Unterprogramms, optimieren dieses Modell und generieren dann neuen Code, der nachweislich gleichwertig ist. Einige dieser Optimierungen sind daher sehr komplex, wenn es darum geht, Code & neu anzuordnen. Für mich verwenden sie formale Überprüfungsprinzipien. Es scheint viele andere Beispiele für formale Überprüfungsmethoden im Compiler zu geben … Die ursprüngliche Frage stellte viele verschiedene Fragen, wie viele bemerkt haben. Ich versuche definitiv nicht, alle darin enthaltenen Fragen zu beantworten.
• von der Auf diese Weise scheint es einige formale Überprüfungsprinzipien zu geben, die auch in der JRE, der Java-Laufzeit-Engine, z. B. der dynamischen Optimierung usw. verwendet werden.
• das ist “ the ch träume von einer formalen Verifikation „, auf die der Filmus oben Bezug genommen hat, imho eine chimäre Abstraktion, und die pragmatische / utilitaristische / realistische Industrie erkennt sie weitgehend als solche an. Es ist seit Jahrzehnten bekannt, dass große Codebasen von Natur aus $ x $ Bugs / Defekte pro $ y $ K-Codezeilen aufweisen, und dies wird sich niemals ändern, egal wie die Theorie / Technologie voranschreitet, es ist eine Tatsache von menschliche Natur. und tatsächlich haben vom Menschen geschaffene mathematische Theoreme die gleichen Eigenschaften, obwohl dies nicht allgemein anerkannt wird!

Möglicherweise ist eine Modellprüfung hilfreich.

http://alloytools.org/documentation.html Alloy ist eine Modellprüfung

Eine schöne Präsentation, die das Konzept der Modellprüfung mit Alloy erklärt: https://www.youtube.com/watch?v=FvNRlE4E9QQ

In derselben Werkzeugfamilie gibt es „eigenschaftsbasiertes Testen“. Alle versuchen, ein Gegenbeispiel für das angegebene Spezifikationsmodell Ihrer Software zu finden.