Version 2.5.0
May 17, 2010

We are happy to announce the availability of a new version of the NuSMV model checker. NuSMV version 2.5.0 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).

Version 2.5.0 is a major release which provides new features, many optimizations and bug fixes, and an extensive reorganization of the source code and API.

Many changes were driven by projects which involved FBK, like:

In all these projects, the core of NuSMV has been improved to deal with large scalability issues. Several bottlenecks were identified, and fixed, with particular care about the memory usage.

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

Features highlights

  • Added forward version of the Emerson-Lei algorithm for checking language emptiness of Buchi fair transitions systems with BDDs.
  • Improved invariant checking with new search strategies and heuristics.
  • Extended the language support for arrays and matrices.
  • Added several commands and options to dump the model. See the details about commands and options below.
  • The previously provided default SAT solver "SIM" is no longer available. To use SAT solvers in NuSMV, now "MiniSAT" or "ZCHaff" are required.

New features details

  • SMV and PSL grammar
    • Support for arrays and matrices has been improved.
      • Array and matrices subscript can be non-constant numeric expressions (only when reading), and they can also be passed to modules as parameters.
      • Is is now possible to declare arrays of expressions. For example:
        DEFINE x := [[1,2,3], [4,5,6]]; VAR i : -1..1; LTLSPEC G x[0][i+1] < 4
    • Besides state and input variables, it is now possible to declare frozen variables. Frozen variables are like state variables, but after the initialization they retain their value through the whole evolution of the model.
    • A new ternary operator <cond> ? <expr> : <expr> has been added to improve models readability.
    • Word support has been extended.
      • New type signed word has been introduced, along with a few new operators: extend, signed and unsigned.
      • New operators have been introduced to easily manipulate word constants. They are uwconst, swconst, sizeof and toint.
      • The PSL grammar now supports word operations. All SMV word operators are supported, made exception for the bit-selection operator, which has a different syntax in PSL [select(w, h, l)].
    • Properties can now be named in the SMV model. The syntax for property naming is NAME pname := expr
  • System commands
    • Model compilation
      • Added -k number options and -t time option to the compute_reachable command, which respectively limit the forward search in number of steps or in execution time.
      • Added the clean_bdd_cache command. Cleans the cached results of evaluations of symbolic expressions to ADD and BDD representations.
      • Added the -d option to the flatten_hierarchy command. This option delays the construction of vars constraints until needed
    • Model Checking
      • Added the check_invar_bmc_inc command, used for checking invariant specifications using BMC incremental algorithms.
      • Added the check_ltlspec_bmc_inc command, used for checking LTL specifications using BMC incremental algorithms.
      • Added some new options to the check_invar command, to control the new analysis strategies and heuristics.
      • Added the -P name command option to all property-checking commands (check_ctlspec, check_ltlspec, etc.) to refer to a property named in the model..
    • Simulation
      • Added the bmc_pick_state command. Similarly to pick_state, chooses an element from the set of initial states, and makes it the current state. This must be done in order to proceed with BMC simulation
      • Added the bmc_inc_simulate command. Does the same as bmc_simulate, but using incremental algorithms.
      • Added the bmc_simulate_check_feasible_constraints command, used to check whether or not a given constraint is feasible and can thus be used as BMC simulation constraint.
    • Trace and counter-examples
      • Added commands execute_traces and execute_partial_traces, respectively used for complete and incomplete traces execution. Complete or even incomplete traces can now be executed within the model, to check whether or not the trace contains only valid assignments that are feasible in the model.
    • Model inspection, dumpers, etc.
      • Added the print_formula command, which prints a formula in canonical format.
      • Added the show_dependencies command, which shows the dependencies for the given expression
      • Added the write_coi_model command, which dumps on a file the model reduced w.r.t. cone of influence over a given property.
      • Added the -p option to the print_fsm_stats command, which prints out the normalized predicates the FSM consists of.
      • Added a few options to the print_reachable_states command, to enrich the features it provides.
      • Added -2 and -n options to the echo command. -2 prints the given string to stderr instead of stdout. -n does not add a trailing newline to the printed string.
  • Command line options
    • Added option -source sc_file: Executes NuSMV commands from file sc_file. -source is an alias for -load which is now deprecated.
    • Added option -disable_bdd_cache to disable bdd reachable states caching.
    • Added option -bdd_soh heuristics to set the heuristics to be used to compute BDD ordering statically by analyzing the input model.
    • Added option -ojeba alg to set the algorithm used for BDD-based language emptiness of Buchi fair transition systems.
  • System variables
    • System variables are now printed in a lexicographic order when calling command set
    • Added system variable bdd_static_order_heuristics, which sets the heuristics for guessing a good ordering by analyzing the input model.
    • Added system variable bmc_inc_invar_alg, which sets the default algorithm for BMC incremental invariants checking.
    • Added system variable check_invar_bddbmc_heuristic, which sets the bdd-bmc heuristics to be used when using bdd-bmc BDD invariants checking strategy
    • Added system variable check_invar_bddbmc_threshold, which sets the threshold to be used when using bdd-bmc BDD invariants checking strategy
    • Added system variable check_invar_forward_backward_heuristic, which sets the heuristics used for forward-backward strategy when checking invariants using BDD.
    • Added system variable check_invar_strategy, which sets the strategy to be used for BDD based invariants specifications checking.
    • Added system variable counter_examples_hiding_prefix. Symbols names that match this string prefix will be not printed out when showing a trace
    • Added system variable counter_examples_show_re. Only symbols whose names match this regular expression will be printed out when showing a trace.
    • Added system variable daggifier_counter_threshold, daggifier_depth_threshold and daggifier_statistics, which control the model dumper behavior.
    • Added system variable enable_bdd_cache, which determines if during evaluation of symbolic expression to ADD and BDD representations the obtained results are cached or not.
    • Added system variable oreg_justice_emptiness_bdd_algorithm, which sets the algorithm used to determine language emptiness of a Buchi fair transition system.
    • Added system variable rbc_rbc2cnf_algorithm, which defines the algorithm used for conversion from RBC to CNF format.
    • Added system variable show_defines_in_traces, which controls whether defines should be printed as part of a trace or be skipped.
    • Added system variable trace_show_defines_with_next, which controls whether defines containing next operator should be printed as part of a trace or be skipped.
    • Added system variable use_coi_size_sorting, which enables/disables the use of the cone of influence variables set size for properties sorting, before the verification step.

Bug fixes and other improvements:

  • Fixed the precedence of mod operator. Now it has the same precedence as division.
  • Fixed some 64-bits issues in the Cudds library and in the NuSMV's core.
  • Win64 and OSX-64 are now supported.
  • Fixed several dozens of bugs. See ChangeLog for details.

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/