---
abstract: 'Formal modelling is indispensable for engineering highly dependable systems. However, a wider acceptance of formal methods is hindered by their insufficient usability and scalability. In this paper, we aim at assisting developers in rigorous modelling and design by increasing automation of development steps. We introduce a notion of refinement patterns – generic representations of typical correctness-preserving model transformations. Our definition of a refinement pattern contains a description of syntactic model transformations, as well as the pattern applicability conditions and proof obligations for verifying correctness preservation. This work establishes a basis for building a tool that would support formal system development via pattern reuse and instantiation. We present a prototype of such a tool and some examples of refinement patterns for automated development in the Event B formalism.'
accompaniment: []
book_title: ' Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers.'
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: ''
data_type: ~
date: 2010
date_type: published
datestamp: 2010-12-03 11:16:09
department: ~
dir: disk0/00/00/02/59
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id:
  - ~
  - ~
  - ~
  - leuschel@cs.uni-duesseldorf.de
editors_name:
  - family: de Boer
    given: Frank S.
    honourific: ''
    lineage: ''
  - family: Bonsangue
    given: Marcello M.
    honourific: ''
    lineage: ''
  - family: Hallerstede
    given: Stefan
    honourific: ''
    lineage: ''
  - family: Leuschel
    given: Michael
    honourific: ''
    lineage: ''
eprint_status: archive
eprintid: 259
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/259/1/main%2Dfmco%2Dbook%2D2010.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: 978-3-642-17070-6
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-12-09 15:37:03
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: 6286
official_url: ~
output_media: ~
pagerange: 70-88
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: Springer
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 22
series: LNCS
skill_areas: []
source: ~
status_changed: 2010-12-03 11:16:09
subjects:
  - Event-Bsemantics
  - deploy_method_comp
  - deploy_method_resil
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Patterns for Refinement Automation
type: book_section
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>