nusmvma11 Arcaini, Paolo Gargantini, Angelo Riccobene, Elvinia

A Model Advisor for NuSMV Specifications

in Innovations in Systems and Software EngineeringSpringer London, vol. 7 (2011): 97-107

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, since 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 \emphmodel 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 engine of our model advisor to notify meta-pro\-per\-ties 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.

[download the pdf file] [DOI]

My sw links