- In großen, verteilten und wichtigen Low-Level-Systemen sollten formale Methoden nicht als zusätzlicher Prozess nur für Korrektheit betrachtet werden, sondern als Engineering-Praxis, die Zeit und Kosten senkt
- In Software vermischen sich Design und Implementierung leicht, sodass späte Designänderungen unmittelbar zu Implementierungs-Rework und Kosten für API-Änderungen führen
- Wenn Verhalten und Schnittstellen vor der Implementierung konkret geprüft werden, lassen sich Fehlerdichte und Probleme nach dem Produktionsstart reduzieren, und man gelangt schneller zum richtigen Design
- In Bereichen mit sich schnell ändernden Nutzeranforderungen oder solchen, die schwer zu formalisieren sind – etwa UI, Dokumentation oder Preislogik –, kann der Nutzen eines umfassenden formalen Vorab-Designs geringer ausfallen
- Tools wie TLA+ und P können auch genutzt werden, um in der Designphase Optimierungen und Einschränkungen zu prüfen und so Trade-offs zwischen Korrektheit und Performance zu reduzieren
Formale Methoden als gute Engineering-Praxis
- Formale Methoden sind ein wichtiger Teil guter Software-Engineering-Praxis
- Besonders wertvoll sind sie für Engineers, die mit großen Systemen, verteilten Systemen und wichtigen Low-Level-Systemen arbeiten
- Ausgangspunkt ist die Annahme, dass Engineering letztlich eine Tätigkeit zur Optimierung von Zeit und Kosten ist
- Performance, Skalierbarkeit, Nachhaltigkeit und Effizienz werden dabei ebenfalls berücksichtigt
- Formale Methoden sind weder billig noch einfach und passen nicht zu jeder Entwicklungsweise; die Intuition, dass sie nur Kosten erhöhen, ist jedoch nicht immer richtig
Zwei Wege zur Kostensenkung
- Der erste ist weniger Rework
- Anders als in anderen Engineering-Disziplinen finden Design und Bau in der Software oft gleichzeitig statt
- Man kann mit der Implementierung beginnen, auch wenn das Design noch nicht weit genug ausgearbeitet ist
- Diese Veränderbarkeit ist eine Stärke von Software, kann aber Designiterationen in Implementierungsiterationen verwandeln und damit die Kosten erhöhen
- Der zweite ist Management von Änderungskosten
- Sobald eine API oder ein System Kunden hat, werden Änderungen deutlich teurer und schwieriger
- Nach Hyrum’s Law wird sich bei ausreichend vielen API-Nutzern unabhängig vom Vertrag irgendjemand auf jedes beobachtbare Verhalten verlassen
- Systemverhalten hinter einer API zu kapseln, ist eine wichtige Idee im Software Engineering; dennoch bleibt die Einschränkung, dass Nutzer auch von Implementierungsdetails abhängig werden können
- Ein System hinter einer API kann zwar vollständig neu implementiert werden, aber Abstraktion beseitigt die Änderungskosten selbst nicht
- Formale Designarbeit kann Rework-Kosten senken und Schnittstellenänderungen früher behandeln, wodurch Geschwindigkeit und Effizienz beim Bau von Software steigen
Systeme, zu denen formales Design gut passt
- Es lässt sich nicht auf jede Software auf dieselbe Weise anwenden
- Bei Software mit vielen schnell evolvierenden oder schwer zu formalisierenden Nutzeranforderungen kann der Wert von Vorab-Design geringer sein
- UI, Websites und die Implementierung von Preislogik gehören dazu
- In solchen Bereichen gibt es viel kontinuierlichen Rework, wodurch die Kosten des Vorab-Designs hoch ausfallen können
- Die Grundidee von Agile ist, Implementierung und Anforderungserhebung parallel durchzuführen, um die Zeit bis zum Release zu verkürzen
- So kann die Implementierung abgeschlossen werden, auch wenn die Anforderungserhebung weiterläuft
- In vielen Fällen ist diese parallele Entwicklungsweise optimal oder eine notwendige Voraussetzung, um überhaupt voranzukommen
- Umgekehrt sind viele Teile großer, verteilter Low-Level-Systeme in ihren Anforderungen gut verstanden
- Zumindest gibt es einen ausreichend großen statischen Anteil an Anforderungen
- In diesem Fall kann formales Vorab-Design Rework und Fehlerdichte in der Implementierungsphase und nach dem Produktionsstart erheblich reduzieren
- Je näher Anforderungen an physikalischen Gesetzen liegen, desto größer ist der Wert von Design und formalem Design; je näher sie an Nutzermeinungen liegen, desto geringer ist er
Grenzen von Anforderungsdokumentation und Formalisierung
- Nutzeranforderungen klar aufzuschreiben, ist sehr wertvoll – ob formal oder informell
- Wenn Anforderungen nicht aufgeschrieben werden, wird Zeit verschwendet, und es kann zu Reibung kommen, weil Menschen in unterschiedliche Richtungen arbeiten
- Es kann schwierig oder wirtschaftlich nicht sinnvoll sein, alle menschlichen Anforderungen formal zu spezifizieren
- Ästhetische UI-Anforderungen
- Lesbarkeit von Dokumentation
- Konsistenz von API-Namen
- Meinungsverschiedenheiten über formale Ansätze entstehen auch aus unterschiedlichen Vorstellungen davon, was formale Ansätze sind und auf welche Weise sie wertvoll sind
- Ein Ansatz wie UML, bei dem Code in umfangreiche Diagramme übertragen wird, kann an Wert verlieren, wenn er schwierige Fragen nicht direkt adressiert
- Mit schlechten Methoden oder schlechten Tools ausgeführt, kann auch wertvolle Arbeit nutzlos werden
In der Praxis nützliche formale Methoden und Tools
- Formale Methoden und automatisches Schließen sind ein breites Feld mit vielen verschiedenen Tools
- Eine Tool-Gruppe, die im Bereich großer Cloud-Systeme nützlich war, ist folgende
- Spezifikationssprachen wie P, TLA+ und Alloy sowie zugehörige Model Checker
- Deterministische Simulationstools wie turmoil
- Sie werden zusammen mit Fuzzing genutzt, um den Zustandsraum durch Tests systematisch zu erkunden
- Verifikationsfreundliche Programmiersprachen wie Dafny und Code-Verifikatoren wie Kani
- Numerische Simulationstechniken
- Formalen Methoden nahestehende Ansätze wie Entscheidungstabellen, Wahrheitstabellen und explizite Zustandsautomaten auf Whiteboards oder in Designdokumenten
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 ist ein Ausgangspunkt, um sich mit leichtgewichtigen formalen Methoden zu beschäftigen
- Implementierungsverifikation ist nicht das einzige Ziel
- Tools wie TLA+ und P haben großen Wert darin, Designs vor der Implementierung schneller und konkreter zu prüfen
Schnellere Software schneller bauen
- Als 2015 How Amazon Web Services Uses Formal Methods geschrieben wurde, lag der Fokus vor allem auf Korrektheit
- Sicherheits- und Lebendigkeitseigenschaften des Designs verifizieren
- Schneller zum richtigen Design gelangen
- Im Fall eines Teams, das TLA+ für ein internes Lock-Management-System nutzte, war wichtig, dass es „aggressive Optimierungen verifiziert“ hatte
- Tools wie TLA+ helfen nicht nur, Systeme schneller zu bauen, sondern auch, schnellere Systeme zu bauen
- Mögliche Optimierungen schnell erkunden
- Die wirklich wichtigen Einschränkungen finden
- Prüfen, ob eine vorgeschlagene Optimierung korrekt ist
- In vielen Fällen reduzieren formale Methoden die schwierigen Trade-offs zwischen Korrektheit und Performance, in die Systeme leicht geraten
Wert von Tools in der Designphase
- Wenn Tools, die beim Nachdenken über Systemdesign helfen, in der Designphase eingesetzt werden, kann das die Geschwindigkeit der Softwareentwicklung deutlich erhöhen
- Sie reduzieren Risiken und ermöglichen es, von Anfang an optimiertere Systeme zu bauen
- Für Engineers, die große und komplexe Systeme bauen, sind formale Methoden Teil guter Engineering-Praxis
1 Kommentare
Hacker-News-Kommentare
Software-formale Verifikation hängt, wie auch der Artikel einräumt, stark von der Art der Software und vom Entwicklungsprozess ab.
Um formale Verifikation einzusetzen, braucht man formale Anforderungen an das Verhalten der Software, doch die meisten Projekte und Designphilosophien passen nicht dazu. Wenn Entwicklung und Design parallel laufen, ohne dass überhaupt klar ist, was man will, sind formale Methoden schwer anzuwenden. Bereiche, die auf Spezifikationen im Voraus angewiesen sind – etwa kleine, sicherheitskritische Systeme –, können jedoch stark profitieren; Luft- und Raumfahrtsoftware ist ein typisches Beispiel.
Heute ist das keine Technik mehr, für die man einen Doktortitel oder jahrelange Forschung braucht; dasselbe gilt für das Schreiben grundlegender High-Level-Spezifikationen. Wenn man einen Model Checker nutzt, lernt man etwas über das System, das man modelliert, und selbst wenn man ihn nur zur Dokumentation oder Schulung verwendet, ist er nützlich. Die grundlegende Stärke formaler Methoden liegt darin, dass sie einen zwingen, Dinge zu Ende zu denken. Viele Entwickler glauben, sie könnten nebenläufige Algorithmen allein mit dem eigenen Kopf, einem Type Checker und ein paar Unit Tests implementieren. Wenn sie aber nach dem Lauf eines Model Checkers Fehler im Design und in den Annahmen finden, werden sie zwangsläufig demütig. Kleine verteilte Systeme gibt es mehr, als man denkt, und der Zustandsraum ist oft viel größer, als man vor einer Formalisierung erwartet.
Zum Beispiel habe ich eine besonders knifflige Zustandsmaschine mit property-basierten Tests versehen, um sicherzustellen, dass die interne Zustandsmaschine keine ungültigen Transitionen ausführt, egal mit welchen seltsamen Eingaben ein Endpoint aufgerufen wird. Der umgebende Code hatte keine formale Spezifikation, die Zustandsmaschine aber schon; dadurch war das möglich, und wir fanden subtile Bugs, die klassische Unit Tests niemals entdeckt hätten.
Um jedoch von formalen Methoden zu profitieren, muss man das Programmverhalten mit etwas anderem als dem Programm selbst vergleichen, und auch dieses Andere muss in einer formalen Sprache geschrieben sein. Man muss das gewünschte Verhalten genau verstehen, aber es muss nicht das gesamte Verhalten der Software abdecken. Auch automatisierte Unit Tests sind formale Spezifikationen, und sie auszuführen ist eine formale Verifikationsmethode. Sie sind nur schwächere Spezifikationen und schwächere Verifikation als das, was man üblicherweise als formale Methoden bezeichnet; konzeptionell oder praktisch gibt es keinen klaren qualitativen Unterschied. Wenn Tests auf eine Software anwendbar sind, ist es wahrscheinlich, dass auch reichhaltigere formale Spezifikationsmethoden anwendbar sind, und das Kosten-Nutzen-Verhältnis lernt man wie beim Testen durch Versuch und Irrtum.
Am Ende geht es darum, wie viel mehr Geld und Zeit man ausgeben will, damit es „agil“ genannt werden kann. Paradoxerweise ist die traditionelle Anforderungsphase von diesen drei Varianten die günstigste und passt auch am besten zum ursprünglichen Geist von Agile: Man konvergiert schnell mit dem Kunden genau zu dem Zeitpunkt, an dem Änderungen am billigsten sind – indem man eine Textzeile ändert.
Trotzdem kann man den Nutzen daraus ziehen, zu prüfen, ob keine Fälle übersehen wurden und ob es im System keine Widersprüche gibt.
Zu formalen Methoden sieht man oft die Argumentation: „Software ist groß und komplex und schwer korrekt hinzubekommen, also formale Methoden.“
Einerseits wünschte ich, das wäre wahr. Ich bin gut in der akademischen Art, Dinge zu lernen, also würde es mir persönlich nützen; und auch praktisch ist es frustrierend, bei tatsächlich komplexer Software nach Ursachen zu suchen, wenn sie scheitert. Aber nur selten wird überzeugend gezeigt, wie formale Methoden dieses Problem lösen. Dieser Text ist insofern besser, als er darauf hinweist, dass der Großteil des heutigen „Designs“ Zeitverschwendung ist, erklärt aber nicht ausreichend, warum TLA besser ist als UML. Es klingt fast so, als würde man, wenn man Monate oder Jahre in TLA investiert, Erleuchtung erlangen und dann auf eine Weise erkennen, dass es nützlich ist, die sich den Nicht-Erleuchteten nicht erklären lässt. Bei Analysis oder Bayes-Statistik gibt es so etwas auch, es ist also nicht unmöglich; am Ende landet man aber wieder bei der projektmanagerhaften Einschätzung: „Wenn es wirklich so nützlich wäre, würden es mehr Leute verwenden, und die Vorteile würden von selbst sichtbar.“ Wenn etwas schon lange existiert, sich aber nicht breit etabliert hat, gibt es dafür sehr wahrscheinlich einen Grund.
Wenn man auf ein Problem stößt, über das schwer nachzudenken ist, greift man zu irgendeiner „Methode“. Bei einem Kommunikationsprotokoll ist es sinnvoll, es als Zustandsmaschine zu beschreiben, und TLA passt besser in diese Nische. In letzter Zeit gab es nicht viele Probleme, die diesen Aufwand rechtfertigen, aber wenn ein solches Problem auftaucht, ist der Wert enorm. Ähnlich ist es bei domänenspezifischen Sprachen: Um viele Probleme zu vermeiden, ist es viel besser, ein Parser-Framework zu verwenden, als selbst einen Parser zu schreiben. Der größte Teil der heutigen Nacharbeit entsteht durch geänderte Anforderungen und dadurch, dass Kunden nicht wissen, was sie wirklich wollen, sondern nur sagen: „Das ist es nicht.“ Teilweise denken die Anfordernden die Implikationen ihrer Wünsche nicht ausreichend durch; wichtiger ist aber, dass das Wissen für gute Entscheidungen nicht ausreichend an einer Stelle zusammenkommt.
Formale Methoden sind eindeutig eine große Investition. Auch wenn sie sich allgemein nicht durchgesetzt haben, sind Teile ihrer Ideen in moderne Typsysteme eingeflossen.
Mein Eindruck war, dass schon die Anforderung, dass ein formaler Verifizierer in vertretbarer Zeit und mit vertretbarem Speicher fertig werden muss, der Design-Komplexität Grenzen setzt. Vielleicht liegt der eigentliche Gewinn der Forderung nach formaler Verifikation darin, das Problem „Software ist groß, komplex und schwer korrekt hinzubekommen“ dadurch zu beheben, dass sie es lästig macht, große komplexe Programme zu handhaben.
Ich würde gern Nachfolger von Property-Based Testing sehen, die mit SAT- oder TLA-Techniken den Eingaberaum schnell und reproduzierbar reduzieren. Durch Parsing und Code Coverage sollte man ableiten können, dass die Übergabe von 12 an eine Funktion keinen anderen Branch nehmen kann als 11, dass aber Werte wie -1 oder 2^17 < n < 2^32 anders sein könnten.
Die meisten Softwareprojekte scheitern immer noch. Das ist kein „Marktversagen“, sondern eher schlicht „am Bauen gescheitert“.
Bei formalen Methoden gibt es grob zwei Stränge: extrinsische Methoden, die vom Code selbst getrennt sind und üblicherweise Spezifikationen des Codes herleiten, und intrinsische Methoden, die im Code enthalten sind und direkter über den Code schließen.
Historisch haben intrinsische Methoden wie Typsysteme auf Funktionsebene über Code geschlossen, während extrinsische Methoden wie entscheidbare Model Checker à la Spin/P mit Modellen von Code arbeiteten, die in Formalismen wie Automaten beschrieben waren. Ich sehe die Gegenwart als ein goldenes Zeitalter der Forschung zu formalen Methoden; gegenüber den Fortschritten bei Typsystemen und den intrinsischen Ansätzen, die Projekte wie Verus vorantreiben, scheinen extrinsische Methoden zunehmend weniger bevorzugt zu werden. https://github.com/verus-lang/verus
Ich habe die Frage gesehen, wie das bei einer Sprache mit großem Footprint wie Rust funktionieren soll, aber noch keine gute Antwort darauf. Ich würde gern mehr dazu lesen.
Es klang so, als seien intrinsische Methoden deshalb bevorzugt, weil man keine separaten Spezifikationen schreiben und pflegen muss, aber tatsächlich ist das nicht so.
Der Abschnitt zu leichtgewichtigen formalen Methoden ist gut. Eine Sammlung von proptest-Strategien neben der Codebasis zu pflegen, ist keine viel größere Investition als manuell geschriebene Unit-Tests, liefert aber dank breiter Coverage und kleiner, verständlicher Fehlerfälle deutlich bessere Einsichten.
Vor allem passt dieser Ansatz auch gut zu gängigen Praktiken der Softwareentwicklung. https://crates.io/crates/proptest
Ich weiß in etwa, wie man gute Tests schreibt und wie viel Aufwand das kostet, aber ein LLM kann viel schneller bessere Tests erstellen als ich. Bei repetitiver, langweiliger Arbeit werde ich ungeduldig; es ist gut möglich, dass es weniger schlampig vorgeht als ich. Als Software Engineer sollte man den Reflex haben, sich wiederholende Aufgaben zu automatisieren, und auch Dokumentation wird heutzutage generiert, sodass man sie häufiger und früher erstellt. LLMs könnten bei der Einführung formaler Verifikation eine kleine Revolution auslösen. Korrekte Spezifikationen zu erstellen ist zwar langweilig, könnte für ein LLM aber eine relativ einfache Aufgabe sein, wenn genügend Kontext wie funktionierender Code, Dokumentation und Hinweise vorhanden ist. Wenn man Spezifikationen nicht vollständig selbst schreiben muss, sondern sie generieren lassen und dann überfliegen kann, ist man viel eher bereit dazu. Rust zu verwenden ist auch ein Signal, dass einem Korrektheit wichtig ist, und sein Compiler kommt einem Werkzeug, das ohne formale Methoden beweist, dass ein System wahrscheinlich korrekt ist, schon sehr nahe. Das ist wahrscheinlich viel einfacher, als formale Methoden an eine Sprache ohne Compiler oder explizite Typen anzuflanschen.
Formale Verifikation von Software ist immer noch zu schwierig, um sich außerhalb extremer Fälle wirklich zu lohnen. Formale Verifikation von Hardware dagegen ist inzwischen etwas, das man kaum noch nicht einsetzen sollte
Ich versuche ständig, dazuzulernen, aber bei den meisten Systemen muss man Experte auf dem Niveau von „jemand, der den Compiler selbst geschrieben hat“ sein. Ich wollte zum Beispiel einen Varint-Encoder/-Decoder beweisen: Für 1–2 Bytes ging es, darüber hinaus nicht. Als ich um Hilfe bat, stellte sich heraus, dass es an völlig undurchschaubaren internen Details lag, etwa daran, dass der Compiler intern Schleifen nur fünfmal entfaltet. In letzter Zeit lerne ich Lean, und es gefällt mir zwar, aber dann stößt man auf Dokumentation wie: „Definitional equality includes η-equivalence …“. Das soll Lean nicht schlechtmachen; im Gegenteil, unter den Alternativen scheint die Dokumentation eher zu den besseren zu gehören
Formale Methoden müssen nicht zwingend kompliziert sein. Das Problem ist, dass die meisten formalen Methoden wie akademische Übungen entworfen wurden, um ein bestimmtes Thema zu demonstrieren, das einen Professor interessiert hat. Auch TLA+ ist eher in Richtung „für das Schreiben von Papers entworfen“
Eine der weniger bekannten, aber von mir geschätzten leichtgewichtigen formalen Methoden ist Trace-Verification mit linearer temporaler Logik: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
Im Grunde muss man nur Events loggen, und in eventbasierten Architekturen bekommt man das praktisch gratis. Danach lässt man Prädikate wie
Always(Locked, Implies(Eventually(Unlocked)))über die Ausführungstraces laufen. Das kann man auch auf vergangene Traces anwenden und mit Stresstests oder Fuzzing kombinieren, um den Zustandsraum zu erkunden. Es ist einfach, mächtig und breit anwendbar; man braucht kein Modell, nur PrädikateFormale Methoden implizieren eine umfassende Begründung über das Systemverhalten. In TLA oder ähnlichen Systemen ist es zwar eine Zustandsmaschine und nicht das reale System, aber das Ergebnis ist ein Beweis, dass LTL-/CTL-/TLA-Eigenschaften für alle Verhaltensweisen des Systems gelten, also für Traces oder Trace-Bäume
Eine frühere Diskussion gab es im Juni 2024: https://news.ycombinator.com/item?id=40753989
15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - Mai 2024, 1 Kommentar
Viel zu langsam. Planung ist im Grunde schon Versteinerung, und jedes Dokument kann vor dem agilen Gericht als belastendes Beweismittel verwendet werden
Das meiste, was ich über formale Methoden gelesen habe, fühlt sich wie Lead-Generierung von Beratern an
Das ist an sich in Ordnung, aber es ist unangenehm, wenn jemand so tut, als hätte er durch formale Methoden Erleuchtung erlangt und könne, wenn meine Mitarbeiter oder Kollegen ein Schulungspaket kaufen oder mich einstellen, schlechte, ja sogar unverantwortlich gefährliche Programmiergewohnheiten kurieren. Meldet euch wieder, wenn formale Methoden tatsächlich hochwertigen Code erzeugen, der nicht von der Spezifikation abweichen kann
In formalen Spezifikationen legt man normalerweise nicht Details auf dieser Ebene fest, sondern beschreibt das allgemeine Verhalten des Systems. Deshalb kann eine Spezifikation oft zu vielen Programmen passen, die sich subtil unterscheiden. Genau deshalb reicht Code als Dokumentation nicht aus: Man kann nicht erkennen, welche Entscheidungen beabsichtigt waren und welche zufällig. Code ist zu konkret, um High-Level-Anforderungen zu beschreiben. Umgekehrt ist es eher umsetzbar, ein Programm gegen eine Spezifikation zu verifizieren
Einige der heutigen Befürworter formaler Methoden betrachten Menschen, die sie nicht einsetzen, als „faul“ oder „dumm“ und versuchen, Überlegenheit daraus abzuleiten, dass sie „das Richtige tun“ oder „eine komplexe Sprache beherrschen“
Natürlich nicht alle, und ich kenne auch nette Leute, aber manche sind im Grunde Leute mit nur einem Trick. Wenn man fragt, welche anderen Systeme für formale Methoden sie in den letzten Jahren gelernt oder ausprobiert haben, heißt es, sie seien „zu beschäftigt“, um etwas Neues zu lernen. Zu den neueren, leichter nutzbaren formalen Methoden gehören FizzBee, das einen Python-Dialekt verwendet und sich wie Pseudocode liest, Quint mit einfacherer Syntax und P mit einer Syntax, die C#-Nutzern vertraut ist. Auch der Autor dieses Artikels hat einmal geschrieben, dass formale Methoden nur die Hälfte seines Problems lösen: https://brooker.co.za/blog/2022/06/02/formal.html
Das dort beschriebene Problem löst jedoch bereits PRISM, das nicht einmal neu ist. Brooker sucht nur nicht in seiner Umgebung danach und versucht auch nicht, es zu lernen