[We apologize if you received multiple copies of this message] N N SSSSS M M V V 2222 NN N S MM MM V V 2 2 N N N S M M M M V V 2 N N N u u SSSSS M M M V V 2 N N N u u S M M V V 2 N NN u u S M M V V 2 N N uuuu SSSSS M M V 222222 V E R S I O N 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 http://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: - COCONUT, COrrect-by-CONstrUcTion Workbench for Design and Verification of Embedded Systems (http://www.coconut-project.eu/). COCONUT was founded by EU FP7-2007-IST-1-217069. - COMPASS, COrrectness, Modeling and Performance of Aerospace SystemS (http://compass.informatik.rwth-aachen.de) - EuRailCheck, European Railways Verification and Validation Tool (http://es.fbk.eu/projects/eurailcheck). 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 ---------------------------------------------------------------------- o Added forward version of the Emerson-Lei algorithm for checking language emptiness of Buchi fair transitions systems with BDDs. o Improved invariant checking with new search strategies and heuristics. o Extended the language support for arrays and matrices. o Added several commands and options to dump the model. See the details about commands and options below. o 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 ---------------------------------------------------------------------- o 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 " ? : " 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" o 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. o 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. o 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. ======== OVERVIEW ======== NuSMV is a reimplementation 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 testbed for formal verification techniques. NuSMV version 2 extends NuSMV with new model checking algorithms and techniques. It combines classical BDD-based 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 the SIM SAT library developed by the University of Genova. Optionally, NuSMV can also be used with the ZCHAFF SAT library developed by Princeton University. 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. Further details on NuSMV 2 and on the NuSMV project can be found 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 . 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 AT 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 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. The NuSMV team has also received several contributions for different part of the system. In particular: * Ariel Fuxman has extended the LTL to SMV tableau translator to the past fragment of LTL * Rik Eshuis has contributed a strong fairness model checking algorithm for LTL specifications * Dan Sheridan 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. ================ GETTING IN TOUCH ================ The home page of the NuSMV project is . For questions, comments, or information on NuSMV, please e-mail to . For getting in touch with the NuSMV development staff, please email to . ============= MAILING LISTS ============= We maintain two mailing lists on NuSMV: * nusmv-users General questions, bugs and bug fixes, possible extensions and user requests on NuSMV can be discussed on this list. * nusmv-announce New releases and other important events for NuSMV will be announced on this list. If you are interested in the usage and in the development of NuSMV, we encourage you to subscribe to these mailing lists, using the form available at url . =========== 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 use the bug report form available at url , or send an email to with the description of the bug. -- NuSMV Staff http://nusmv.fbk.eu/