Linuxtrent: NuSMV 2
- From: Emanuele Olivetti <olivetti@xxxxxx>
- To: linuxtrent <linuxtrent@xxxxxxxxxxxxx>
- Date: Tue, 13 Nov 2001 10:42:59 +0100
Vi annuncio che, con il mio gruppo qui in IRST (e' il gruppo di Metodi Formali
della divisione di Sistemi di Ragionamento Automatico
http://sra.itc.it/research_area.epl?name=Formal+Methods),
abbiamo scritto la nuova versione del software di Model Checking "NuSMV 2"
con licenza LGPL (!).
Con questo software e' possibile verificare esattamente (ovvero con una
dimostrazione matematica) e automaticamente se una determinata proprieta' e'
rispettata da un sistema descritto tramite un opportuno linguaggio formale
(e' un di linguaggio di programmazione). Questo tipo di software viene
utilizzato per la progettazione di circuiti elettronici, sistemi di controllo,
software ecc., per sapere esattamente (e prima di produrre e mettere in
opera/vendita il sistema) se ci sono bachi in progettazione.
Oggi ha un buon successo, per esempio, tra i produttori di CPU.
Con la versione 2 inizia anche la distribuzione Open Source e quindi il
modello di sviluppo che tutti ben conosciamo.
NuSMV e' stato sviluppato da tante persone di varie istituzioni nel corso di
anni di lavoro e la nuova versione 2 introduce molte novita' dal punto di
vista funzionale.
Una cosa importante: e' sviluppato completamente in ambiente Linux utilizzando
prodotti Open Source. E' previsto a breve il porting (la ricompilazione piu'
che altro) per altri *nix e per win32 (cygwin inizialmente).
Che altro dire... forse non sara' utile proprio a tutti pero' ci tenevo a
dirvelo :-)
il sito: http://nusmv.irst.itc.it
Emanuele
P.S.: vi allego l'annuncio ufficiale (piu' formale) che stiamo distribuendo.
P.S.2: comunque NuSMV potrebbe esservi piu' utile di quanto immaginate...;-)
-- Attached file included as plaintext by Listar --
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 . 0 . 0
We are happy to announce the availability of a new version of the
NuSMV model checker. NuSMV version 2.0.0 is available from
http://nusmv.irst.itc.it
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).
Moreover, NuSMV 2 is distributed with an OpenSource license, namely
the GNU Lesser General Public License (LGPL, see the COPYRIGHT
below). The aim is to provide a publicly available state-of-the-art
symbolic model checker, and to allow anybody interested to participate
in its development.
We are looking for partners and contributors to the OpenSource
development of NuSMV. If you would like to
- develop a new functionality or an improvement,
- ask for an extension to NuSMV,
- request information or simply state your opinion,
please email the NuSMV mailing list <nusmv-users@xxxxxxxxxxx>.
========
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 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
implements new partitioning techniques; 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 a Bounded Model Checker, connected to the
SIM SAT library developed by the University of Genova.
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.
=========
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 the CUDD library is copyright University of Colorado. The
CUDD library is *not* covered by LGPL.
Please contact <nusmv-users@xxxxxxxxxxx> if you have any doubt or
comment on the license.
========
PARTNERS
========
Different partners have contributed code for the initial release of
NuSMV 2. Every source file in the NuSMV 2 distribution contains a
header that acknowledges the copyright holders for the file.
In particular:
* CMU and ITC-IRST contributed the source code on 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 on 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.
Ken McMillan (Cadence) has expressed an interest in contributing to
the project with the improvements that have been carried out on
Cadence SMV along the years. Statements of interest have also come
from several other commercial and academic institutions.
================
GETTING IN TOUCH
================
The home page of the NuSMV project is <http://nusmv.irst.itc.it/>.
For questions, comments, or information on NuSMV, please e-mail to
<nusmv-users@xxxxxxxxxxx>.
For getting in touch with the NuSMV development staff, please email to
<nusmv@xxxxxxxxxxx>.
=============
MAILING LISTS
=============
We maintain two mailing lists on NuSMV:
* nusmv-users <nusmv-users@xxxxxxxxxxx>
General questions, bugs and bug fixes, possible extensions and user
requests on NuSMV can be discussed on this list.
* nusmv-announce <nusmv-announce@xxxxxxxxxxx>
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 <http://nusmv.irst.itc.it/mail.html>.
===========
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
<http://nusmv.irst.itc.it/bug_report.html>, or send an email to
<nusmv-users@xxxxxxxxxxx> with the description of the bug.
--
NuSMV Staff <nusmv@xxxxxxxxxxx>
http://nusmv.irst.itc.it/
--
Per iscriversi (o disiscriversi), basta spedire un messaggio con SOGGETTO
"subscribe" (o "unsubscribe") a mailto:linuxtrent-request@xxxxxxxxxxxxxxxxx
Other related posts:
