• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems

Denisa Diaconescu, Ioana Leustean, Luigia Petre, Kaisa Sere, Gheorghe Stefanescu, Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems. In: Diego Latella, Helen Treharne (Eds.), 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science 7321, 221–236, Springer, Heidelberg, 2012.

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.

BibTeX entry:

@INPROCEEDINGS{inpDiLePeSeSt12a,
  title = {Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems},
  booktitle = {9th International Conference on Integrated Formal Methods (iFM 2012)},
  author = {Diaconescu, Denisa and Leustean, Ioana and Petre, Luigia and Sere, Kaisa and Stefanescu, Gheorghe},
  volume = {7321},
  series = {Lecture Notes in Computer Science},
  editor = {Latella, Diego and Treharne, Helen},
  publisher = {Springer, Heidelberg},
  pages = {221–236},
  year = {2012},
  keywords = {Event-B, refinement, register-voice interactive systems, file transfer protocol, scenario-based semantics, streams, traces},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication