The capabilities of NUSMV were tested on a series of examples
taken from the literature, which were then used for a comparison
with the original CMU SMV. Below is a brief description of the
tests used and their sources:
the {4,8,10,11}-bit alternating bit protocol by Armin Biere
[4].
a bounded retransmission (communication) protocol, by
Klaus Havelund [40].
the examples of the CMU SMV distribution.
a model of the Shuttle Digital Autopilot, by Sergey Berezin.
some models of the PCI Bus protocol, by Sergio Campos.
a model of production cell, by Kirsten Winter [61].
some model of part of a preliminary version of the system requirements
specification of TCAS II (Traffic Alert and Collision Avoidance
System II), by William Chan [1].
These examples can be found in the distribution of NUSMV. Table
3 lists the results of such a comparative test. For each
test, we report the number of (current and next) boolean variables necessary
to represent the corresponding model (``# of BDD vars''), and the
memory17 and time required by the systems to analyze the model. We mark as
time out the failure to the problems in 15000 seconds. For the examples
marked with ``(*)'' a previously computed ordering file was provided to the
system. The verification of the examples marked with a ``(+)'' required the
modification of some of the parameters of the BDD package. The other symbols
between parentheses are command line options passed to the model checkers:
-f enables the computation of the set of reachable states (which is
then used to restrict the search in model checking), while -cp #
enables conjunctive partitioning with the threshold of each partition set to
#. All these tests were performed on an Intel Pentium-II 300Mhz
processor with 512Mb of RAM under Linux RedHat 5.0.
The results listed in Table 3 show that NUSMV performs in
most examples better (in 22 examples of the 39 listed w.r.t. to speed and in
8 examples w.r.t. to memory occupation) than CMU SMV, especially for larger
examples. This enhancement in performance is mainly due to the use of the
state of the art CUDD BDD package. In the tests none of the enhanced
capabilities not present in CMU SMV (e.g., enhanced partitioning methods),
were used.
>