---
abstract: 'The construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques that support reuse and allow us to formally combine sub-components through refinement steps while reusing their properties. Sub-components can result from a design or architectural goal and a refinement framework should allow further parallel development over the sub-components. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronisation over shared events and shared states are not allow. We define the necessary proof obligations to ensure a valid composition or decomposition.  We also show that shared event composition preserves refinement proofs for sub-components, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding subcomponents.  A case study applying these two techniques is illustrated using Rodin, the Event-B toolset.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - ras07r@ecs.soton.ac.uk
  - mjb@ecs.soton.ac.uk
creators_name:
  - family: Silva
    given: Renato
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-11
date_type: completed
datestamp: 2012-05-16 08:21:11
department: ~
dir: disk0/00/00/03/99
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 399
event_dates: November 2010
event_location: 'Graz, Austria'
event_title: Formal Methods for Components and Objects 2010
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /399/1.hassmallThumbnailVersion/comp_decomp_paper.pdf;/399/1/comp_decomp_paper.pdf
full_text_status: public
funders:
  - Fundação Ciência e Tecnologia
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: ~
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: 2012-05-18 14:16:58
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://www.informatik.uni-trier.de/~ley/db/conf/fmco/fmco2010.html
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects:
  - Deploy
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 13
series: ~
skill_areas: []
source: ~
status_changed: 2012-05-16 08:21:11
subjects:
  - Event-Bsemantics
  - Refinement
  - deploy_method_comp
  - deploy_tooldev_modelc
  - deploy_tooldev_rodinplugins
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Shared Event Composition/Decomposition in Event-B
type: conference_item
userid: 257
volume: ~