Formale Methoden zur Fehlererkennung: Was geht, was nicht

Modellbasierte Entwicklung schiebt Fehler früher in den Prozess — aber das allein reicht nicht. Auch im Modell selbst können logische Fehler stecken, die kein Test je aufdeckt: Zustände, die nie erreicht werden; Bedingungen, die nie wahr sein können; Wertebereiche, die still überlaufen. Bei der ersten Ariane 5 reichte 1996 eine ungeprüfte Wertebereichs-Konvertierung, um die Rakete 37 Sekunden nach dem Start zu zerstören. In Systemen, die nach dem Start niemand mehr patcht, ist das die teuerste Art, einen Bug zu finden.

Der Nutzen formaler Fehlererkennung steht damit außer Frage. Interessant ist, ob sie sich auf Zustandsautomaten praktikabel umsetzen lässt. Wir haben das in zwei Masterarbeiten an der TU Dortmund ausprobiert, mit itemis CREATE als Testbench. Hier werfen wir einen genaueren Blick auf das Gesamtergebnis: was diese Methoden leisten, wo sie an Grenzen stoßen, und was am Ende brauchbar ist.

Reachability als Erfüllbarkeitsproblem

Der Kern ist ein symbolischer Ausführungsbaum (Symbolic Execution Tree, SET). Statt mit konkreten Eingaben rechnet die Analyse mit Symbolen. Für jeden Pfad führt sie eine Pfadbedingung mit: die Konjunktion aller Guards und Zuweisungen entlang dieses Pfades. Jeder Knoten im Baum hält den symbolischen Zustand fest: Variablenwerte plus aktuelle Pfadbedingung. Folgeknoten entstehen durch Transitionsregeln oder Regeln, die Ausdrücke in die Pfadbedingung einarbeiten.

Erreichbarkeit reduziert sich damit auf Erfüllbarkeit. Ein Zustand ist erreichbar, wenn mindestens ein Pfad im Baum eine erfüllbare Pfadbedingung hat. Diese Prüfung übernimmt ein SMT-Solver (in unserem Fall Z3). Liefert er für jeden Pfad zu einer Transition UNSAT, ist die Transition unerreichbar.

Die interessanten Fehlerklassen werden dadurch zu kleinen, präzisen Solver-Anfragen:

• Widerspruch im Guard: der Guard g ist unerfüllbar. Der Solver prüft sat(g). UNSAT bedeutet, die Transition feuert unter keiner Belegung.
• Tautologie im Guard: der Guard ist allgemeingültig. Prüfung über unsat(¬g). Ist die Negation unerfüllbar, ist der Guard immer wahr und damit überflüssig.
• Überschattung: zwei Transitionen t1 (höhere Priorität) und t2 aus demselben Zustand beim selben Ereignis. t2 ist überschattet, wenn g(t2) ∧ ¬g(t1) unerfüllbar ist: jede Belegung, die t2 auslösen würde, löst auch t1 aus.

• Division durch Null: für jeden Divisor d auf dem Pfad prüft der Solver sat(pc ∧ d == 0). Ist das erfüllbar, gibt es einen erreichbaren Pfad, auf dem der Divisor null werden kann.
• Toter Zustand: ein erreichter Zustand, dessen sämtliche ausgehende Guards unter der aktuellen Pfadbedingung unerfüllbar sind.

• Endlosschleife: ein Zyklus, dessen Austrittsbedingung nie erfüllbar wird, sodass dahinterliegende Zustände unerreichbar bleiben.

Eine grundlegende Eigenschaft ist dabei nicht verhandelbar: Ein erreichbarer Zustand darf nie als unerreichbar markiert werden. Die Analyse arbeitet konservativ. Sie meldet „unerreichbar" nur, wenn sie es beweisen kann. False Positives bei der Unerreichbarkeit gibt es nicht. Das ist die Voraussetzung dafür, dass Anwender dem Werkzeug vertrauen.

