Software Verification

V-Modell: Links runter: Anforderung -> Design -> Code. Rechts hoch: Unit Test -> Integration Test -> System Test -> Acceptance Test. Jede Stufe verifiziert die gegenüberliegende Stufe. Der Unit Test verifiziert den Code. Der System Test verifiziert das Design.

1. Dynamic vs. Static Verification

• Dynamic: Code ausführen (Testing). Findet echte Runtime-Fehler. Aber unvollständig.
• Static: Code anschauen (Review, Linting, Beweisen). Findet Design-Fehler und Logik-Probleme ohne Ausführung.

2. Traceability

In der kritischen Software (Medizin, Auto) musst du beweisen, dass jede Anforderung getestet wurde. Anforderung RF-123 ("Muss rot blinken") -> Test Case TC-456 ("Prüfe blinken") -> Resultat PASS. Ohne diese Matrix keine Zulassung (FDA/TÜV).

1. Abstract Interpretation (Cousot & Cousot)

Wie verifiziert man eine Endlosschleife? Man kann sie nicht unendlich oft testen. Abstract Interpretation ist die Lösung: Man bildet die echten Werte auf ein "abstraktes Domain" ab. Anstatt zu sagen x = 5, sagt man x ist POSITIV. Wenn die Schleife x = x + 1 macht, bleibt x weiterhin POSITIV. Man rechnet so lange, bis sich das Ergebnis nicht mehr ändert (Fixpunkt). So kann man beweisen, dass x niemals 0 wird, ohne jemals die Schleife im Computer wirklich ausgeführt zu haben. Das ist die Engine hinter Tools wie Astrée (wird genutzt, um das Kontrollsystem des Airbus A380 zu verifizieren).

2. Bounded Model Checking (BMC)

In der Chip-Entwicklung oder bei komplexen Protokollen nutzt man BMC. Man übersetzt das Programm und die Fehlbedingung in ein riesiges logisches Rätsel (SAT-Instanz). Man fragt: "Gibt es einen Pfad der Länge $k$, der zu einem Absturz führt?" Der SAT-Solver prüft nun Millionen von Möglichkeiten gleichzeitig per massiver Parallelisierung in der Mathe. Wenn er für $k=100$ keinen Fehler findet, ist das System zwar nicht "bewiesen", aber man hat eine extrem hohe Konfidenz, dass keine "einfachen" Bugs mehr drin sind.

3. Software Contract & Hoare Logic

Modernes Engineering nutzt Design by Contract (Eiffel, Ada, Spark). Jede Funktion hat:

• Pre-condition: "Gib mir eine Zahl > 0."
• Post-condition: "Ich garantiere, das Ergebnis ist die Wurzel." Ein Verifier (wie Dafny oder Framer-C) prüft nun mathematisch, ob der Funktions-Körper (L0-Code) die Post-condition für alle möglichen Inputs erfüllt, die die Pre-condition erfüllen. Das ist "Correctness by Construction" – anstatt Fehler später zu suchen, macht man es unmöglich, sie zu programmieren.

Vertiefung im Glossar

Für konkrete Werkzeuge und Methoden fuehrt der nächste Schritt zu TLA+, SPIN (Simple Promela Interpreter), NuSMV, Dafny, Coq, Isabelle/HOL, Frama-C, CBMC (C Bounded Model Checker), SAT Solver, Model Checking, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) und Mu-Calculus.