Was sind die Hindernisse, die eine breite Anwendung formaler Methoden verhindern? [geschlossen]

Formale Methoden können verwendet werden, um Code für eine Anwendung anzugeben, zu beweisen und zu generieren. Dies ist weniger fehleranfällig und wird daher hauptsächlich in sicherheitskritischen Programmen verwendet.

Warum verwenden wir es nicht häufiger für die tägliche Programmierung oder für Webanwendungen usw.?

Verweise :

• Formale Methoden
• B Methode
• Hoare Logic

Ein Ingenieur ist eine Person, die mit einem Dollar machen kann, was jeder Idiot mit 10 machen kann.

Ressourcenbeschränkungen, Budgetbeschränkungen, Zeitbeschränkungen, sie alle sind wichtig.

Das Entwickeln von Software mit formalen Methoden ist in der Regel erheblich teurer und dauert viel länger als ohne. Bei vielen Projekten ist es außerdem am schwierigsten, die Geschäftsanforderungen zu verstehen. Alles, was Sie in diesem Fall mit formalen Methoden kaufen, ist der Beweis, dass Ihr Code zu 100% Ihrem unvollständigen und falschen Verständnis der Geschäftsanforderungen entspricht.

Aus diesem Grund ist die Verwendung formaler Methoden, Beweise, Programmüberprüfungen und ähnlicher Techniken in der Regel auf wichtige Dinge beschränkt, z. B. Avionik-Software, Steuerungssysteme für medizinische Geräte, Kraftwerke usw.

Programmieren oder nicht programmieren?

Um ein Problem mit einem Softwareprodukt zu lösen, können Sie, nachdem Sie die Anforderungen verstanden haben, ENTWEDER ein Programm in Programmiersprachen schreiben ODER das Programm in einer formalen Sprache angeben und Tools zur Codegenerierung verwenden. Letzteres fügt nur eine Abstraktionsebene hinzu.

Die richtigen Dinge tun oder die richtigen Dinge tun?

Der formale Ansatz gibt Ihnen den Beweis, dass Ihre Software den Spezifikationen entspricht. So macht Ihr Produkt die Dinge richtig. Aber macht es die richtigen Dinge?

Die Anforderungen, an denen Sie arbeiten, sind möglicherweise unvollständig oder nicht eindeutig. Sie könnten sogar fehlerhaft sein. Im schlimmsten Fall werden die tatsächlichen Bedürfnisse nicht einmal zum Ausdruck gebracht. Aber ein Bild sagt mehr als tausend Worte, nur Google-Bilder für "Was der Kunde will", zum Beispiel aus diesem Artikel :

Die Kosten der Formalität

In einer perfekten Welt hätten Sie von Anfang an vollständige und perfekte Anforderungen. Sie können dann Ihre Software vollständig spezifizieren. Wenn Sie sich für eine formelle Methode entscheiden, wird Ihr Code automatisch generiert, damit Sie produktiver arbeiten können. Produktivitätsgewinne würden die Kosten der formalen Werkzeuge ausgleichen. Und alle würden jetzt formale Methoden anwenden. Warum ist es nicht so?

In der Praxis ist das selten die Realität! Dies ist der Grund, warum so viele Wasserfallprojekte gescheitert sind und warum iterative Entwicklungsmethoden (Agile, RAD usw.) die Führung übernommen haben: Sie können unvollständige und unvollständige Anforderungen, Entwürfe und Implementierungen verarbeiten und verfeinern, bis sie in Ordnung sind.

Und hier kommt der Punkt. Bei formalen Methoden muss für jede Iteration eine vollständig konsistente formale Spezifikation vorliegen. Dies erfordert sorgfältiges Denken und zusätzliche Arbeit, da formale Logik nicht verzeiht und unvollständige Gedanken nicht mag. Einfache Wegwerfversuche werden unter dieser Bedingung teuer. Und jede Iteration, die zum Zurückverfolgen führen würde (z. B. eine Idee, die nicht funktioniert hat, oder eine Anforderung, die falsch verstanden wurde).

In der Praxis