Der symbolische Ausführungsbaum wächst exponentiell — ohne Beschneidung terminiert die Analyse nicht. Wer Tiefe oder Pfade begrenzt, riskiert blinde Flecken: Fehler in tief verschachtelten Pfaden bleiben unsichtbar, nicht weil sie nicht existieren, sondern weil der Baum sie nicht mehr erreicht. Das Tiefenlimit ist die zentrale Stellschraube dieses Trade-offs.

Welche Methode trägt

Drei Anforderungen schränkten die Auswahl ein: Die Prüfung sollte direkt am Modell im Editor laufen — kein separater Übersetzungsschritt. Sie sollte arithmetische Daten verarbeiten können, weil unsere Fehlerklassen (unerfüllbare Guards, Division durch Null) in die Domäne eines SMT-Solvers fallen, nicht eines Kontrollflussprufers. Und sie sollte mit dem Statechart-Modell von itemis CREATE umgehen, ohne es vorab zu vereinfachen.

Der etablierte Zweig für dieses Problem ist das Model Checking. Die bekanntesten Werkzeuge sind SPIN (Modellierung in Promela, Eigenschaften in Linear Temporal Logic) und UPPAAL (Timed Automata für Echtzeitsysteme). Beide sind industriell erprobt: SPIN in der Flugsoftware der NASA-Sonde Deep Space 1, UPPAAL überall dort, wo harte Zeitschranken gelten. Für temporale Eigenschaften nebenläufiger oder zeitbehafteter Systeme sind sie die erste Wahl.

Speziell auf Statecharts zugeschnitten ist das Gamma Statechart Composition Framework der TU Budapest (FTSRG). Gamma nutzt itemis CREATE als Frontend: Die Komponenten werden direkt dort modelliert, Gamma kompiliert sie in eine eigene Zwischensprache und übersetzt sie dann in Backends wie UPPAAL, Theta, Promela oder SMV. Aus demselben Modell generiert das Framework anschließend Java-Code. Komposite und orthogonale Zustände (die unser Prototyp ausgeklammert hat) gehören zu Gammas Kerngebiet.

Für unser Ziel passte diese Route nicht gut genug. Erstens verlangt sie einen Übersetzungsschritt: Das Statechart wird in ein anderes Format überführt, statt direkt am Modell im Editor geprüft zu werden. Zweitens abstrahieren die Backends Daten bewusst; SPIN kennt nicht einmal eine Uhr. Unerfüllbare Guards mit Integer-Arithmetik, Division durch Null oder tote Zustände fallen aber in die Domäne eines SMT-Solvers. Deshalb der Blick auf die SMT- und Symbolic-Execution-Familie.

Drei Wege standen zur Wahl:

Reines SMT-Solving. Den Guard direkt an Z3 übergeben. Schnell und exakt für lokale Eigenschaften wie Widersprüche, Tautologien und Überschattungen. Für eine Erreichbarkeitsanalyse über das ganze Modell fehlt aber das Rahmenwerk, das Pfade und Laufzeitzustände erzeugt.

Deduktive Verifikation mit Dafny. In der Theorie das stärkste Mittel. In der Praxis nicht tragfähig: Dafny verlangt, dass die Terminierung jedes Programms beweisbar ist. Ein reaktiver Automat, der dauerhaft auf Ereignisse wartet, passt nicht in dieses Korsett. Der Ansatz produzierte außerdem False Positives.

Programmverifikation mit dem KeY-Project. Über generierten Java-Code analysiert, kam besser mit nicht terminierenden Automaten zurecht, fand tote Zustände und Divisionen durch Null und ließ sich als Java-Programm direkt einbinden. Die Schwäche blieben beliebige Schleifen, die das Verfahren aufhängen.

