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, 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]