Specification Metrics for Event-B Developments

Abstract

In this paper we define several metrics for Event-B specifications in order to as-sess the maintainability of a rigorous system in its early development stage. We perform measurements of physical features of the specification. Moreover, we derive metrics like difficulty of constructing a specification or effort needed for its creation. The specification is investigated in the perspective of its syntactical characteristics. We base our metrics on the Event-B language primitives, namely operators and operands that we regard meaningful for our measurement model. We also use statistics about proof obligations in our metrics, as we consider the proving activity as a vital element in the process of creating a specification. Presented metrics are applied to a number of Event-B specifications, both their dynamic and static parts. They are examined in order to empirically con-firm appropriateness for management purposes. Obtained results are analysed in a perspective of an abstract specification and its consecutive refinements.