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.

(2017). NuSeen: A Tool Framework for the NuSMV Model Checker . Retrieved from http://hdl.handle.net/10446/116147

NuSeen: A Tool Framework for the NuSMV Model Checker

Arcaini, Paolo;Gargantini, Angelo;
2017-01-01

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.
2017
Arcaini, Paolo; Gargantini, Angelo Michele; Riccobene, Elvinia
File allegato/i alla scheda:
File Dimensione del file Formato  
nuseen_icst17ttt.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 345.55 kB
Formato Adobe PDF
345.55 kB Adobe PDF   Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/116147
Citazioni
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 7
social impact