Wenn Sie aus rechtlichen oder vertraglichen Gründen nicht verpflichtet sind, formale Methoden anzuwenden, können Sie auch ohne formale Systeme eine sehr hohe Qualität erzielen, z. B. durch vertragliche Programmierung und andere bewährte Verfahren (z. B. Code Review, TDD usw.). Sie können nicht nachweisen, dass Ihre Software funktioniert, aber Ihre Benutzer werden früher Freude an der Arbeit mit Software haben.

Update: gemessener Aufwand

In der Oktoberausgabe 2018 von Communications of the ACM gibt es einen interessanten Artikel über formal verifizierte Software in der realen Welt mit einigen Schätzungen des Aufwands.

Interessanterweise (basierend auf der Entwicklung von Betriebssystemen für militärische Ausrüstungen) scheint es, dass die Herstellung formal erprobter Software 3,3-mal mehr Aufwand erfordert als mit herkömmlichen Ingenieurtechniken. Es ist also sehr teuer.

Auf der anderen Seite ist der Aufwand für das Abrufen von Hochsicherheitssoftware auf diese Weise 2,3-mal geringer als bei herkömmlich entwickelter Software, wenn Sie den Aufwand für das Zertifizieren solcher Software auf einem hohen Sicherheitsniveau (EAL 7) erhöhen. Wenn Sie also hohe Zuverlässigkeits- oder Sicherheitsanforderungen haben, gibt es definitiv ein Geschäftsmodell für die formelle Umsetzung.

seL4-Design und Code-Entwicklung dauerten zwei Personenjahre. Die Summe aller serospezifischen Nachweise über die Jahre ergibt insgesamt 18 Personenjahre für 8.700 Zeilen C-Code. Im Vergleich dazu dauerte die Entwicklung von L4Ka :: Pistachio, einem anderen Mikrokern der L4-Familie, der in seiner Größe mit seL4 vergleichbar ist, sechs Personenjahre und bietet kein nennenswertes Maß an Sicherheit. Dies bedeutet, dass zwischen verifizierter Software und herkömmlich entwickelter Software nur ein Faktor 3,3 besteht . Nach der Schätzmethode von Colbert und Boehm 8 würde eine traditionelle Common-Criteria-EAL7-Zertifizierung für 8.700 Zeilen C-Code mehr als 45,9 Personenjahre dauern. Das heißt, die formale Verifizierung der Implementierung auf Binärniveau ist bereits mehr als ein Faktor von 2,3 Dies ist kostengünstiger als die höchste Zertifizierungsstufe von Common Criteria, bietet jedoch eine deutlich höhere Sicherheit.

Jedes Programm in einer beliebigen Sprache kann als formale Spezifikation angesehen werden (entspricht einer Drehmaschine). Jede übergeordnete „formale Spezifikation“ zum Nachweis der formalen Korrektheit ist ebenfalls nur ein weiteres Programm. Aber es ist (normalerweise) ein schlechtes, unvollständiges, vages, unzureichend durchdachtes Programm. Und nicht zufällig, normalerweise von Leuten geschrieben, die nicht wissen, wie man programmiert (normalerweise sind sie Domain-Experten).

Wenn Sie also beweisen, dass ein Programm mit den übergeordneten formalen Anforderungen kompatibel ist (dh die gleichen Antworten liefert oder wie Sie sie charakterisieren), müssen Sie die Mehrdeutigkeiten in der übergeordneten formalen Spezifikation auflösen. Es gibt keinen guten allgemeinen Weg, dies zu tun.

Diese Zuordnung von Anforderungen auf hoher Ebene zu Details auf niedriger Ebene ist der Kern dessen, worum es bei der echten Programmierung geht. Es sollte nicht überraschen, dass die Kernarbeit, die ein Programmierer beim Lesen und Interpretieren von Spezifikationen leistet, nicht durch das Winken von Hand ersetzt werden kann.

Sogar in den Anfängen der Logikprogrammierung, als dieses Konzept zunächst so vielversprechend erschien (weil sowohl die High-Level-Spezifikation als auch die eigentlichen zugrunde liegenden Programme in derselben Sprache geschrieben werden konnten), erwies sich dieses Kernproblem als unlösbar.