University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Bounded Retransmission in Event-B||CSP: A Case Study

Schneider, Steve A., Treharne, Helen and Wehrheim, Heike (2011) Bounded Retransmission in Event-B||CSP: A Case Study Department of Computing, University of Surrey. (Unpublished)


Download (433kB)


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.

Item Type: Other
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
Schneider, Steve
Wehrheim, Heike
Date : 21 March 2011
Uncontrolled Keywords : Event-B, CSP, Bounded Retransmission Protocol, Stepwise Refinement
Depositing User : Christine Daoutis
Date Deposited : 25 Mar 2011 13:58
Last Modified : 06 Jul 2019 05:07

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800