@inproceedings{deploy383,
       booktitle = {9th International Conference on Integrated Formal Methods (iFM'12)},
           month = {June},
           title = {Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems},
          author = {Denisa Diaconescu and Ioana Leustean and Luigia Petre and Kaisa Sere and Gheorghe Stefanescu},
            year = {2012},
             url = {http://deploy-eprints.ecs.soton.ac.uk/383/},
        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.}
}

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>