"383","Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems","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.","http://deploy-eprints.ecs.soton.ac.uk/383/","Diaconescu, Denisa and Leustean, Ioana and Petre, Luigia and Sere, Kaisa and Stefanescu, Gheorghe","UNSPECIFIED","       <span class=\"person_name\">Diaconescu, Denisa</span> and <span class=\"person_name\">Leustean, Ioana</span> and <span class=\"person_name\">Petre, Luigia</span> and <span class=\"person_name\">Sere, Kaisa</span> and <span class=\"person_name\">Stefanescu, Gheorghe</span>     (2012)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/383/\"><em>Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems.</em></a>       In: 9th International Conference on Integrated Formal Methods (iFM'12), June 19-21, 2012, Pisa.         (In Press)   ",",,,Kaisa.Sere@abo.fi,","2012-06-19"
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>