Modellprüfung für Software

Die Modellprüfung verifiziert automatisch, ob das Modell eines Systems eine temporale Logikspezifikation erfüllt, indem sie dessen erreichbare Zustände erschöpfend untersucht.

Definition

Modellprüfung ist eine automatische Verifikationstechnik, die, gegeben ein endliches Zustandsmodell eines Systems und eine temporale Logikspezifikation, erschöpfend prüft, ob die Spezifikation erfüllt ist, und einen Gegenbeispiel-Trace erzeugt, falls dies nicht der Fall ist.

Scope

Dieses Thema umfasst die automatische Verifikation von endlichen Zustands- und nebenläufigen Systemen hinsichtlich temporal-logischer Eigenschaften (Sicherheit und Lebendigkeit), das Zustandsraumexplosionsproblem und Techniken zu dessen Bekämpfung (symbolische Darstellung mit binären Entscheidungsdiagrammen, Partial-Order-Reduktion, Abstraktion), begrenzte Modellprüfung mit SAT/SMT und Counterexample-Guided Abstraction Refinement für Software.

Core questions

• Wie kann eine Eigenschaft durch die Untersuchung aller erreichbaren Zustände verifiziert werden?
• Was ist das Zustandsraumexplosionsproblem und wie wird es gemildert?
• Wie skalieren symbolische und begrenzte Methoden die Modellprüfung?
• Wie werden Software-Systeme mit unendlichem Zustand in endliche Modelle abstrahiert?

Key theories

Temporale Logik-Modellprüfung

Clarke, Emerson und Sistla sowie unabhängig davon Queille und Sifakis führten Algorithmen ein, um endliche Zustands- und nebenläufige Systeme automatisch anhand temporaler Logikspezifikationen zu prüfen.

Symbolische Modellprüfung

Burch und Kollegen stellten Zustandsmengen symbolisch mit binären Entscheidungsdiagrammen dar, was die Verifikation von Systemen mit astronomisch vielen Zuständen ermöglichte und die naive Zustandsraumexplosion überwand.

Clinical relevance

Modellprüfung wird zur Verifikation von Hardware-Designs, Kommunikationsprotokollen sowie nebenläufiger und sicherheitskritischer Software eingesetzt, wo sie subtile Fehler findet, die beim Testen übersehen werden, und Gegenbeispiele liefert, die Fehler genau lokalisieren. Ihre Automatisierung unterscheidet sie vom interaktiven Theorembeweisen.

History

Aufbauend auf Pnuelis Einführung der temporalen Logik für Programme entwickelten Clarke und Emerson sowie unabhängig davon Queille und Sifakis um 1981-82 die Modellprüfung, eine Arbeit, die später mit einem Turing Award ausgezeichnet wurde. Die symbolische Modellprüfung mit binären Entscheidungsdiagrammen (1990er Jahre) und die SAT-basierte begrenzte Modellprüfung erweiterten ihre Reichweite erheblich, und Abstraktions-Verfeinerungsmethoden brachten sie in die Softwareentwicklung.

Debates

Bekämpfung der Zustandsraumexplosion

Die zentrale Herausforderung besteht darin, dass die Anzahl der Zustände exponentiell mit der Systemgröße wächst; Forscher diskutieren die beste Mischung aus symbolischer Darstellung, Abstraktion, Partial-Order-Reduktion und begrenzter Prüfung, um die Verifikation handhabbar zu halten.

Key figures

• Edmund Clarke
• E. Allen Emerson
• Joseph Sifakis
• Kenneth McMillan
• Amir Pnueli

Seminal works

• clarke1986
• queille1982
• burch1992

Frequently asked questions

Wie unterscheidet sich die Modellprüfung vom Theorembeweisen?

Die Modellprüfung ist vollautomatisch und untersucht den Zustandsraum eines Systems erschöpfend für endliche oder abstrahierte Modelle, während das Theorembeweisen logische Deduktion (oft interaktiv) verwendet und unendliche Zustands-Systeme behandeln kann, aber mehr menschliche Anleitung erfordert.

Was ist das Zustandsraumexplosionsproblem?

Es ist das exponentielle Wachstum der Anzahl erreichbarer Zustände, wenn ein System Komponenten oder Variablen hinzugewinnt, was die naive Modellprüfung begrenzt und symbolische, begrenzte und abstraktionsbasierte Techniken motiviert.