Modellüberprüfung ist der algorithmische Verifizierungsprozess, der den Zustandsraum eines formalen Modells exploriert, um zu bestimmen, ob es eine gegebene Spezifikation erfüllt, die oft in temporalen oder modalen Logiken ausgedrückt wird.

Prinzip

Durchquere erschöpfend oder symbolisch die erreichbaren Zustände des Modells nach der Semantik des Systems, evaluiere die Spezifikation in jedem relevanten Zustand oder Ablauf und liefere Erfüllungsergebnisse oder Gegenbeispielspuren, wenn Eigenschaften fehlschlagen.

Demonstration

Prüfe ein endliches Protokollmodell gegenüber einer LTL-Sicherheitseigenschaft, indem der erreichbare Zustandsgraph mittels Breitensuche oder symbolischer BDDs aufgebaut und im Fehlerfall eine Gegenbeispielspur gemeldet wird.

Fehlanwendung

Die naive Anwendung der Modellüberprüfung auf Systeme mit effektiv unendlichem Zustandsraum ohne geeignete Abstraktion führt zu irreführenden Ergebnissen; eine Gegenbeispielspur als Implementierungsbeweis zu interpretieren, ohne Modellierungslücken zu prüfen, ist irreführend.

Konsequenz

Modellüberprüfung liefert konkrete Gegenbeispiele für verletzte Eigenschaften und hohe Sicherheit für endliche Zustandsmodelle; sie automatisiert Fehlerfinden, Regressionsprüfung und Verifikation von Entwurfsmodellen unter spezifizierter Semantik.

Umkehrung

Die Umkehr ist deduktive Verifikation oder Theorembeweis, bei dem symbolische Korrektheitsbeweise konstruiert werden statt Zustandsräume erschöpfend zu erkunden; Simulation ist eine schwächere Alternative, die Verhaltenstests stichprobenartig durchführt.

Abgrenzung

Modellüberprüfung ist anwendbar auf endliche oder effektiv aufzählbare Zustandsräume, Modelle mit wohldefinierter Semantik und Eigenschaften in prüfbaren Logiken; sie schließt unabstrahierte unendliche Zustandsysteme und informelle Spezifikationen aus, sofern nicht geeignet kodiert.

Semantische Spannung

Es besteht Spannung zwischen der zustandsraumorientierten Modellüberprüfung und dem symbolischen Beweisen der Theorembeweiser: Modellprüfung liefert Gegenbeispiele und konkrete fehlerhafte Abläufe, während Beweise allgemeine Garantien liefern, jedoch nicht notwendigerweise Gegenbeispiele.

Synthese

Modellüberprüfung ist eine algorithmische, häufig erschöpfende Methode, die bewertet, ob ein formales Modell eine Spezifikation erfüllt, indem sie dessen Zustandsraum durchläuft oder symbolisch darstellt und Erfüllungsresultate oder diagnostische Gegenbeispiele zurückgibt.