---
abstract: "Recently, Space Systems Finland has undertaken formal Event B development of a part of on-board software for the BepiColombo space mission. As a result, lack of modularization mechanisms in Event B has been identified as a serious  obstacle to scalability. One of the main benifits of modularization is that it allows us to decompose system models into components that can be independently developed.  It also helps to manage complexity of models that in the industrial setting are usually  very large and difficult to comprehend. On the other hand, modularization enables  reuse of formally developed components in the formal product line development.  In this paper we propose a conservative extension of Event B formalism to support modularization. We demonstrate how our approach can support reuse in the formal  development in the space domain. \r\n"
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - '"Alexei Iliasov" <Alexei.Iliasov@newcastle.ac.uk>'
  - Elena.Troubitsyna@abo.fi
  - Linas.Laibinis@abo.fi
  - alexander.romanovsky@ncl.ac.uk
  - ~
  - ~
  - ~
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
  - family: Troubitsyna
    given: Elena
    honourific: ''
    lineage: ''
  - family: Laibinis
    given: Linas
    honourific: ''
    lineage: ''
  - family: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
  - family: Varpaaniemi
    given: Kimmo
    honourific: ''
    lineage: ''
  - family: Ilic
    given: Dubravka
    honourific: ''
    lineage: ''
  - family: Latvala
    given: Timo
    honourific: ''
    lineage: ''
data_type: ~
date: 2010
date_type: published
datestamp: 2010-01-11 08:48:50
department: ~
dir: disk0/00/00/01/72
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 172
event_dates: 'February 22-25, 2010'
event_location: 'Orford, Québec, Canada'
event_title: 'Abstract State Machines (ASM), Alloy, B and Z  Conference (ABZ 2010)'
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/172/1/Modules_paper%2Dsubmitted.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-04-19 15:05:59
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: 174-188
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: 27
series: ~
skill_areas: []
source: ~
status_changed: 2010-01-11 08:48:50
subjects:
  - Event-Bsemantics
  - Refinement
  - deploy_industrial_space
  - deploy_method_comp
  - deploy_tooldev_rodinplugins
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: "Supporting Reuse in Event B Development: Modularisation Approach \r\n"
type: conference_item
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>