TY - INPR ID - deploy383 UR - http://deploy-eprints.ecs.soton.ac.uk/383/ A1 - Diaconescu, Denisa A1 - Leustean, Ioana A1 - Petre, Luigia A1 - Sere, Kaisa A1 - Stefanescu, Gheorghe Y1 - 2012/06/19/ N2 - 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. TI - Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems AV - public M2 - Pisa T2 - 9th International Conference on Integrated Formal Methods (iFM'12) ER -