---
abstract: 'We present here a case study developing a parallel program. The approach that we use combines refinement and decomposition techniques. This involves in the first step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via refinement. Afterwards, decomposition is applied to separate the resulting model into sub-models for different processes. These sub-models are later independently developed using refinement. Our approach aids the understanding of parallel programs and reduces the complexity in their proofs of correctness.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - htson@inf.ethz.ch
  - jabrial@inf.ethz.ch
creators_name:
  - family: Hoang
    given: Thai Son
    honourific: ''
    lineage: ''
  - family: Abrial
    given: Jean-Raymond
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-02
date_type: published
datestamp: 2010-02-05 10:39:21
department: ~
dir: disk0/00/00/02/06
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 206
event_dates: ~
event_location: ~
event_title: ABZ2010
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
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-02-05 10:39:21
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
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: 6
series: ~
skill_areas: []
source: ~
status_changed: 2010-02-05 10:39:21
subjects:
  - deploy_method_comp
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Event-B Decomposition for Parallel Programs
type: conference_item
userid: 16
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>