Folge 311 - Wozu formale Methoden? mit Lars Hupel | Stichpunkte

Der nachfolgende Text wurden mit KI erstellt und kann Fehler enthalten. Fehler gefunden? Bei GitHub editieren

Wichtige Keytakeaways

• Formale Methoden sind ein Bündel von Maßnahmen zur Verbesserung der Korrektheit von Software, die von einfachen Typsystemen bis zu komplexen Theorembeweisern reichen.
• Der praktische Einsatz formaler Methoden ist eine wirtschaftliche Abwägung: Die Nutzung ist aufwändig und daher teuer, aber unverzichtbar in sicherheitskritischen Bereichen wie Aviation, Healthcare und Defense.
• Gutes Systemdesign mit Immutability, klarer Zustandsmodellierung und State Machines schafft eine solide Grundlage für die Anwendung formaler Methoden und ist oft schon ausreichend, um Fehler zu finden.
• Typsysteme sind die in der Praxis am häufigsten verwendete formale Methode und schließen bereits viele Fehlerklassen aus, ohne zusätzliche Komplexität zu erzeugen.
• Der Akt der Modellierung selbst – etwa durch Zustandsdiagramme – hilft Entwicklern, Fehler frühzeitig zu erkennen, bevor Code implementiert wird.
• Formale Methoden formalisieren die implizite Theoriebildung von Entwicklern und machen verborgenes Domänenwissen explizit und kommunizierbar.

Behandelte Kernfragen

• Was sind formale Methoden und in welcher Beziehung stehen sie zu anderen Korrektheitstechniken?
• Wie unterscheiden sich Typsysteme, State Machines, Model Checking und Theorembeweiser in Bezug auf Mächtigkeit und Anwendbarkeit?
• Warum wird formale Verifikation nicht standardmäßig in der Softwareentwicklung eingesetzt?
• Wie können Entwickler ohne Spezialisierung formale Methoden in ihren Projekten einsetzen?
• Welche Rolle spielen KI und Machine Learning bei der Automatisierung von Beweisen?
• Wie trägt der iSAQB Certified Architect mit dem Formale-Methoden-Modul zur Ausbildung bei?

Glossar wichtiger Begriffe

• Theorembeweiser (z.B. Isabelle): Ein Tool, mit dem die Korrektheit von Code formal bewiesen werden können, indem Definitionen, Sätze und Beweise wie im Matheunterricht genutzt werden; erfordert manuelle Erklärung jedes Beweisschrittes durch den Nutzer.

• Model Checking: Eine automatisierte Technik, die alle möglichen Zustände eines Systems durchsucht, um zu prüfen, ob bestimmte Eigenschaften verletzt werden; weniger aufwendig als Theorembeweise, aber auf begrenzte Zustandsräume beschränkt.

• Separation Logic: Ein mathematisches Framework zur Verifikation von imperativen Programmen, das Speicherbereiche voneinander trennt, um modular Korrektheits-Eigenschaften lokal zu beweisen und dann zusammenzufügen.

• Event Sourcing: Ein Architektur-Pattern, bei dem alle Änderungen am System als unveränderliche Events dokumentiert werden, aus denen der aktuelle Zustand rekonstruierbar ist; ideal für formale Verifikation, da Zustandsübergänge isoliert betrachtet werden können.

• Isar: Eine spezialisierte Sprache innerhalb von Isabelle zur Dokumentation von Beweisen, die wie ein Mathematikbuch lesbar ist und Semi-Automatic Reasoning ermöglicht, bei dem das System einfache Schritte automatisiert.

• State Space: Die Gesamtheit aller möglichen Zustände, die ein System einnehmen kann; große State Spaces erschweren formale Verifikation, weshalb Abstraktion und Modellvereinfachung notwendig sind.

• State Space Explosion Das Problem, dass die Anzahl möglicher Zustände bei komplexen Systemen exponentiell wächst und Verifikation unmöglich macht.

Genannte Technologien

• Isabelle: Funktionaler Theorembeweiser für mathematische und softwaretechnische Beweise
• TLA+: Spezifikationssprache und Model Checker von Leslie Lamport für verteilte Systeme
• Lean: Moderner Theorembeweiser mit Dual-Implementation für erhöhte Korrektheitssicherheit
• Rust: Programmiersprache mit strengem Typsystem zur Ausschließung von Speicherfehlern
• CompCert: Ein formal verifizierter C-Compiler, der beweist, dass er keine neuen Bugs einführt
• seL4: Ein formal verifizierter Mikro-Kernel für Betriebssysteme in kritischen Anwendungen

Liste der behandelten Fragen

1. Was sind formale Methoden und welche verschiedenen Arten gibt es?
2. Wie unterscheiden sich statische und dynamische Typprüfung in Bezug auf formale Verifikation?
3. Welche praktischen Anwendungsfälle rechtfertigen den Einsatz von Theorembeweisern wie Isabelle?
4. Wie können Entwickler ohne spezialisierte Ausbildung formale Methoden einführen?
5. Welche Rolle spielen Machine Learning und KI bei der Automatisierung von Beweisen?
6. Warum ist formale Verifikation nicht der Standard in der kommerziellen Softwareentwicklung?