KeY kam am nächsten, aber der Weg über generierten Java-Code bedeutet wieder einen Übersetzungsschritt — und willkürliche Schleifen hängen das Verfahren auf. Die Kombination aus Symbolic Execution und SMT-Solver behebt genau das: Symbolic Execution erzeugt den Pfadbaum direkt am Modell, ohne Reaktivität vorauszusetzen. Der SMT-Solver prüft die Pfadbedingungen — ohne die Datenlücken von SPIN oder den Terminierungszwang von Dafny. Genau denselben Aufbau nutzen etablierte Werkzeuge auf Code-Ebene wie KLEE oder EXE.

Die Wand: Zustandsexplosion

Dieses Tiefenlimit ist keine willkürliche Schranke — es ist die direkte Antwort auf ein strukturelles Problem. Symbolische Ausführung verfolgt alle Pfade gleichzeitig, und das skaliert schlecht. Jede Verzweigung verdoppelt im schlimmsten Fall die Pfade, jeder Zyklus erzeugt prinzipiell unendlich viele. In der Modellprüfung heißt dasselbe Phänomen Zustandsexplosion. Es ist die Hürde, an der das ganze Feld seit Jahrzehnten arbeitet, mit ML-gestützter Pfadauswahl, State Merging, Kopplung an Bounded Model Checking oder concolic execution — der Mischung aus symbolischer und konkreter Ausführung — als Antworten darauf. Für Statecharts mit arithmetischen Guards greift keiner davon direkt: concolic execution setzt ausführbaren Code voraus, Bounded Model Checking abstrahiert Daten.

Wir haben den Baum daher über Zyklen-Elimination beschränkt. Die Zyklen findet die Analyse über die starken Zusammenhangskomponenten des Transitionsgraphen — Mengen von Zuständen, die sich gegenseitig erreichen können. Beim Auflösen eines Zyklus würde man naiv das gesamte Variablenwissen verwerfen. Der entscheidende Kniff: Nur das Wissen über Variablen vergessen, die sich innerhalb des Zyklus tatsächlich ändern. Alles andere bleibt erhalten — so rechnet der Solver mit den stabilen Größen weiter.

Zwischen konservativer Elimination, die einen Zyklus eine einstellbare Anzahl von Malen durchläuft bevor sie abbricht, und präventiver Elimination, die ihn beim ersten Besuch schließt, kann gewählt werden. Auch Zyklen aus lokalen Reaktionen werden behandelt, nicht nur aus Transitionen. Der Preis ist immer derselbe: etwas Präzision gegen garantierte Terminierung.

Was es schnell genug macht

Der Solver-Aufruf dominiert die Laufzeit. Vier Optimierungen haben am meisten gebracht:

• Unabhängigkeitsoptimierung. Eine Pfadbedingung zerfällt oft in Teilmengen von Constraints, die keine Variablen teilen. Für eine konkrete Frage prüft der Solver nur die relevante Teilmenge, nicht die ganze Bedingung. Dieselbe Idee steckt in KLEE und EXE unter dem Namen constraint independence.
• Wiederverwendung von Erfüllbarkeitsergebnissen. Gleiche oder eingebettete Teilbedingungen tauchen im Baum ständig wieder auf. Ein Cache spart die wiederholten Solver-Aufrufe.
• Kontext-Solving. Bereits bekanntes Wissen wird als Kontext mitgegeben, statt jede Anfrage von null zu lösen.
• Kostenfunktion für die Pfadwahl. Die Engine bevorzugt Pfade, die am ehesten neue Erreichbarkeiten aufdecken.

Die Modelle werden nach SMT-LIB2 serialisiert, als Solver-Backend dienten Z3 und jConstraints. Für Zustandsautomaten als Modell gab es 2020 keine vergleichbare Engine — wir haben sie deshalb von Grund auf modular aufgebaut, mit austauschbaren Strategien für Exploration und Erfüllbarkeit.

Was dabei herauskam:

