Software measurement and formal methods: a case study centered on TRIO+ specifications

This paper presents a case study where product measures are defined for a formal specification language (TRIO+) and are validated as quality indicators. To this end, defect and effort data were collected during the development of a monitoring/control system for a power plant. We show that some of the underlying hypotheses of these measures are supported by empirical results and that several measures are significant early indicators of specification change and effort. From a more general perspective, this study exemplifies one important advantage of formal specifications: they are measurable and can thus be better controlled, assessed, and managed than informal ones.