Version 2.5.1
Oct 01, 2010

We are happy to announce the availability of a new version of the NuSMV model checker. NuSMV version 2.5.1 is available from https://nusmv.fbk.eu.

NuSMV 2 extends the previous versions of NuSMV with several new features, most notably with the possibility of performing SAT-based Bounded Model Checking (see the Overview below).

This is a minor release that provides most notably a major change in the language. It features also several bug fixes (more than 30), a few new operators in the SMV language, some new command line options, a few optimizations, and some fixes in the documentation.

The main changes are listed below. For details please refer to the ChangeLog.

New features

  • SMV grammar

    • The new version 2.5.1 makes a strong distinction between integers and boolean types. This breaks backward compatibility, since integers values cannot be used anymore where booleans are used, and vice-versa.

      To mitigate the problems that may arise from this change, new operators have been introduced (e.g., the count operator), and the signature of existing ones have been extended (e.g., the toint operator) to allow to cope with no longer supported expressions.

      Thus, the following typical snippets of code are no longer accepted:

      1. Given N boolean expressions b1, ..., bN, to specify that at most M out of N must be TRUE, before it was possible to write

        1
        (b1 + b2 + ... + bN) <= M.

        From 2.5.1 on this condition has to be specified as

        1
        count(b1,b2,...,bN) <= M.

      2. Constant "1" cannot be used anymore as default condition into a case statement. Thus the following code snippet

        1
2
3
4
5
6
        case
  b1 : e1;
  ...
  bN : eN;
  1  : eD; -- expression for default condition
esac

        has to be rewritten as

        1
2
3
4
5
6
        case
  b1 : e1;
  ...
  bN : eN;
  TRUE : eD; -- expression for default condition
esac

        In this snippet b1, ..., bN are boolean expressions representing the conditions, and e1, ..., eN, eD are the expressions the case construct evaluates to when the corresponding condition evaluates to TRUE.

    • Added the count() operator, which takes a list of boolean expressions and returns the number of expressions that evaluates to TRUE.

    • Operator toint() now supports word type expressions.

  • System commands

    • Command show_vars no longer prints by default all the values of an enumerative variable, and truncates it if too long to be printed, and reports the number of the remaining elements. The new command line option -v for this command enables the previous behavior.

    • Command set now accepts "0" and "1" when setting values of boolean system variables. Now set <var> 0 has the same effect as unset <var>, and set <var> 1 has the same effect as set <var>.

  • Command line options

    • The backward-compatibility option -old has been extended to make NuSMV accept syntactical construct "1" in case conditions to specify the default condition. This is intended to mitigate the impact of the strong type distinction between integer and boolean types, in existing SMV models. This feature will be removed in future releases.

Bug fixes

  • Garbage in dimacs file under Windows platforms.
    Thanks to Luca Zanetti <> for reporting it.
  • Standard output and error, and the shell's prompt are now in sync under Windows. Thanks to Aleksey Nogin <> for the report and for providing a patch.
  • The parser can handle now comments with length greater than 16381 characters.
  • The type checker can now successfully detect ambiguities in identifiers which refer to both enumerative literals and variable names.
  • Fixed a crash which was in some cases occurring when extracting the counter-example of a false property, with cone of influence was enabled.
  • Fixed some memory leaks.
  • Fixed several portability issues.

Attachment

Overview

NuSMV is a re-implementation and extension of SMV, the first model checker based on BDDs. It has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, and as a test-bed for formal verification techniques.

NuSMV version 2 extends NuSMV with new model checking algorithms and techniques. It combines classical BDD-based symbolic techniques with SAT-based techniques. It also presents other new features: for instance, it allows for a more powerful manipulation of multiple models; it can generate flat models for the whole language; it allows for cone of influence reduction.

