---
abstract: 'The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal method that allows modelling and refinement of systems. The combination, reuse and validation of component specifications are not currently supported in Event-B. We extend the Event-B formalism using shared event composition as an option for developing (distributed) systems. Refinement is used in the development of specifications using composed machines and we prove that properties and proof obligations of specifications can be reused to ensure valid composed specifications. The main contributions of this work are the Event-B extension to support shared event composition and refinement including the proof obligations for a composed machine.'
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
creators_name:
  - family: Silva
    given: Renato
    honourific: ''
    lineage: ''
data_type: ~
date: 2011-12-03
date_type: published
datestamp: 2012-05-16 08:20:52
department: ~
dir: disk0/00/00/03/98
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 398
event_dates: 20-24 June 2011
event_location: 'Lero, Limerick, Ireland'
event_title: B 2011 Workshop
event_type: workshop
exhibitors_id: []
exhibitors_name: []
fileinfo: /398/1.hassmallThumbnailVersion/Towards%20the%20Composition%20of%20Speci%EF%AC%81cations%20%20in%20Event-B.pdf;/398/1/Towards%20the%20Composition%20of%20Speci%EF%AC%81cations%20%20in%20Event-B.pdf
full_text_status: public
funders:
  - FCT
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:17:01
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://www.sciencedirect.com/science/article/pii/S1571066111001691
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: 12
series: ~
skill_areas: []
source: ~
status_changed: 2012-05-16 08:20:52
subjects:
  - Event-Bsemantics
  - Refinement
  - deploy_method_comp
  - deploy_tooldev_rodinplugins
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Towards the Composition of Specifications in Event-B
type: conference_item
userid: 257
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>