Eine automatische Verifikationstechnik, die den Zustandsraum eines formalen Systemmodells (in der Regel ein endlicher Zustandsübergangsgraph) exhaustiv durchsucht, um zu prüfen, ob das Modell eine Spezifikation in temporaler oder modaler Logik erfüllt, und im Fehlerfall Gegenbeispielspuren liefert.

Prinzip

Das System in ein endliches oder symbolisches Zustandsmodell übersetzen, die gewünschte Eigenschaft in einer Spezifikationslogik (z. B. LTL, CTL) ausdrücken und eine exhaustive (explizite, symbolische, begrenzte oder durch partiellen Ordnungsabbau reduzierte) Suche erreichbarer Zustände durchführen; Gegenbeispiele sind konkrete Übergangsspuren, die die Eigenschaft verletzen.

Demonstration

Überprüfen einer LTL‑Sicherheits­eigenschaft auf einem endlichen nebenläufigen System mittels symbolischem Model Checking mit BDDs oder SAT‑basierter bounded model checking: schlägt die Eigenschaft fehl, liefert das Werkzeug eine endliche Spur der Transitionen, die zur Verletzung führt und die zum Debuggen genutzt werden kann.

Fehlanwendung

Model Checking naiv auf unendliche Zustandsysteme anzuwenden ohne Abstraktion, zu glauben, bounded model checking beweise unbeschränkte Eigenschaften, oder Gegenbeispiele aus Abstraktionen (spurious counterexamples) fälschlich als reale Fehler zu interpretieren.

Konsequenz

Model Checking ermöglicht vollautomatische, gegenbeispielgeführte Fehlerfindung und, wo machbar, Korrektheitsgarantien für das betrachtete Modell; es erfordert eine präzise Formalisierung von Verhalten und Anforderungen, leidet jedoch unter dem Zustandsraum‑Explosionsproblem, das die Skalierbarkeit einschränkt.

Umkehrung

Statt exhaustiver Zustandsdurchsuchung kann man deductive verification oder Theorem Proving einsetzen, die symbolisch über Klassen von Verhalten argumentieren; die Umkehr tauscht Automatisierung und konkrete Gegenbeispiele gegen Allgemeinheit und Beweisverpflichtungen.

Abgrenzung

Am besten geeignet für endliche oder endlich repräsentierbare Systeme bzw. Systeme, die einer sounden Abstraktion zugänglich sind; verschiedene Logiken und Modelltypen (timed, probabilistic, hybrid) erfordern erweiterte Algorithmen. Model Checking adressiert die Korrektheit des Modells gegenüber einer Spezifikation, nicht notwendigerweise der Implementierung, sofern diese nicht modelliert ist.

Semantische Spannung

Spannung besteht zwischen explizitem State‑Model Checking, symbolischen Methoden (BDD, SAT/SMT) und Abstraktions/Verfeinerungsansätzen: die Wahl beeinflusst Skalierbarkeit, Interpretierbarkeit von Gegenbeispielen und ob Ergebnisse exhaustiv oder beschränkt sind. Zudem besteht ein Zielkonflikt zwischen vollautomatischer Suche und interaktiven Beweistechniken.

Synthese

Model Checking ist eine automatisierte, exhaustive Analyse eines formalen Modells gegenüber temporalen oder logischen Spezifikationen, die konkrete Gegenbeispiele zum Debuggen liefert und, wenn anwendbar, vollständige Korrektheitsgarantien; seine Wirksamkeit beruht auf Repräsentation, Abstraktion und Suchtechniken zur Beherrschung des Zustandsraumwachstums.