creators_name: Olszewska, Marta creators_name: Sere, Kaisa creators_id: mplaska@abo.fi creators_id: Kaisa.Sere@abo.fi type: conference_item datestamp: 2010-10-26 06:06:50 lastmod: 2010-10-26 06:08:56 metadata_visibility: show title: Specification Metrics for Event-B Developments ispublished: pub subjects: deploy_industrial_space subjects: deploy_method_other subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplatform subjects: theory full_text_status: public pres_type: paper 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. date: 2010-09-20 date_type: published pagerange: 1-12 event_title: CONQUEST 2010 event_location: Dresden, Germany event_dates: 20-22 September 2010 event_type: conference refereed: TRUE citation: Olszewska, Marta and Sere, Kaisa (2010) Specification Metrics for Event-B Developments. In: CONQUEST 2010, 20-22 September 2010, Dresden, Germany. document_url: http://deploy-eprints.ecs.soton.ac.uk/249/1/OlSe_Conquest2010.pdf