The BDD-based model checking component exploits the CUDD library developed by Fabio Somenzi at Colorado University. The SAT-based model checking component includes an RBC-based Bounded Model Checker, connected to a SAT solver to be compiled separately (instructions and building support are batteries included in NuSMV, details are underneath). The currently available SAT solvers are: + The ZCHAFF SAT library developed by the Princeton University + The MINISAT SAT library developed by Niklas Een or Niklas Sorensson.

NuSMV version 2 is distributed with an OpenSource license, namely the GNU Lesser General Public License (LGPL). The aim is to provide a publicly available state-of-the-art symbolic model checker. With the OpenSource development model, a whole community participates in the development of a software systems, with a distributed team and independent peer review. This may result in a rapid system evolution, and in increased software quality and reliability: for instance, the OpenSource model has boosted the take-up of notable software systems, such as Linux and Apache. With the NuSMV OpenSource project, we would like to reach the same goals within the model checking community, opening the development of NuSMV.

You can find further details on NuSMV 2 and on the NuSMV project in paper:

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. "NuSMV 2: An OpenSource Tool for Symbolic Model Checking". In Proc. CAV'02, LNCS. Springer Verlag, 2002.

Copyright

NuSMV version 2 (NuSMV 2 in short) is licensed under the GNU Lesser General Public License (LGPL in short). A copy of LGPL-2.1 can be found at url <http://www.gnu.org/licenses/lgpl.txt>.

The aim of the NuSMV OpenSource project is to allow anybody interested to participate to the development of NuSMV. To this purpose, we have chosen a license that:

  1. permits to use the system in research and commercial applications, without restrictions;
  2. is "copyleft", that is, it requires that anyone who improves the system has to make the improvements freely available.

In brief, the LGPL license allows anyone to freely download, copy, use, modify, and redistribute NuSMV 2, proviso that any modification and/or extension to the library is made publicly available under the terms of LGPL.

The license also allows the usage of the NuSMV 2 as part of a larger software system without being obliged to distributing the whole software under LGPL. Also in this case, the modification to NuSMV 2 (not to the larger software) should be made available under LGPL.

Notice that zchaff is for non-commercial purposes only. NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN PERMISSION FROM PRINCETON UNIVERSITY. Please contact Sharad Malik (malik@ee.princeton.edu) for details.

Notice also that the CUDD library is copyright University of Colorado. The CUDD library is not covered by LGPL.

Please contact <nusmv@list.fbk.eu> if you have any doubt or comment on the license.

Partners

Different partners have participated to the initial release of NuSMV 2. Every source file in the NuSMV 2 distribution contains a header that acknowledges the developers and the copyright holders for the file. In particular:

  • CMU and ITC-IRST contributed the source code of NuSMV version 1;
  • ITC-IRST has also developed several extensions for NuSMV 2;
  • ITC-IRST and the University of Trento have developed the SAT-based Bounded Model Checking package of NuSMV 2;
  • the University of Genova has contributed SIM, a state-of-the-art SAT solver, and the RBC package used in the Bounded Model Checking algorithms.
  • FBK-irst has developed version 2.5.0 and later.

The NuSMV team has also received several contributions for different part of the system. In particular:

  • Ariel Fuxman <afuxman@cs.toronto.edu> has extended the LTL to SMV tableau translator to the past fragment of LTL
  • Rik Eshuis <eshuis@cs.utwente.nl> has contributed a strong fairness model checking algorithm for LTL specifications
  • Dan Sheridan <dan.sheridan@contact.org.uk> has contributed several extensions and enhancements to the Bounded Model Checking algorithms.

Statements of interest have also come from several other commercial and academic institutions.

Mailing Lists

Refer to this page.

Bug Reports

We have performed an extensive test activity on NuSMV2. Still, NuSMV is large software system and contains many interacting features.

If you find a bug or misbehavior, please let us know, so that we can fix it for the next releases of NuSMV.

You can send an email to <nusmv-users@list.fbk.eu> with the description of the bug. Refer to this page for more information.

NuSMV Staff <>
https://nusmv.fbk.eu/