creators_name: Diaconescu, Denisa creators_name: Leustean, Ioana creators_name: Petre, Luigia creators_name: Sere, Kaisa creators_name: Stefanescu, Gheorghe creators_id: Kaisa.Sere@abo.fi type: conference_item datestamp: 2012-03-23 09:32:25 lastmod: 2012-03-23 09:32:25 metadata_visibility: show title: Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems ispublished: inpress subjects: Refinement subjects: theory full_text_status: public pres_type: paper abstract: The state-based formal method Event-B relies on the concept of correct stepwise development, ensured by discharging corresponding proof obligations. The register-voice interactive systems (rv-IS) formalism is a recent approach for developing software systems using both structural state-based as well as interaction-based composition operators. One of the most interesting feature of the rv-IS formalism is the structuring of the components interactions. In order to study whether a more structured (rv-IS inspired) interaction approach can significantly ease the proof obligation effort needed for correct development in Event- B, we need to devise a way of integrating these formalisms. In this paper we propose a refinement-based translation from Event-B to rv-IS, exemplified with a file transfer protocol modelled in both formalisms. date: 2012-06-19 date_type: published event_title: 9th International Conference on Integrated Formal Methods (iFM'12) event_location: Pisa event_dates: June 19-21, 2012 event_type: conference refereed: TRUE citation: Diaconescu, Denisa and Leustean, Ioana and Petre, Luigia and Sere, Kaisa and Stefanescu, Gheorghe (2012) Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems. In: 9th International Conference on Integrated Formal Methods (iFM'12), June 19-21, 2012, Pisa. (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/383/1/paper40iFM2012CameraReady.pdf