Abstrakt
NuSeen is a framework that assists a designer during the modeling and V&V activities when using the NuSMV model checker. 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.