• Die schnellste Strategie blieb bei bis zu rund 6.800 Knoten und Kanten unter 0,2 Sekunden.
• Die Tests deckten alle Komponenten ab und erreichten 85 Prozent Code-Coverage.
• Auf demselben Ausführungsbaum laufen weitere Analysen ohne Neuberechnung — darunter Erkennung uninitialisierter Variablen und, perspektivisch am wertvollsten, eine Testfallgenerierung, die alle Ausführungspfade abdeckt.

Was der Ansatz nicht abdeckt:

• Komposite und orthogonale Zustände, History-Knoten und mehrere Regionen werden nicht unterstützt.
• Externe Funktionsaufrufe werden nicht analysiert.
• Evaluiert wurde an einem synthetischen Automaten, nicht an einem Produktivmodell.
• Die praktische Obergrenze von rund 6.800 Knoten ergibt sich aus der Berechnung der starken Zusammenhangskomponenten.

Einordnung

Formale Verifikation wird in sicherheitskritischen Bereichen längst angewendet. DO-178C (Luftfahrt), EN 50128 (Bahn), ISO 26262 (Automotive) und IEC 61508 verlangen den Nachweis, dass Software definiert reagiert und nichts Unerwartetes tut.

Was diese Normen eint: Sie akzeptieren nur Aussagen, die beweisbar sind — nicht solche, die wahrscheinlich stimmen. Der entscheidende Punkt ist daher Vollständigkeit. Formale Verifikation im Sinne dieser Normen setzt eine vollständige Analyse voraus: Entweder ist eine Eigenschaft bewiesen, oder es gibt ein Gegenbeispiel. Der hier beschriebene Ansatz (Symbolic Execution mit Zyklen-Elimination) erfüllt das nicht. Er ist konservativ: Was als unerreichbar markiert wird, ist es. Aber er ist nicht vollständig: Was er nicht findet, kann trotzdem existieren. Das macht ihn zu einem nützlichen Begleiter im Entwicklungsprozess, nicht zu einem Ersatz für normgerechte formale Verifikation.

Fazit

Die Machbarkeit ist belegt, mit klaren Konturen. Lokale Fehler wie unerfüllbare Guards, Tautologien und Überschattungen findet bereits ein SMT-Solver schnell und exakt. Eine Erreichbarkeitsanalyse über das ganze Modell ist mit Symbolic Execution plus Solver praktikabel, solange die Pfadexplosion über Zyklen-Elimination kontrolliert wird und dafür etwas Präzision geopfert wird. Für den Alltag im Entwicklungsprozess reicht dieser Ansatz.

Die Analyse ist konservativ: Was sie als unerreichbar meldet, ist es auch. Das erlaubt einen anderen Einsatzmodus als klassische Verifikation: keine einmalige Gate-Prüfung vor dem Release, sondern ein permanenter Hintergrundcheck im Editor. Ein unerfüllbarer Guard wird sichtbar, während er entsteht, nicht wenn das Modell bereits in andere Artefakte eingeflossen ist. Je früher ein Fehler gefunden wird, desto billiger ist er zu beheben; das gilt für Code, und es gilt für Modelle.

Der Zustandsautomat war für uns nur die Testbench. Unentscheidbarkeit, Pfadexplosion und die Abwägung zwischen Vollständigkeit und Praktikabilität gelten für formale Verifikation insgesamt, unabhängig vom Modelltyp.

Zu den Quellen

Wir haben die Machbarkeit in zwei Masterarbeiten am Lehrstuhl für Software Engineering (LS-14) der TU Dortmund geprüft, betreut von Prof. Dr. Jakob Rehof und Dr.-Ing. Martin Hentschel, in Kooperation mit itemis (Dominic Starzinski, 2019; Jonas Wielage, 2020).

Modellgetriebene Softwareentwicklung bei itemis: Zustandsautomaten analysieren, validieren und Code generieren: Modellgetriebene Softwareentwicklung →