@inproceedings{deploy249, booktitle = {CONQUEST 2010}, month = {September}, title = {Specification Metrics for Event-B Developments}, author = {Marta Olszewska and Kaisa Sere}, year = {2010}, pages = {1--12}, url = {http://deploy-eprints.ecs.soton.ac.uk/249/}, 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.} }