A Quantitative Completeness Analysis for Property-Sets

This paper defines a quantitative metric of the completeness of a formal specification. A "good" (formal) specification is already needed in the beginning of the development process to prevent cost-intensive corrections of errors found in the late phases of a design process. A quantitative analysis method is presented to evaluate whether a specification is "good". The method considers only the formal specification, an implementation (design) is not necessary. Thus, an analysis of a specification can be directly done. The properties of the specification are transformed into a normal form to calculate the metric. Experimental results of the analysis method are given, e. g., metrics for specifications of the AMBA AHB bus.