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

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 and control system for a power plant. We show that some of the underlying hypotheses of these measures are supported bp 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.