--- 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.\r\n\r\nPresented 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." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: mplaska@abo.fi copyright_holders: [] corp_creators: [] creators_id: - mplaska@abo.fi - Kaisa.Sere@abo.fi creators_name: - family: Olszewska given: Marta honourific: '' lineage: '' - family: Sere given: Kaisa honourific: '' lineage: '' data_type: ~ date: 2010-09-20 date_type: published datestamp: 2010-10-26 06:06:50 department: ~ dir: disk0/00/00/02/49 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 249 event_dates: 20-22 September 2010 event_location: 'Dresden, Germany' event_title: CONQUEST 2010 event_type: conference exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/249/1/OlSe_Conquest2010.pdf full_text_status: public funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-10-26 06:08:56 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: 1-12 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 42 series: ~ skill_areas: [] source: ~ status_changed: 2010-10-26 06:06:50 subjects: - deploy_industrial_space - deploy_method_other - deploy_tooldev_modelc - deploy_tooldev_rodinplatform - theory succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Specification Metrics for Event-B Developments type: conference_item userid: 261 volume: ~