Published in

Elsevier, Electronic Notes in Theoretical Computer Science, (280), p. 69-80, 2011

DOI: 10.1016/j.entcs.2011.11.019

Links

Tools

Export citation

Search in Google Scholar

Bounded Retransmission in Event-B∥CSP: a Case Study

Journal article published in 2011 by Steve A. Schneider, Helen Treharne, Heike Wehrheim
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Red circle
Postprint: archiving forbidden
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO

Abstract

Event-B∥CSP is a combination of Event-B and CSP in which CSP controllers are used in conjunction with Event-B machines to allow a more explicit approach to control flow. Recent results have provided an approach to stepwise refinement of such combinations. This paper presents a simplified Bounded Retransmission Protocol case study, inspired by Abrialʼs treatment of this example, to illustrate several aspects new in the approach. The case study includes refinement steps to illustrate four different aspects of this approach to refinement: (1) splitting events; (2) introducing convergent looping behaviour; (3) the relationship between anticipated, convergent, and devolved events; and (4) converging anticipated events.