Abstract
A model review is a validation technique aiming to determine if a model not only fulfils the intended requirements, but also
are of sufficient quality to be easy to develop, maintain, and enhance. The model review process is of extremely importance
since it allows to identify defects early in the system development, reducing the cost of fixing them. Usually model review
is performed by external qualified people, but there is nowadays an increasing desire to automatize this process by systematically
checking formal specifications for known vulnerabilities or defects. In this paper we propose a technique to perform automatic
review of Abstract State Machine formal specifications. We first detect a family of typical vulnerabilities and defects a
developer can introduce during the modelling activity using the ASMs (or any other state-transition based formal approach)
and we express such faults as the violation of meta-properties that guarantee certain quality attributes of the specification.
These meta-properties are defined in terms of two logical operators Always and Sometime to capture properties that must be
true in every state or eventually true in at least one state of the ASM under analysis. Then, we map the logical operators
always and sometime to temporal logic formulas and we exploit the model checking facilities of AsmetaSMV, a model checker
for ASM models based on NuSMV, to check the meta-property violation. The violation of a meta-property always means that the
quality attribute is not met and indicates a potential fault in the model. As a proof of concept, we also report the result
of applying this ASM review process to some benchmark specifications.
[download the pdf file]