The Role of Mutation Analysis for Property Qualification

The paper proposes a comprehensive methodology for property qualification based on a combination of dynamic and static techniques. In particular, given a set of properties defined to check the correctness of a design implementation, the methodology first evaluates property coverage, property overspecification, and it identifies vacuous properties. This is commonly performed by exploiting mutation analysis and automatic testbenches generation, i.e., dynamic strategies. This phase allows us to quickly evaluate the quality of properties with respect to the use of formal approaches. Then, a second phase, based on model checking, is applied to the restricted number of situations, where the dynamic approach is not exhaustive. Experimental results show the effectiveness and efficiency of the proposed methodology.