---
abstract: "The state-based formal method Event-B relies on the concept\r\nof correct stepwise development, ensured by discharging corresponding\r\nproof obligations. The register-voice interactive systems (rv-IS) formalism\r\nis a recent approach for developing software systems using both\r\nstructural state-based as well as interaction-based composition operators.\r\nOne of the most interesting feature of the rv-IS formalism is the\r\nstructuring of the components interactions. In order to study whether a\r\nmore structured (rv-IS inspired) interaction approach can significantly\r\nease the proof obligation effort needed for correct development in Event-\r\nB, we need to devise a way of integrating these formalisms. In this paper\r\nwe propose a refinement-based translation from Event-B to rv-IS, exemplified with a file transfer protocol modelled in both formalisms."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - ~
  - ~
  - ~
  - Kaisa.Sere@abo.fi
  - ~
creators_name:
  - family: Diaconescu
    given: Denisa
    honourific: ''
    lineage: ''
  - family: Leustean
    given: Ioana
    honourific: ''
    lineage: ''
  - family: Petre
    given: Luigia
    honourific: ''
    lineage: ''
  - family: Sere
    given: Kaisa
    honourific: ''
    lineage: ''
  - family: Stefanescu
    given: Gheorghe
    honourific: ''
    lineage: ''
data_type: ~
date: 2012-06-19
date_type: published
datestamp: 2012-03-23 09:32:25
department: ~
dir: disk0/00/00/03/83
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 383
event_dates: 'June 19-21, 2012'
event_location: Pisa
event_title: 9th International Conference on Integrated Formal Methods (iFM'12)
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/383/1/paper40iFM2012CameraReady.pdf
full_text_status: public
funders:
  - EC
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
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-03-23 09:32:25
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:
  - DEPLOY
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 11
series: ~
skill_areas: []
source: ~
status_changed: 2012-03-23 09:32:25
subjects:
  - Refinement
  - theory
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems
type: conference_item
userid: 263
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>