nuseenICST17 Paolo Arcaini Angelo Gargantini Elvinia Riccobene

NuSeen: a tool framework for the NuSMV model checker

in 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017) - Testing Tools Papers Track (2017)

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] [The tool is available at]

My sw links