NFM2010 Arcaini, Paolo Gargantini, Angelo Riccobene, Elvinia

Automatic review of Abstract State Machines by Meta Property Verification

in Proceedings of the Second NASA Formal Methods Symposium (NFM 2010) (Eds. C\'esar Mu\ noz) , n. NASA/CP-2010-216215 (2010)

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]

My sw links