Blog

Wie lässt sich Software wirklich korrekt umsetzen – und wo stoßen klassische Tests an ihre Grenzen? Lars Hupel gibt Einblicke in den Einsatz formaler Methoden und zeigt, wann sich ihr Einsatz besonders lohnt.

Korrektheit klingt selbstverständlich, spielt aber in der Praxis oft nur eine untergeordnete Rolle. Warum ist das so – und in welchen Fällen wird sie wirklich kritisch?

Natürlich möchte niemand „inkorrekte“ Software liefern. Aber in den allermeisten Projekten gibt es schlicht kein Budget, vollständige Korrektheit sicherzustellen.

Das liegt daran, dass Methoden, um diese zu erreichen oder zu approximieren, die Softwareentwicklung verteuern. Denn das Team muss, zumindest für die kritischen Teile der Software, detaillierte Spezifikationen schreiben und dann natürlich auch die Implementierung gegen die Spezifikation prüfen.

„Kritisch“ wird oft in Kontexten benutzt, in denen Softwarefehler inakzeptabel sind. Das kann verschiedene Branchen betreffen, z.B. Luft- und Raumfahrt, Medizin oder Finanzdienstleistungen. Dort kann man nicht einfach hinnehmen, wenn Software die Anforderungen nicht vollständig erfüllt, da sonst großer Schaden entsteht.

Du sagst, dass Tests allein nicht ausreichen, um Korrektheit sicherzustellen. Wo liegen die Grenzen klassischer Testverfahren – und was leisten formale Methoden darüber hinaus?

Dijsktra sagte einmal, dass Testing nur die Anwesenheit von Bugs zeigen kann, nicht aber die Abwesenheit. Denn Tests können prinzipbedingt nicht den gesamten möglichen Eingabe- und Ergebnisraum von Software abdecken. Sicherlich ist jede:r schon einmal Bugs begegnet, die sich in Grenzfällen verstecken. (Man denke z.B. daran, dass YAML „no“ als „false“ interpretiert, was in einer Länderliste denkbar ungünstig ist.)

Formale Methoden gehen nun darüber hinaus und geben uns Garantien, statt einem bloßen Versprechen. Statt nur eine (endliche) Liste von Testfällen abzuarbeiten, wird für bestimmte Eigenschaften eine universelle Aussage getroffen.

Formale Methoden gelten oft als komplex oder schwer zugänglich. Wie gelingt es, diese Ansätze in realen Projekten sinnvoll und pragmatisch einzusetzen?

Dafür gibt es vermutlich keine Zauberformel.

Der erste wichtige Aspekt ist, die Teile eines Systems zu identifizieren, bei denen sich die Anwendung formaler Methoden lohnt.

Der zweite ist, abhängig von den Anforderungen die richtige formale Methode auszuwählen. Es gibt eine große Palette an Optionen, von leichtgewichtig (bspw. Modellierung von Zustandsmaschinen) bis hin zu schwergewichtig (Programmverifikation).

Nehmen wir als Beispiel eine Banking-App: Wahrscheinlich ist es nicht so schlimm, wenn die App ab und zu mal abstürzt (keine formalen Methoden notwendig). Aber dabei sollte sie auf keinen Fall eine Überweisung verschlucken oder doppeln (formale Methoden notwendig).

Welche Anforderungen stellt der Einsatz formaler Methoden an die Softwarearchitektur? Worauf sollten Architekt:innen achten, wenn sie verifizierbare Systeme entwerfen?

Verifizierbarer Code muss auf eine bestimmte Art und Weise konzeptioniert und geschrieben werden.

Beispielsweise sollte man so weit wie möglich externe Interaktionen wie Datenbank- oder Netzwerkzugriffe isolieren. Auch sollten sich Komponenten möglichst klar auf eine Aufgabe fokussieren und nur über definierte Schnittstellen kommunizieren.

Glücklicherweise sind das auch Merkmale einer guten Softwarearchitektur im Allgemeinen. Das heißt: wer die Prinzipien der iSAQB-Module DDD oder DSL ernst nimmt, wird bei der Anwendung von formalen Methoden Vorteile haben.

Du bringst Beispiele aus der Praxis mit: Wo siehst du aktuell die wichtigsten Einsatzgebiete für formale Methoden? Wo lohnt sich ihr Einsatz besonders?

Ein in der Softwareentwicklung alltägliches Beispiel ist der Compilerbau. Compilerbugs sind oft schwer zu debuggen und können zu äußerst ungünstigem Verhalten führen.

„CompCert“ ist ein akademisches Projekt, aus dem ein praxistauglicher C-Compiler hervorgegangen ist. Man kann diesen in sicherheitskritischen Kontexten einsetzen, um sicherzustellen, dass der kompilierte Code auch der tatsächlichen Semantik des Quelltextes entspricht. Just letzten Monat wurde angekündigt, dass CompCert in Flugzeugen des Herstellers ATR eingesetzt werden.

Mehr zum Thema gibt es beim Software Architecture Forum 2026: Dort zeigt Lars Hupel in seiner Session, wie sich formale Methoden konkret in der Softwarearchitektur einsetzen lassen.

Über den Sprecher:

Lars ist Evangelist bei Giesecke+Devrient, ein internationales Unternehmen, welches sich auf Zahlungssysteme, Konnektivität, digitale Identitäten und Infrastruktur spezialisiert hat. Lars arbeitet daran, moderne finanzielle Dienste und Umgebungen zu schaffen.