Next:
Input Formulas Up: Model Checking Benchmarking Scripts Previous: Explicit Tool Models

Symbolic Tool Models

We can also benchmark LTL formula modeling with CadenceSMV and NuSMV. To check whether a LTL formula $\varphi $ is satisfiable, we model check $\neg\varphi $ against a universal SMV model. For example, if $\varphi = (X (a))$, we provide the following input to NuSMV:

MODULE main
  VAR
    a : boolean;
    b : boolean;
    c : boolean;
  LTLSPEC !(X(a=1 ))
  FAIRNESS
    1
(The ``FAIRNESS'' line varies with versions of NuSMV. The CadenceSMV model is very similar.) SMV negates the specification, $\neg\varphi $, symbolically compiles $\varphi $ into $A_{\varphi }$, and conjoins $A_{\varphi }$ with the universal model. If the automaton is not empty, then SMV finds a fair path, which satisfies the formula $\varphi $. In this way, SMV acts as both a symbolic compiler and a search engine.



Kristin Yvonne Rozier 2007-05-10