---
abstract: "Feature-oriented modelling is a well-known approach for Software Product \r\nLine (SPL) development. It is a widely used method when developing groups of \r\nrelated software. With an SPL approach, the development of a software product \r\nis quicker, less expensive and of higher quality than a one-off development since \r\nmuch effort is re-used. However, this approach is not common in formal methods \r\ndevelopment, which is generally high cost and time consuming, yet crucial in \r\nthe development of critical systems. With the increase of more complex critical \r\nsystems, it becomes more important to apply formal methods to the development \r\ncycle, and we propose a method that allows the application of SPL development \r\ntechniques to formal methods. This results in faster and cheaper development of \r\nformal systems. \r\nOur method combines Event-B [1] and feature models [2]. A feature in a \r\nfeature model represents a requirement of the product family and is formally \r\ndescribed in Event-B using special feature modelling patterns. A feature repre- \r\nsented in Event-B is referred to as component. We develop composition rules, \r\nwhich allow components to be composed. Special composition proof obligations \r\nallow the verification of the composition. \r\nThe feature model is formed by features which may be associated with Event- \r\nB components. A subset of features from the feature model can be selected to \r\nform a feature model instance, thereby selecting several of these Event-B com- \r\nponents. These components are composed pair-wise, and composition POs can \r\nbe discharged to prove properties and to ensure consistency of the composition. \r\nThe final Event-B machine represents the formal specification which is associated \r\nwith the feature model instance and is obtained by composing these components. \r\nThe motivation of our work is to allow product line development for critical \r\nsystems. We use traditional product line methods, i.e. feature modelling, and \r\nlink it with the formal method Event-B. \r\nFuture work is focussed on amending feature diagrams to reflect Event-B \r\ncomponents more precisely. Refinement patterns will also be addressed. \r\n"
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - jhs06r@ecs.soton.ac.uk
  - mrp@ecs.soton.ac.uk
  - mjb@ecs.soton.ac.uk
creators_name:
  - family: Sorge
    given: Jennifer
    honourific: ''
    lineage: ''
  - family: Poppleton
    given: Michael
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2010-02
date_type: published
datestamp: 2010-10-29 09:04:41
department: ~
dir: disk0/00/00/02/52
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 252
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/252/1/paper_53%2D1.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-29 09:04:41
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: ABZ2010
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: Springer
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 22
series: ~
skill_areas: []
source: ~
status_changed: 2010-10-29 09:04:41
subjects:
  - Event-Bsemantics
  - deploy_method_comp
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: A Basis for Feature-Oriented Modelling in Event-B
type: other
userid: 142
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>