NuSMV-Befehle: Symbolischer Model Checker für CTL und LTL

NuSMV (New Symbolic Model Verifier) ist ein weit verbreiteter symbolischer Model Checker, entwickelt an der Universität Trient (FBK-IRST). Er ist die Neuimplementierung und Erweiterung des klassischen SMV von Ken McMillan (CMU), der 1998 den Turing Award für das symbolische Model Checking mit BDDs mitprägte. NuSMV prüft Eigenschaften, die in CTL (Computation Tree Logic) oder LTL (Linear Temporal Logic) formuliert sind, gegen ein endliches Zustandsmodell.

SMV-Eingabesprache

MODULE main
VAR state : {idle, busy};
ASSIGN
  init(state) := idle;
  next(state) := case
    state = idle : busy;
    TRUE        : idle;
  esac;
SPEC AG (state != busy -> AX state = busy)

Eine SMV-Datei beschreibt MODULEs, VAR-Deklarationen, INIT/ASSIGN/TRANS-Übergänge und SPEC-Eigenschaften. Typische CTL-Operatoren sind AG, EG, AF, EF, AX, EX; LTL nutzt G, F, X, U.

Befehle

nusmv modell.smv          # Batch-Modus: Modell laden und alle SPEC pruefen
nusmv -dcx modell.smv     # Dynamic Cone of Influence (Reduktion)
nusmv -p "AG (x = 1)" modell.smv   # Eigenschaft direkt pruefen
nusmv -bmc -k 10 modell.smv        # Bounded Model Checking
# interaktive Session:
read_model                 # Datei laden
go                         # BDD bauen
check_ctlspec              # CTL-Spezifikationen pruefen
check_ltlspec              # LTL-Spezifikationen pruefen
check_invar                # Invarianten pruefen
pick_state; simulate       # Zustand waehlen und Pfade simulieren
print_reachable_states     # erreichbare Zustaende anzeigen
show_vars                  # Variablen auflisten

Die Eigenschaften können entweder in der SMV-Datei stehen oder per -p bzw. über den Property-Index (-n) in der interaktiven Session geprüft werden. -bmc aktiviert das beschränkte Modellprüfen, das mit SAT-Solvern längere Pfade skaliert als die reine BDD-Suche.

Einordnung

Der Nachfolger nuXmv erweitert NuSMV um IC3/PDR-basierte Algorithmen und wird ebenfalls von FBK entwickelt. NuSMV bildet mit SPIN/Promela das Standard-Duo der automatisierbaren Model Checker: SPIN prüft asynchrone Prozesse, NuSMV synchrone endliche Systeme. Zusammen mit TLA+, B-Methode und Event-B deckt er die automatisierte Seite der formalen Verifikation ab.

Verwandte Grundlagen: Z-Notation (Spezifikationssprache), C/C++-Befehle (typische Zielsysteme).