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

13

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 :

toto
quelle
3
Wir könnten Häuser mit 5 Fuß dicken Mauern bauen - wie mittelalterliche Schlösser. Meistens wäre das mehr Mühe, als es wert ist.
Baldrickk
5
Sie können versuchen, formale Methoden auf ein Webentwicklungsprojekt anzuwenden, und sehen, wie es funktioniert. Höchstwahrscheinlich werden Sie bemerken, dass Sie viel Mühe in eine Aktivität mit geringem Wert stecken. Vergleichen Sie dies mit einem schnellen Rauchtest, der bereits viele Bugs erkennt. Interessanterweise sind statische Typsysteme eine einfache Art von Proofsystem, aber insbesondere die Webentwicklung meidet diese Sprachen (anstatt hochdynamische Sprachen wie Ruby, PHP oder JavaScript zu bevorzugen). Korrelation impliziert keine Kausalität, gibt aber Anlass zum Nachdenken.
Amon
1
Sie möchten also lieber in einer Spezifikationssprache als in einer Programmiersprache programmieren? Ok, Sie werden in der Lage sein zu beweisen, dass es gemäß den Spezifikationen funktioniert. Aber wie wollen Sie beweisen, dass die Spezifikation das wahre Problem widerspiegelt?
Christophe
3
@toto die Frage ist: die Dinge richtig zu machen (Arbeit nach den Spezifikationen) oder die richtigen Dinge zu tun (mit den guten Spezifikationen). Während in der Theorie die Spezifikation genau das ist, was wir wollen, wissen wir in der Praxis selten genau, was wirklich benötigt wird: beyssonmanagement.com/2012/10/29/…
Christophe
3
Für diejenigen, die enttäuscht sind, dass dies geschlossen ist, gibt es jetzt einen großartigen Blog-Beitrag: Warum wenden die Leute keine formalen Methoden an?
ICC97

Antworten:

19

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.

Jörg W. Mittag
quelle
1
Ich möchte auch hinzufügen, dass das Einfügen formaler Methoden in die Programmiersprache ein Bereich aktiver Forschung ist, dh noch nicht für den Mainstream bereit ist
jk.
1
Ich akzeptiere diese Antwort, aber ich wollte auch einen Ansatz, warum formale Methoden immer noch als "teuer" und "zeitaufwendig" gelten, insbesondere wenn wir wissen, wie teuer Wartung und Code-Tracking / Debugging bei großen Projekten sind.
Toto
1
TDD & BDD sind Ansätze, die auf den Prinzipien der Hoare-Logik aufbauen, einer Grundlage formaler Ansätze. Sie verbessern die Effizienz, ohne sie zu beeinträchtigen.
Martin Spamer
1
@toto Beweise sind wirklich WIRKLICH schwer. Viele Dinge, die Mathematiker in Beweisen für selbstverständlich halten, gelten in Programmen nicht. Zum Beispiel in C ++, zusätzlich ist nicht assoziativ: (-1 + 1) + INT_MAX = INT_MAX, -1 + (1 + INT_MAX)ist nicht definiertes Verhalten.
Hovercouch
1
@toto: Der Grund, warum sie als "teuer" und "zeitaufwendig" eingestuft werden, ist, dass wir uns Projekte ansehen können, die mit formalen Methoden entwickelt wurden, und empirisch nachweisen können, dass die Entwicklung dieser Projekte viel länger dauert. Sehen Sie sich zum Beispiel die Entwicklungszeit von seL4 / L4.verified im Vergleich zu jeder anderen Implementierung von L4 an.
Jörg W Mittag
12

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 :

Bildbeschreibung hier eingeben

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.

Christophe
quelle
Bei der vertragsbasierten Programmierung werden zumindest informelle Beweise verwendet.
Frank Hileman
@FrankHileman ja! Die einfache Klärung von Vorbedingungen, Nachbedingungen und Invarianten hilft dabei, Code effizient zu überprüfen, Fehler zu reduzieren und Tests zu systematisieren.
Christophe
Dies sollte mit Abstand die beste Antwort sein.
Hashim
0

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.

Lewis Pringle
quelle