Abstract
NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is
very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements
specified as temporal properties. In this paper, we propose \NuSeen, a framework that assists a designer during the modeling
and V&V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline,
\NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples.
It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the
framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests
achieving value and decision coverage for NuSMV models.
[download the pdf file] [DOI] [The tool is available at http://nuseen.sourceforge.net//]