Among possible model validation techniques able to identify defects early in the system development, model review aims also at determining if a model is of sufficient quality, where quality is measured as the absence of certain faults. In this paper, we tackle the problem of automatic reviewing NuSMV formal specifications by developing a model advisor which helps to assure given model qualities for NuSMV programs. Vulnerabilities and defects a developer can introduce during the modeling activity using NuSMV are expressed as the violation of formal meta-properties. These meta-properties are then mapped to temporal logic formulas, and the NuSMV model checker itself is used as the engine of our model advisor to notify meta-properties violations, so revealing the absence of some quality attributes of the specification. As a proof of concept, we also report the result of applying this review process to several NuSMV specifications.

A model advisor for NuSMV specifications

ARCAINI, Paolo;GARGANTINI, Angelo Michele;
2011-01-01

Abstract

Among possible model validation techniques able to identify defects early in the system development, model review aims also at determining if a model is of sufficient quality, where quality is measured as the absence of certain faults. In this paper, we tackle the problem of automatic reviewing NuSMV formal specifications by developing a model advisor which helps to assure given model qualities for NuSMV programs. Vulnerabilities and defects a developer can introduce during the modeling activity using NuSMV are expressed as the violation of formal meta-properties. These meta-properties are then mapped to temporal logic formulas, and the NuSMV model checker itself is used as the engine of our model advisor to notify meta-properties violations, so revealing the absence of some quality attributes of the specification. As a proof of concept, we also report the result of applying this review process to several NuSMV specifications.
journal article - articolo
2011
Arcaini, Paolo; Gargantini, Angelo Michele; Riccobene, Elvinia
File allegato/i alla scheda:
File Dimensione del file Formato  
Gargantini - Model advisor for NuSMV.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 224.05 kB
Formato Adobe PDF
224.05 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/25640
Citazioni
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact